stage

harp-lab · Mar 27, 2023 · 7349087 · 7349087
1 parent 9be1bf8
commit 7349087
Showing 1 changed file with 127 additions and 67 deletions.
diff --git a/evaluation/points-to-llvm /aa.slog b/evaluation/points-to-llvm /aa.slog
@@ -528,6 +528,10 @@
  -->
     (deref (variable var) k c val)]
 
+; state
+[(state to) <-- (step-to from to)]
+[(stuck-state s) <-- (state s) (~ step-to s _)]
+
 ; Injection 
 ; start at main
 (entry-point "</home/stargazermiao/workspace/PL/cclyzerpp/test/c/ex_simple.bc>:main:[basicblock]%2")
@@ -561,95 +565,124 @@
 
 ; ret
 [(eval [(ret x) rst ...] k c) --> (do-eval x k c)]
-; [(eval [(ret x) rst ...] (local-k cur-k prev-ctx prev-k) (ctx ctx0 ctx1 prev-func cur-func))
-;  -->
-    (step-to
-        ?(eval [(ret x) rst ...] (local-k cur-k prev-ctx prev-k) (ctx ctx0 ctx1 prev-func cur-func))
-        (eval-ret-to-call
-            {aeval x (local-k cur-k prev-ctx prev-k) (ctx ctx0 ctx1 prev-func cur-func)}
-            cur-k prev-k
-            (ctx prev-ctx ctx0 ctx1 prev-func)))
-            ; ]
-
-[(eval [(ret-void) rst ...]
-    (local-k [callee rst ...] prev-ctx prev-k)
-    (ctx ctx0 ctx1 prev-func cur-func))
- -->
-    (eval [rst ...] prev-k (ctx prev-ctx ctx0 ctx1 prev-func))]
+(step-to
+    ?(eval [(ret x) rst ...] (local-k cur-k prev-ctx prev-k) (ctx ctx0 ctx1 prev-func cur-func))
+    ; -->
+    (eval-ret-to-call
+        {aeval x (local-k cur-k prev-ctx prev-k) (ctx ctx0 ctx1 prev-func cur-func)}
+        cur-k prev-k
+        (ctx prev-ctx ctx0 ctx1 prev-func)))
+
+(step-to
+    ?(eval [(ret-void) rst ...]
+        (local-k [callee rst ...] prev-ctx prev-k)
+        (ctx ctx0 ctx1 prev-func cur-func))
+    ; -->
+    (eval [rst ...] prev-k (ctx prev-ctx ctx0 ctx1 prev-func)))
 
 ; br
-[(eval [(br-uncond next-bb) rst ...] k c)
- -->
-    (eval {bb-instrs next-bb} k c)]
+(step-to
+    ?(eval [(br-uncond next-bb) rst ...] k c)
+    ; -->
+    (eval {bb-instrs next-bb} k c))
 ; branch to both, maybe we can check cond value here
-[(eval [(br-cond v-cond lt lf) rst ...] k c)
- -->
-    (eval {bb-instrs lt} k c)
-    (eval {bb-instrs lf} k c)]
+(step-to
+    ?(eval [(br-cond v-cond lt lf) rst ...] k c)
+    ; -->
+    (eval {bb-instrs lt} k c))
+(step-to
+    ?(eval [(br-cond v-cond lt lf) rst ...] k c)
+    ; -->
+    (eval {bb-instrs lf} k c))
 
 ; switch
 ; step to a helper
-[(eval [(switch cond-v cases default-l) rst ...] k c)
- -->
-    (eval-switch-cases cond-v cases default-l k c)]
-[(eval-switch-cases cond-v [(case const next-l) c-rsts ...] default-l k c)
- -->
+(step-to
+    ?(eval [(switch cond-v cases default-l) rst ...] k c)
+    ; -->
+    (eval-switch-cases cond-v cases default-l k c))
+(step-to
+    ?(eval-switch-cases cond-v [(case const next-l) c-rsts ...] default-l k c)
+    ; -->
     ;; maybe add value check here
-    (eval next-l {bb-instrs next-l} k c)
-    (eval-switch-cases cond-v [c-rsts ...] default-l k c)]
-[(eval-switch-cases cond-v [] default-l k c)
- -->
-    (eval default-l {bb-instrs default-l} k c)]
+    (eval next-l {bb-instrs next-l} k c))
+(step-to
+    ?(eval-switch-cases cond-v [(case const next-l) c-rsts ...] default-l k c)
+    ; -->
+    ;; maybe add value check here
+    (eval-switch-cases cond-v [c-rsts ...] default-l k c))
+
+(step-to
+    ?(eval-switch-cases cond-v [] default-l k c)
+    ; -->
+    (eval default-l {bb-instrs default-l} k c))
 
 ; binary operation
-[(eval [(binary-op bop lhs op1 op2) rst ...] k c)
-  -->
-    (do-aeval op1 k c) (do-aeval op2 k c)]
+(step-to
+    ?(eval [(binary-op bop lhs op1 op2) rst ...] k c)
+    ; -->
+    (do-aeval op1 k c) (do-aeval op2 k c))
 [(eval [(binary-op bop lhs op1 op2) rst ...] k c)
  -->
     (dataflow {aeval op1 k c} (register lhs c))
-    (dataflow {aeval op2 k c} (register lhs c))
-    ; (heap (register lhs k) (binary-op-val bop v1 v2))
-    (eval [rst ...] k c)]
+    (dataflow {aeval op2 k c} (register lhs c))]
+(step-to
+    ?(eval [(binary-op bop lhs op1 op2) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; alloca
 [(eval [(alloca lhs n) rst ...] k c)
  -->
-    (eval [rst ...] k c)
     (dataflow (addr lhs c) (register lhs c))
     (dataflow (nil) (addr lhs c))]
+(step-to
+    ?(eval [(alloca lhs n) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; load
 [(eval [(load lhs ptr) rst ...] k c) --> (do-deref ptr k c)]
 [(eval [(load lhs ptr) rst ...] k c)
  -->
-    (dataflow {deref ptr k c} (register lhs c))
-    (eval [rst ...] k c)]
+    (dataflow {deref ptr k c} (register lhs c))]
+(step-to
+    ?(eval [(load lhs ptr) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; store
 [(eval [(store v ptr) rst ...] k c)
  -->
-    (do-aeval ptr k c)
-    (do-aeval v k c)]
+    (do-aeval ptr k c) (do-aeval v k c)]
 [(eval [(store v ptr) rst ...] k c)
  -->
-    (dataflow {aeval v k c} {aeval ptr k c})
-    (eval [rst ...] k c)]
+    (dataflow {aeval v k c} {aeval ptr k c})]
+(step-to
+    ?(eval [(store v ptr) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; GEP
 ; can base be a int?
 [(eval [(getelementptr lhs base indices) rst ...] k c) --> (do-deref base k c)]
 [(eval [(getelementptr lhs base indices) rst ...] k c)
  -->
-    (dataflow {deref base k c} (register lhs c))
-    (eval [rst ...] k c)]
+    (dataflow {deref base k c} (register lhs c))]
+(step-to
+    ?(eval [(getelementptr lhs base indices) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; type conversion
 [(eval [(convert _ lhs op) rst ...] k c) --> (do-aeval op k c)]
 [(eval [(convert _ lhs op) rst ...] k c)
  -->
-    (dataflow {aeval op k c} lhs)
-    (eval [rst ...] k c)]
+    (dataflow {aeval op k c} lhs)]
+(step-to
+    ?(eval [(convert _ lhs op) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; icmp/fcmp
 [(eval [(icmp lhs cond-v op1 op2) rst ...] k c)
@@ -658,8 +691,11 @@
 [(eval [(icmp lhs cond-v op1 op2) rst ...] k c)
  -->
     (dataflow {aeval op1 k c} (register lhs c))
-    (dataflow {aeval op2 k c} (register lhs c))
-    (eval [rst ...] k c)]
+    (dataflow {aeval op2 k c} (register lhs c))]
+(step-to
+    ?(eval [(icmp lhs cond-v op1 op2) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; phi
 [(eval [(phi lhs pairs) rst ...] k c)
@@ -671,8 +707,11 @@
 [(eval-phi-pairs lhs [(phi-value-pair l op) prst ...] rst k c) --> (do-aeval op k c)]
 [(eval-phi-pairs lhs [(phi-value-pair l op) prst ...] rst k c)
  -->
-    (dataflow {aeval op k c} (register lhs c))
-    (eval-phi-pairs lhs [prst ...] rst k c)]
+    (dataflow {aeval op k c} (register lhs c))]
+(step-to
+    ?(eval-phi-pairs lhs [(phi-value-pair l op) prst ...] rst k c)
+    ; -->
+    (eval-phi-pairs lhs [prst ...] rst k c))
 
 ; select
 [(eval [(select lhs cond-v op1 op2) rst ...] k c)
@@ -681,55 +720,76 @@
 [(eval [(select lhs cond-v op1 op2) rst ...] k c)
  -->
     (dataflow {aeval op1 k c} (register lhs c))
-    (dataflow {aeval op2 k c} (register lhs c))
-    (eval [rst ...] k c)]
+    (dataflow {aeval op2 k c} (register lhs c))]
+(step-to
+    ?(eval [(select lhs cond-v op1 op2) rst ...] k c)
+    ; -->
+    (eval [rst ...] k c))
 
 ; call
 ; only directed call
 ; internal call
 [(eval [(call lhs (constant fconst) args) rst ...] k (ctx ctx0 ctx1 ctx2 cur-func))
  (func {fconst-funcdecl fconst})
  -->
-    (eval-func-args 0 fconst args [(call lhs (constant fconst) args) rst ...]
-        k (local-k [(call lhs (constant fconst) args) rst ...] ctx0 k)
-        (ctx ctx0 ctx1 ctx2 cur-func) (ctx ctx1 ctx2 cur-func fconst))]
-[(eval-func-args i func [] k new-k c new-c)
- -->
-    (eval {bb-instrs {func-entry-bb func}} new-k new-c)]
+    (step-to
+        (eval [(call lhs (constant fconst) args) rst ...] k (ctx ctx0 ctx1 ctx2 cur-func))
+        ; -->
+        (eval-func-args 0 fconst args [(call lhs (constant fconst) args) rst ...]
+            k (local-k [(call lhs (constant fconst) args) rst ...] ctx0 k)
+            (ctx ctx0 ctx1 ctx2 cur-func) (ctx ctx1 ctx2 cur-func fconst)))]
+(step-to 
+    ?(eval-func-args i func [] k new-k c new-c)
+    ; -->
+    (eval {bb-instrs {func-entry-bb func}} new-k new-c))
 [(eval-func-args i func [arg arst ...] k new-k c new-c) --> (do-aeval arg k c)]
 [(eval-func-args i func [arg arst ...] k new-k c new-c)
  (fconst-params func i param)
  -->
     (dataflow {aeval arg k c} (register param new-c))
-    (eval-func-args {+ 1 i} func [arst ...] k new-k c new-c)]
+    (step-to
+        (eval-func-args i func [arg arst ...] k new-k c new-c)
+        ; -->
+        (eval-func-args {+ 1 i} func [arst ...] k new-k c new-c))]
 ; external call
 [(eval [(call lhs (constant fconst) args) rst ...] k c)
  (fconst-ret-void fconst)
  (fconst-funcdecl fconst fdecl)
  (external-funcdecl fdecl)
  -->
-    (eval [rst ...] k c)]
+    (step-to
+        (eval [(call lhs (constant fconst) args) rst ...] k c)
+        ; -->
+        (eval [rst ...] k c))]
 [(eval [(call lhs (constant fconst) args) rst ...] k c)
  (fconst-ret-val fconst)
  (fconst-funcdecl fconst fdecl)
  (external-funcdecl fdecl)
  -->
     (dataflow (unknown) (register lhs k))
-    (eval [rst ...] k c)]
+    (step-to
+        (eval [(call lhs (constant fconst) args) rst ...] k c)
+        ; -->
+        (eval [rst ...] k c))]
 [(eval [(call lhs (constant fconst) args) rst ...] k c)
  (fconst-ret-ptr fconst)
  (fconst-funcdecl fconst fdecl)
  (external-funcdecl fdecl)
  -->
     (dataflow (unknown) (addr lhs c))
     (dataflow (addr lhs c) (register lhs c))
-    (eval [rst ...] k c)]
+    (step-to
+        (eval [(call lhs (constant fconst) args) rst ...] k c)
+        ; -->
+        (eval [rst ...] k c))]
 
 ; returned
 [(eval-ret-to-call ret-v [(call lhs (constant func) args) rst ...] k c)
  -->
-    (dataflow ret-v (register lhs c))
-    (eval [rst ...] k c)]
+    (dataflow ret-v (register lhs c))]
+(step-to
+    ?(eval-ret-to-call ret-v [(call lhs (constant func) args) rst ...] k c)
+    (eval [rst ...] k c))
 
 
 ;; (eval [instr ...] [contour ...] prev-bb (kaddr [instr ...] prev-kaddr))