CHB: add error-enabled assign commands

sipma · sipma · commit db5eae8b18ac · 2025-01-02T10:40:39.000-08:00
diff --git a/CodeHawk/CH/chutil/cHTraceResult.ml b/CodeHawk/CH/chutil/cHTraceResult.ml
@@ -61,6 +61,25 @@ let tmap2
   | Error e1, Error e2 -> Error (msg1 :: msg2 :: (e1 @ e2))
 
 
+let tmap3
+      ?(msg1="")
+      ?(msg2="")
+      ?(msg3="")
+      (f: 'a -> 'b -> 'c -> 'd)
+      (r1: 'a traceresult)
+      (r2: 'b traceresult)
+      (r3: 'c traceresult): 'd traceresult =
+  match r1, r2, r3 with
+  | Ok v1, Ok v2, Ok v3 -> Ok (f v1 v2 v3)
+  | Error e1, Ok _, Ok _ -> Error (msg1 :: e1)
+  | Ok _, Error e2, Ok _ -> Error (msg2 :: e2)
+  | Ok _, Ok _, Error e3 -> Error (msg3 :: e3)
+  | Error e1, Error e2, Ok _ -> Error (msg1 :: msg2 :: (e1 @ e2))
+  | Error e1, Ok _, Error e3 -> Error (msg1 :: msg3 :: (e1 @ e3))
+  | Ok _, Error e2, Error e3 -> Error (msg2 :: msg3 :: (e2 @ e3))
+  | Error e1, Error e2, Error e3 -> Error (msg1 :: msg2 :: msg3 :: (e1 @ e2 @ e3))
+
+
 let tbind ?(msg="") (f: 'a -> 'c traceresult) (r: 'a traceresult) =
   match r with
   | Ok v -> f v
diff --git a/CodeHawk/CH/chutil/cHTraceResult.mli b/CodeHawk/CH/chutil/cHTraceResult.mli
@@ -65,6 +65,20 @@ val tmap2:
   -> 'c traceresult
 
 
+(** [tmap3 f r1 r2 r3] is [Ok (f v1 v2 v3)] if [r1] is [Ok v1] and [r2] is
+    [Ok v2] and [r3] is [Ok v3]; otherwise it returns an [Error] appending
+    the messages corresponding to the error value as appropriate.*)
+val tmap3:
+  ?msg1:string
+  -> ?msg2:string
+  -> ?msg3:string
+  -> ('a -> 'b -> 'c -> 'd)
+  -> 'a traceresult
+  -> 'b traceresult
+  -> 'c traceresult
+  -> 'd traceresult
+
+
 (** [tfold ~ok ~error r] is [ok v] if [r] is [Ok v] and [error e] if [r] is
     [Error e].*)
 val tfold: ok:('a -> 'c) -> error:(string list -> 'c) -> 'a traceresult -> 'c
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -766,6 +766,31 @@ object (self)
    * resolve and save ScaledReg (cpureg1, cpureg2, 1, offset)   (memrefs2)
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
 
+  method get_memory_variable_varoffset
+           ?(size=4) (var1: variable_t) (var2: variable_t) (offset: numerical_t):
+           variable_t traceresult =
+    let addr = XOp (XPlus, [XVar var1; XVar var2]) in
+    let addr = XOp (XPlus, [addr; num_constant_expr offset]) in
+    let address = simplify_xpr (self#inv#rewrite_expr addr) in
+    let (memref_r, memoff_r) = self#decompose_memaddr address in
+    tbind
+      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+      (fun memref ->
+        if memref#is_global_reference then
+          tbind
+            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
+            (fun memoff ->
+              self#env#mk_global_variable ~size (get_total_constant_offset memoff))
+            memoff_r
+        else
+          tmap
+            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+            (fun memoff ->
+              (self#env#mk_memory_variable
+                 memref (get_total_constant_offset memoff)))
+            memoff_r)
+      memref_r
+
   method get_memory_variable_2
            ?(size=4) (var1:variable_t) (var2:variable_t) (offset:numerical_t) =
     let _ = track_function
@@ -792,6 +817,42 @@ object (self)
    * resolve and save ScaledReg (cpureg1, cpureg2, s, offset)  (memrefs3)
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
 
+  method get_memory_variable_scaledoffset
+           ?(size=4)
+           (base: variable_t)
+           (index: variable_t)
+           (scale: int)
+           (offset: numerical_t): variable_t traceresult =
+    let indexexpr =
+      if self#inv#is_constant index then
+        num_constant_expr (self#inv#get_constant index)
+      else
+        XVar index in
+    let addr = XOp (XPlus, [XVar base; num_constant_expr offset]) in
+    let addr = self#inv#rewrite_expr addr in
+    let addr =
+      XOp (XPlus,
+           [addr; XOp (XMult, [int_constant_expr scale; indexexpr])]) in
+    let address = simplify_xpr (self#inv#rewrite_expr addr) in
+    let (memref_r, memoff_r) = self#decompose_memaddr address in
+    tbind
+      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+      (fun memref ->
+        if memref#is_global_reference then
+          tbind
+            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
+            (fun memoff ->
+              self#env#mk_global_variable ~size (get_total_constant_offset memoff))
+            memoff_r
+        else
+          tmap
+            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+            (fun memoff ->
+              (self#env#mk_memory_variable
+                 memref (get_total_constant_offset memoff)))
+            memoff_r)
+      memref_r
+
   method get_memory_variable_3
            ?(size=4)
            (base:variable_t)
@@ -1528,6 +1589,65 @@ object (self)
      (List.length vars) > 0
      && List.for_all is_fixed_type (variables_in_expr x)
 
+   method get_assign_commands_r
+            ?(signed=false)
+            ?(size=4)
+            (lhs_r: variable_t traceresult)
+            (rhs_r: xpr_t traceresult): cmd_t list =
+     if Result.is_error lhs_r then
+       let (cmds, op_args) =
+         TR.tfold
+           ~ok:(fun rhs ->
+             let reqN () = self#env#mk_num_temp in
+             let reqC = self#env#request_num_constant in
+             let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
+             (rhscmds, get_rhs_op_args rhs_c))
+           ~error:(fun e ->
+             begin
+               log_error_result
+                 ~tag:("assignment lhs unknown")
+                 ~msg:(p2s self#l#toPretty)
+                 __FILE__ __LINE__ e;
+               ([], [])
+             end)
+           rhs_r in
+       cmds @ [OPERATION ({op_name = unknown_write_symbol; op_args = op_args})]
+
+     else if Result.is_error rhs_r then
+       let lhs = TR.tget_ok lhs_r in
+       [ABSTRACT_VARS [lhs]]
+
+     else
+       let lhs = TR.tget_ok lhs_r in
+       let rhs = TR.tget_ok rhs_r in
+       let rhs = simplify_xpr (self#inv#rewrite_expr rhs) in
+       let rhs =
+         if not signed then
+           match rhs with
+           | XConst (IntConst n) ->
+              let n =
+                match size with
+                | 1 -> n#modulo numerical_e8
+                | 2 -> n#modulo numerical_e16
+                | 4 -> n#modulo numerical_e32
+                | _ -> n in
+              num_constant_expr n
+           | _ -> rhs
+         else
+           rhs in
+
+       let rhs =
+         (* if rhs is a composite symbolic expression, create a new variable
+            for it *)
+         if self#is_composite_symbolic_value rhs then
+           XVar (self#env#mk_symbolic_value rhs)
+         else
+           rhs in
+       let reqN () = self#env#mk_num_temp in
+       let reqC = self#env#request_num_constant in
+       let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
+       rhscmds @ [ASSIGN_NUM (lhs, rhs_c)]
+
    (* Note: recording of loads and stores is performed by the different
       architectures directly in FnXXXDictionary.*)
    method get_assign_commands
@@ -1753,6 +1873,18 @@ object (self)
             (x2s size) (btype_to_string vtype) in
      [ABSTRACT_VARS [lhs]]
 
+   method get_abstract_commands_r (lhs_r: variable_t traceresult): cmd_t list =
+     TR.tfold
+       ~ok:(fun lhs -> [ABSTRACT_VARS [lhs]])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"lhs not abstracted" ~msg:(p2s self#l#toPretty)
+             __FILE__ __LINE__ e;
+           []
+         end)
+       lhs_r
+
    method get_ssa_abstract_commands (reg: register_t) () =
      let regvar = self#env#mk_register_variable reg in
      (regvar, [ABSTRACT_VARS [regvar]])
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -5785,11 +5785,26 @@ class type floc_int =
              -> numerical_t
              -> variable_t
 
+    method get_memory_variable_varoffset:
+             ?size:int
+             -> variable_t
+             -> variable_t
+             -> numerical_t
+             -> variable_t traceresult
+
     (* returns the memory reference corresponding to a base and index
        variable plus offset *)
     method get_memory_variable_2:
              ?size:int -> variable_t -> variable_t -> numerical_t -> variable_t
 
+    method get_memory_variable_scaledoffset:
+             ?size:int
+             -> variable_t
+             -> variable_t
+             -> int
+             -> numerical_t
+             -> variable_t traceresult
+
     (* returns the memory reference corresponding to a base and scaled index
        variable plus offset *)
     method get_memory_variable_3:
@@ -5940,7 +5955,7 @@ class type floc_int =
 
     (** {2 Assignments} *)
 
-    (** [floc#get_assign_commands var ~size ~vtype xpr] returns the CHIF commands
+    (** [get_assign_commands var ~size ~vtype xpr] returns the CHIF commands
         representing the assignment [var := xpr].
 
         If [size] is not None and the left-hand side [var] is externally observable
@@ -5949,6 +5964,8 @@ class type floc_int =
 
         If [vtype] is known type facts are added for both [var] and [xpr] for this
         instruction.
+
+        Deprecated. To be replaced with [get_assign_commands_r].
      *)
     method get_assign_commands:
              variable_t
@@ -5957,13 +5974,31 @@ class type floc_int =
              -> xpr_t
              -> cmd_t list
 
-    (** [floc#get_ssa_assign_commands reg ~vtype xpr] creates an ssa-register
+    (** [get_assign_commands_r var xpr] returns the CHIF commands representing
+        the assignment [var := xpr].
+
+        If [size] of [var] (in bytes) is different from the default value 4,
+        the value of [xpr] is restricted to the given width if the value is a
+        numerical constant.*)
+    method get_assign_commands_r:
+             ?signed:bool
+             -> ?size:int
+             -> variable_t traceresult
+             -> xpr_t traceresult
+             -> cmd_t list
+
+
+    (** [get_ssa_assign_commands reg ~vtype xpr] creates an ssa-register
         variable [ssavar] for the current context address and returns
         a tuple of the register-variable, and the CHIF commands representing
         the assignment and assert-equal:
         {[ reg := xpr
            assert (reg = ssavar)
-        ]} *)
+        ]}
+
+        Deprecated. All ssa variables have been moved to the python front end.
+        To be replaced with [get_assign_commands_r].
+     *)
     method get_ssa_assign_commands:
              register_t
              -> ?vtype:btype_t
@@ -5977,14 +6012,19 @@ class type floc_int =
 
     (** {2 Variable abstraction}*)
 
+    method get_abstract_commands_r: variable_t traceresult -> cmd_t list
+
     (* returns the CHIF code associated with an abstraction of variables *)
     method get_abstract_commands:
              variable_t -> ?size:xpr_t -> ?vtype:btype_t -> unit -> cmd_t list
 
     (** floc#[get_ssa_abstract_commands reg ()] creates an ssa-register
         variable [ssavar] for the current context address and returns a tuple of
         the register-variable and the CHIF commands representing the assignment
-        {[ reg := ssavar ]}*)
+        {[ reg := ssavar ]}
+
+        Deprecated. To be replaced with [get_abstract_commands_r]
+     *)
     method get_ssa_abstract_commands:
              register_t -> unit -> (variable_t * cmd_t list)
 
