improves semantics of some ITT instructions (BinaryAnalysisPlatform#1379

) 1) removes double assignments in moves 2) removes doubled gotos in pop, push, stm, and ldm
thestr4ng3r · Dec 2, 2021 · 47a614a · 47a614a
1 parent 71076d4
commit 47a614a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 7 deletions.
diff --git a/plugins/thumb/thumb_core.ml b/plugins/thumb/thumb_core.ml
@@ -166,7 +166,8 @@ module Make(CT : Theory.Core) = struct
       data@@[dst := CT.ite ~?cnd exp (var dst)]
 
 
-  let branch cnd t f =
-    data@@[CT.branch (holds cnd) (seq t) (seq f)]
+  let branch cnd t f = match cnd with
+    | `AL -> data [seq t]
+    | _ -> data@@[CT.branch (holds cnd) (seq t) (seq f)]
 
 end
diff --git a/plugins/thumb/thumb_mov.ml b/plugins/thumb/thumb_mov.ml
@@ -18,7 +18,6 @@ module Make(CT : Theory.Core) = struct
   let borrow_from_sub ~rn ~rm = bit (rn < rm)
 
   let movi8 rd x = it_set rd (const x) @@ fun v -> [
-      v := const x;
       nf := if Int.(x lsr 7 = 1) then bit1 else bit0;
       zf := if Int.(x = 0) then bit1 else bit0;
     ]
@@ -58,11 +57,9 @@ module Make(CT : Theory.Core) = struct
       vf := overflow_from_add (var r) (var rn) (var rm);
     ]
 
-  let addspi off =
-    it_set sp (var sp + const off) @@ fun _ -> []
+  let addspi off = sp <-? var sp + const off
 
-  let addrspi rd off =
-    it_set rd (var sp + const off) @@ fun _ -> []
+  let addrspi rd off = rd <-? var sp + const off
 
   let cmp x y r = [
     nf := msb (var r);