CHB: improved handling of sideeffect values

Author: sipma

CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml

@@ -297,14 +297,15 @@ object (self)
        XPOBlockWrite (ty, addr, size)) ->
        (match self#termev#xpr_local_stack_address addr with
         | Some offset ->
+           let numoffset = (CHNumerical.mkNumerical offset)#neg in
            let csize =
              match size with
              | XConst (IntConst n) -> Some n#toInt
              | _ ->
                 TR.tfold_default (fun s -> Some s) None (size_of_btype ty) in
            let sevalue =
-             self#finfo#env#mk_side_effect_value
-               self#loc#ci (bterm_to_string taddr) in
+             self#finfo#env#mk_stack_sideeffect_value
+               ~btype:(Some ty) self#loc#ci numoffset (bterm_to_string taddr) in
            self#finfo#stackframe#add_block_write
              ~offset:(-offset)
              ~size:csize

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -228,6 +228,22 @@ object (self)
 end
 
 
+class default_bterm_evaluator_t
+        (finfo: function_info_int)
+        (_callargs: (fts_parameter_t * xpr_t) list): bterm_evaluator_int =
+object
+
+  method finfo = finfo
+  method bterm_xpr (_t: bterm_t) = None
+  method xpr_local_stack_address (_x: xpr_t) = None
+  method bterm_stack_address (_t: bterm_t) = None
+  method constant_bterm (_t: bterm_t) = None
+
+end
+
+let default_bterm_evaluator = new default_bterm_evaluator_t
+
+
 class arm_bterm_evaluator_t
         (finfo: function_info_int)
         (callargs: (fts_parameter_t * xpr_t) list): bterm_evaluator_int =
@@ -2725,12 +2741,14 @@ object (self)
        end
      | _ -> ()
 
-   method private get_sideeffect_assign (side_effect: xxpredicate_t) =
+   method private get_sideeffect_assign
+                    (termev: bterm_evaluator_int) (side_effect: xxpredicate_t) =
      let msg =
        LBLOCK [
            self#l#toPretty; STR ": "; xxpredicate_to_pretty side_effect] in
-     match side_effect with
-     | XXBlockWrite (ty, dest, size) ->
+     let xpo = BCHXPOPredicate.xxp_to_xpo_predicate termev self#l side_effect in
+     match (side_effect, xpo) with
+     | (XXBlockWrite (_, dest, size), XPOBlockWrite (ty, adest, _)) ->
        let get_index_size k =
 	 match get_size_of_type ty with
 	 | Ok s -> num_constant_expr (k#mult (mkNumerical s))
@@ -2774,7 +2792,13 @@ object (self)
                     end)
                   (numerical_to_doubleword n)
 	     | _ ->
-	        self#env#mk_side_effect_value self#cia (bterm_to_string dest) in
+                (match termev#xpr_local_stack_address adest with
+                 | Some offset ->
+                    let numoffset = (CHNumerical.mkNumerical offset)#neg in
+                    self#env#mk_stack_sideeffect_value
+                      ~btype:(Some ty) self#cia numoffset (bterm_to_string dest)
+                 | _ ->
+	            self#env#mk_side_effect_value self#cia (bterm_to_string dest)) in
 	   let seAssign =
              let _ =
                chlog#add
@@ -2799,7 +2823,7 @@ object (self)
               []
 	    end
        end
-     | XXStartsThread (sa, _pars) ->
+     | (XXStartsThread (sa, _pars), _) ->
        let _ =
 	 match self#evaluate_summary_term sa self#env#mk_num_temp with
 	 | XConst (IntConst n) ->
@@ -2825,8 +2849,9 @@ object (self)
    method private record_precondition_effects (sem:function_semantics_t) =
      List.iter self#record_precondition_effect sem.fsem_pre
 
-   method get_sideeffect_assigns  (sem:function_semantics_t) =
-     List.concat (List.map self#get_sideeffect_assign sem.fsem_sideeffects)
+   method get_sideeffect_assigns
+            (termev: bterm_evaluator_int) (sem:function_semantics_t) =
+     List.concat (List.map (self#get_sideeffect_assign termev) sem.fsem_sideeffects)
 
    (* Records reads of global memory *)
    method private record_memory_reads (pres:xxpredicate_t list) =
@@ -2896,7 +2921,8 @@ object (self)
 
      (* ------------------------------------------------- assign side effects *)
      let sideEffectAssigns =
-	 self#get_sideeffect_assigns self#get_call_target#get_semantics  in
+       let termev = default_bterm_evaluator self#f [] in
+	 self#get_sideeffect_assigns termev self#get_call_target#get_semantics  in
      let _ =
 	 self#record_precondition_effects self#get_call_target#get_semantics in
 
@@ -3032,7 +3058,7 @@ object (self)
          List.filter self#env#is_global_variable self#env#get_variables in
        [ABSTRACT_VARS globals] in
      let sideeffect_assigns =
-       self#get_sideeffect_assigns self#get_call_target#get_semantics in
+       self#get_sideeffect_assigns termev self#get_call_target#get_semantics in
      let _ =
        self#record_memory_reads self#get_call_target#get_semantics.fsem_pre in
      let defClobbered = List.map (fun r -> (ARMRegister r)) arm_temporaries in

CodeHawk/CHB/bchlib/bCHFloc.mli

@@ -6,7 +6,7 @@
  
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2021 Henny Sipma
-   Copyright (c) 2022-2023 Aarno Labs LLC
+   Copyright (c) 2022-2025 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -27,6 +27,9 @@
    SOFTWARE.
    ============================================================================= *)
 
+(* xprlib *)
+open XprTypes
+
 (* bchlib *)
 open BCHLibTypes
 
@@ -60,3 +63,5 @@ val get_i_floc:
   -> floc_int
 
 
+val default_bterm_evaluator:
+  function_info_int -> (fts_parameter_t * xpr_t) list -> bterm_evaluator_int

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -995,12 +995,18 @@ object (self)
     self#mk_variable (varmgr#make_calltarget_value tgt)
 
   method mk_global_sideeffect_value
-           (iaddr: ctxt_iaddress_t) (gaddr: doubleword_int) (arg: string) =
-    self#mk_variable (varmgr#make_global_sideeffect_value iaddr arg gaddr)
+           ?(btype=None)
+           (iaddr: ctxt_iaddress_t)
+           (gaddr: doubleword_int)
+           (arg: string) =
+    self#mk_variable (varmgr#make_global_sideeffect_value ~btype iaddr arg gaddr)
 
   method mk_stack_sideeffect_value
-           (iaddr: ctxt_iaddress_t) (offset: numerical_t) (arg: string) =
-    self#mk_variable (varmgr#make_stack_sideeffect_value iaddr arg offset)
+           ?(btype=None)
+           (iaddr: ctxt_iaddress_t)
+           (offset: numerical_t)
+           (arg: string) =
+    self#mk_variable (varmgr#make_stack_sideeffect_value ~btype iaddr arg offset)
 
   method mk_side_effect_value (iaddr:ctxt_iaddress_t) (arg:string) =
     self#mk_variable (varmgr#make_side_effect_value iaddr "sev" arg)

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3563,6 +3563,7 @@ and constant_value_variable_t =
   | SideEffectValue of
       ctxt_iaddress_t                    (* callsite *)
       * string                           (* name of parameter *)
+      * btype_t option                   (* type of value *)
       * sideeffect_argument_location_t   (* location of argument passed *)
   (** [SideEffectValue (iaddr, name, seloc] represents the value
   assigned by the callee at call site [iaddr] to the parameter with
@@ -3932,9 +3933,17 @@ object
   method make_function_pointer_value:
            string -> string -> ctxt_iaddress_t -> assembly_variable_int
   method make_global_sideeffect_value:
-           ctxt_iaddress_t -> string -> doubleword_int -> assembly_variable_int
+           ?btype:btype_t option
+           -> ctxt_iaddress_t
+           -> string
+           -> doubleword_int
+           -> assembly_variable_int
   method make_stack_sideeffect_value:
-           ctxt_iaddress_t -> string -> numerical_t -> assembly_variable_int
+           ?btype:btype_t option
+           -> ctxt_iaddress_t
+           -> string
+           -> numerical_t
+           -> assembly_variable_int
   method make_side_effect_value:
            ctxt_iaddress_t -> string -> string -> assembly_variable_int
   method make_field_value: string -> int -> string -> assembly_variable_int
@@ -4852,9 +4861,17 @@ class type function_environment_int =
     method mk_function_pointer_value:
              string -> string -> ctxt_iaddress_t -> variable_t
     method mk_global_sideeffect_value:
-             ctxt_iaddress_t -> doubleword_int -> string -> variable_t
+             ?btype:btype_t option
+             -> ctxt_iaddress_t
+             -> doubleword_int
+             -> string
+             -> variable_t
     method mk_stack_sideeffect_value:
-             ctxt_iaddress_t -> numerical_t -> string -> variable_t
+             ?btype:btype_t option
+             -> ctxt_iaddress_t
+             -> numerical_t
+             -> string
+             -> variable_t
     method mk_side_effect_value: ctxt_iaddress_t -> string -> variable_t
     method mk_field_value: string -> int -> string -> variable_t
     method mk_symbolic_value: xpr_t -> variable_t
@@ -6266,7 +6283,8 @@ class type floc_int =
     method get_conditional_assign_commands:
              xpr_t -> variable_t -> xpr_t -> cmd_t list
 
-    method get_sideeffect_assigns: function_semantics_t -> cmd_t list
+    method get_sideeffect_assigns:
+             bterm_evaluator_int -> function_semantics_t -> cmd_t list
 
     (** {2 Variable abstraction}*)
 

CodeHawk/CHB/bchlib/bCHVarDictionary.ml

@@ -91,6 +91,7 @@ object (self)
     tables <- [
       memory_base_table;
       memory_offset_table;
+      sideeffect_argument_location_table;
       assembly_variable_denotation_table;
       constant_value_variable_table;
       stack_access_table
@@ -243,9 +244,11 @@ object (self)
       | FunctionPointer (s1, s2, a) ->
          (tags @ [a], [bd#index_string s1; bd#index_string s2])
       | CallTargetValue t -> (tags, [id#index_call_target t])
-      | SideEffectValue  (a, name, seloc) ->
+      | SideEffectValue  (a, name, optty, seloc) ->
          (tags @  [a],
-          [bd#index_string name; self#index_sideeffect_argument_location seloc])
+          [bd#index_string name;
+           (match optty with Some ty -> bcd#index_typ ty | _ -> (-1));
+           self#index_sideeffect_argument_location seloc])
       | BridgeVariable (a,i) -> (tags @ [a], [i])
       | FieldValue (sname,offset,fname) ->
          (tags, [bd#index_string sname; offset; bd#index_string fname])
@@ -272,7 +275,10 @@ object (self)
     | "ct" -> CallTargetValue (id#get_call_target (a 0))
     | "se" ->
        SideEffectValue
-         (t 1, bd#get_string (a 0), self#get_sideeffect_argument_location (a 1))
+         (t 1,
+          bd#get_string (a 0),
+          (if (a 1) > 0 then Some (bcd#get_typ (a 1)) else None),
+          self#get_sideeffect_argument_location (a 2))
     | "bv" -> BridgeVariable (t 1, a 0)
     | "fv" -> FieldValue (bd#get_string (a 0), a 1, bd#get_string  (a 2))
     | "sv" -> SymbolicValue (xd#get_xpr (a 0))

CodeHawk/CHB/bchlib/bCHVariable.ml

@@ -121,7 +121,7 @@ object (self:'a)
              "staticstub_" ^ (function_stub_to_string fs)
 	  | AppTarget a -> "tgt_" ^ a#to_hex_string
 	  | _ -> "tgt_qq_")
-	| SideEffectValue (address,arg,_) -> "se_" ^ address ^ "_" ^ arg
+	| SideEffectValue (address, arg, _, _) -> "se_" ^ address ^ "_" ^ arg
 	| FieldValue (sname,offset,fname) ->
 	   sname ^ "." ^ fname ^ "_amp_" ^ (string_of_int offset)
         | SymbolicValue x -> "sv__" ^ (string_of_int (vard#xd#index_xpr x)) ^ "__sv"
@@ -191,6 +191,7 @@ object (self:'a)
          | TypeCastValue (_, _, ty, _) -> Some ty
          | SyscallErrorReturnValue _ -> None
          | CallTargetValue _ -> None
+         | SideEffectValue (_, _, Some ty, _) -> Some ty
          | SideEffectValue _ -> None
          | FieldValue _ -> None
          | SymbolicValue _ -> None
@@ -235,12 +236,12 @@ object (self:'a)
 
   method is_global_sideeffect =
     match denotation with
-    | AuxiliaryVariable (SideEffectValue (_, _, SEGlobal _)) -> true
+    | AuxiliaryVariable (SideEffectValue (_, _, _, SEGlobal _)) -> true
     | _ -> false
 
   method get_global_sideeffect_target_address: doubleword_result =
     match denotation with
-    | AuxiliaryVariable (SideEffectValue (_, _, SEGlobal dw)) -> Ok dw
+    | AuxiliaryVariable (SideEffectValue (_, _, _, SEGlobal dw)) -> Ok dw
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
               ^ "Variable is not a global sideeffect value: "
@@ -278,15 +279,15 @@ object (self:'a)
   method get_call_site: ctxt_iaddress_t traceresult =
     match denotation with
     | (AuxiliaryVariable (FunctionReturnValue a))
-    | (AuxiliaryVariable (SideEffectValue (a, _, _))) -> Ok a
+    | (AuxiliaryVariable (SideEffectValue (a, _, _, _))) -> Ok a
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
               ^ "Variable is not a function return value or sideeffect value: "
               ^ self#get_name]
 
   method get_se_argument_descriptor: string traceresult =
     match denotation with
-    | (AuxiliaryVariable (SideEffectValue (_, name, _))) -> Ok name
+    | (AuxiliaryVariable (SideEffectValue (_, name, _, _))) -> Ok name
     | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                   ^ "Variable is not a sideeffect value: " ^ self#get_name]
 
@@ -641,6 +642,7 @@ object (self)
                   | InitialRegisterValue (PowerSPRegister _, _)
                   | InitialMemoryValue _
                   | FunctionReturnValue _
+                  | SideEffectValue _
                   | TypeCastValue _ ->
                    Ok (memrefmgr#mk_basevar_reference v)
                 | _ ->
@@ -697,17 +699,23 @@ object (self)
     self#mk_variable (AuxiliaryVariable (CallTargetValue tgt))
 
   method make_global_sideeffect_value
-           (iaddr: ctxt_iaddress_t) (arg: string) (gaddr: doubleword_int) =
-    let sev = SideEffectValue (iaddr, arg, SEGlobal gaddr) in
+           ?(btype=None)
+           (iaddr: ctxt_iaddress_t)
+           (arg: string)
+           (gaddr: doubleword_int) =
+    let sev = SideEffectValue (iaddr, arg, btype, SEGlobal gaddr) in
     self#mk_variable (AuxiliaryVariable sev)
 
   method make_stack_sideeffect_value
-           (iaddr: ctxt_iaddress_t) (arg: string) (stackoffset: numerical_t) =
-    let sev = SideEffectValue (iaddr, arg, SEStack stackoffset) in
+           ?(btype=None)
+           (iaddr: ctxt_iaddress_t)
+           (arg: string)
+           (stackoffset: numerical_t) =
+    let sev = SideEffectValue (iaddr, arg, btype, SEStack stackoffset) in
     self#mk_variable (AuxiliaryVariable sev)
 
   method make_side_effect_value (iaddr:ctxt_iaddress_t) (descr: string) (arg:string) =
-    let sev = SideEffectValue (iaddr, arg, SEDescr descr) in
+    let sev = SideEffectValue (iaddr, arg, None, SEDescr descr) in
     self#mk_variable (AuxiliaryVariable sev)
 
   method make_field_value (sname:string) (offset:int) (fname:string) =

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250803"
-  ~date:"2025-08-03"
+  ~version:"0.6.0_20250804"
+  ~date:"2025-08-04"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibx86/bCHPredefinedUtil.ml

@@ -514,7 +514,8 @@ let get_esp_adjustment_assign (summary: function_summary_int) (floc: floc_int) =
 
 
 let get_side_effects summary floc =
-  floc#get_sideeffect_assigns summary#get_function_semantics
+  let termev = BCHFloc.default_bterm_evaluator floc#f [] in
+  floc#get_sideeffect_assigns termev summary#get_function_semantics
 
 
 class virtual predefined_callsemantics_base_t (md5hash:string) (instrs:int) =