arm: fix a bug in gen-inverse-behavior (use reg-range-db for shfarg i…

…nstead of #t)

GA/test-search.rkt

@@ -8,7 +8,7 @@
 
 
 (define parser (new GA-parser%))
-(define machine (new GA-machine% [config 5]))
+(define machine (new GA-machine% [config 1]))
 
 (define printer (new GA-printer% [machine machine]))
 (define simulator-racket (new GA-simulator-racket% [machine machine]))
@@ -28,16 +28,17 @@
 
 (define prefix 
 (send parser ir-from-string "
-drop pop a 325 a! !
+0 a! !+ 0 
 "))
 
 (define postfix
 (send parser ir-from-string "
+2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ push drop pop dup over - 1 + 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ 2/ over - and + push drop pop
 "))
 
 (define code
 (send parser ir-from-string "
-2* 2* @+ 3 and +
+0 b! @b 2/ 2/ 2/ 2/
 "))
 
 
@@ -55,15 +56,18 @@ drop pop a 325 a! !
 (define encoded-code (send printer encode code))
 (define encoded-sketch (send printer encode sketch))
 
+(define t1 (current-seconds))
 (define f
   (send backward synthesize-window
         encoded-code ;; spec
         encoded-sketch ;; sketch = spec in this case
         encoded-prefix encoded-postfix
-        (constraint s t) 1 11 3600
+        (constraint r s t) 1 11 3600
         ;#:assume (constrain-stack 
         ;          machine '((<= . 65535) (<= . 65535) (<= . 65535)))
         ))
+(define t2 (current-seconds))
+(pretty-display `(time ,(- t2 t1)))
 #|(send stoch superoptimize encoded-code 
       (constraint machine [reg 0] [mem]) ;; constraint
       (constraint machine [reg 0] [mem]) ;; live-in

arm/arm-inverse.rkt

@@ -49,7 +49,7 @@
       (define shfop (inst-shfop my-inst))
       (define shfarg (inst-shfarg my-inst))
       (when (and shfop (member (vector-ref shf-opcodes shfop) shf-inst-reg))
-            (vector-set! in shfarg #t))
+            (vector-set! in shfarg reg-range-db))
 
       (for ([arg (inst-args my-inst)]
 	    [type arg-types])
@@ -194,3 +194,40 @@
 
 
     ))
+
+#|
+(require "arm-simulator-racket.rkt" "arm-parser.rkt" "arm-printer.rkt")
+
+(define (test)
+  
+  (define parser (new arm-parser%))
+  (define machine (new arm-machine% [config (list 4 1 0 )] [bitwidth 4]))
+  
+  (define printer (new arm-printer% [machine machine]))
+  (define simulator-racket (new arm-simulator-racket% [machine machine]))
+  (define inverse (new arm-inverse% [machine machine] [simulator simulator-racket]))
+
+  (define code
+    (send parser ir-from-string "
+        sub r0, r1, r2, lsl r3
+"))
+  (define encoded-code (send printer encode code))
+  (define my-inst (vector-ref encoded-code 0))
+  
+  (define code2
+    (send parser ir-from-string "
+        sub r0, r2, r0, lsl r1
+"))
+  (define encoded-code2 (send printer encode code2))
+  (define my-inst2 (vector-ref encoded-code2 0))
+  
+  (send inverse gen-inverse-behavior my-inst)
+
+  (define state1 (vector '#(-8 #f #f)
+                           '#()
+                           -1 0))
+  (define live-out (cons (list 0) (list)))
+
+  (send inverse interpret-inst my-inst2 state1 live-out)
+  )
+|#

forwardbackward.rkt

@@ -392,6 +392,7 @@
     (define t-extra 0)
     (define t-verify 0)
     (define c-build-hash 0)
+    (define c-mask 0)
     (define c-intersect 0)
     (define c-interpret-0 0)
     (define c-interpret 0)
@@ -571,7 +572,7 @@
       (define states2-vec 
 	(map (lambda (x) (mask-in (send machine progstate->vector x) live2-list #:keep-flag try-cmp)) states2))
 
-      (when info
+      (when debug
             (pretty-display `(states1-vec ,states1-vec))
             (pretty-display `(states2-vec ,states2-vec))
             (pretty-display `(live2-vec ,live2-vec))
@@ -652,7 +653,7 @@
                      (send simulator interpret (vector-append spec-precise postfix-precise) ce-input)]
                     [ce-output-vec
                      (send machine progstate->vector ce-output)])
-               (when debug
+               (when #t
                      (pretty-display "[6] counterexample (precise)")
                      (send machine display-state ce-input)
                      (pretty-display `(ce-out-vec ,ce-output-vec)))
@@ -718,7 +719,7 @@
                         (send simulator-abst interpret spec ce-input)]
                        [ce-output-vec
                         (send machine progstate->vector ce-output)])
-                  (when debug
+                  (when #t
                         (newline)
                         (pretty-display "[3] counterexample")
                         (pretty-display `(ce ,ce-count-extra ,ce-input-vec ,ce-output-vec)))
@@ -953,6 +954,7 @@
 			     (set! t-mask (+ t-mask (- t1 t0)))
 			     (set! t-hash (+ t-hash (- t2 t1)))
 			     (set! t-intersect (+ t-intersect (- t3 t2)))
+                             (set! c-mask (add1 c-mask))
 
 			     (when
 			      (and new-candidates (not (empty? new-candidates)))
@@ -1104,7 +1106,8 @@
 	  (when my-inst
                 (when debug
                       (send printer print-syntax-inst (send printer decode-inst my-inst))
-                      (pretty-display `(live ,my-liveout)))
+                      ;;(pretty-display `(live ,my-liveout))
+                      )
                 (define inst-id (inst->id my-inst))
                 ;; (define t-interpret 0)
                 ;; (define t-hash 0)
@@ -1120,6 +1123,7 @@
                              )
 			;;(pretty-display `(test-live ,test ,old-liveout ,out-vec ,in-vec))
 			(when (and in-vec (not (empty? in-vec)))
+                              ;;(pretty-display `(in-vec ,my-liveout))
 			      (class-insert-bw! current my-liveout test 
 						in-vec (concat-progs inst-id progs)))
                         ;; (let ([t2 (current-milliseconds)])
@@ -1154,19 +1158,19 @@
          (define ttt (current-milliseconds))
          (refine hash1 hash2 my-inst live1 live2 flag1 flag2)
          (when 
-          (and verbo (> (- (current-milliseconds) ttt) 500))
-          (pretty-display (format "search ~a ~a = ~a + ~a + ~a | ~a\t(~a + ~a/~a)\t~a ~a ~a/~a\t[~a/~a]\t~a/~a\t~a/~a (~a) ~a" 
+          (and verbo) ;;(> (- (current-milliseconds) ttt) 500))
+          (pretty-display (format "search ~a ~a = ~a + ~a + ~a | ~a\t(~a + ~a/~a)\t~a/~a ~a ~a/~a\t[~a/~a]\t~a/~a\t~a/~a (~a) ~a" 
                                   (- (current-milliseconds) ttt) ce-count-extra
                                   t-refine t-collect t-check
                                   t-build t-build-inter t-build-hash c-build-hash
-                                  t-mask t-hash t-intersect c-intersect
+                                  t-mask c-mask t-hash t-intersect c-intersect
                                   t-interpret-0 c-interpret-0
                                   t-interpret c-interpret
                                   t-extra c-extra c-check
                                   t-verify
                                   )))
          (set! t-build 0) (set! t-build-inter 0) (set! t-build-hash 0) (set! t-mask 0) (set! t-hash 0) (set! t-intersect 0) (set! t-interpret-0 0) (set! t-interpret 0) (set! t-extra 0) (set! t-verify 0)
-         (set! c-build-hash 0) (set! c-intersect 0) (set! c-interpret-0 0) (set! c-interpret 0) (set! c-extra 0) (set! c-check 0)
+         (set! c-build-hash 0) (set! c-mask 0) (set! c-intersect 0) (set! c-interpret-0 0) (set! c-interpret 0) (set! c-extra 0) (set! c-check 0)
          (set! t-refine 0) (set! t-collect 0) (set! t-check 0)
          (refine-all hash1 live1 flag1 hash2 live2 flag2 iterator)
          ))
@@ -1181,7 +1185,7 @@
          (define keys-bw (hash-keys (vector-ref classes-bw step-bw)))
          (set! keys (sort-live keys))
          (set! keys-bw (sort-live-bw keys-bw))
-         (when debug
+         (when #t
                (for ([key keys])
                     (pretty-display `(key ,(entry-live key) ,(entry-flag key))))
                (pretty-display `(keys-bw ,step-bw ,keys-bw)))

stat.rkt

@@ -106,7 +106,7 @@
 	    (define info-file (format "~a/best.info" dir))
 	    (define-values (cost-r len-r time-r id-r) (get-best-info dir))
 
-	    (when (or (not cost-r) (< cost cost-r))
+	    (when (or (not cost-r) (<= cost cost-r))
 		(pretty-display "FOUND!!!")
 		(with-output-to-file #:exists 'append (format "~a/summary" dir)
 		  (thunk