CHB: more expressive representation for side effect values

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -2761,14 +2761,17 @@ object (self)
 	   let rhs =
  	     match dest with
  	     | NumConstant n ->
-                log_tfold_default
-                  (mk_tracelog_spec
-                     ~tag:"get_sideeffect_assign:BlockWrite"
-                     (self#cia ^ ": constant: " ^ n#toString))
-                  (fun dw ->
-	            let argDescr = dw#to_hex_string in
-	            self#env#mk_side_effect_value self#cia ~global:true argDescr)
-                  (self#env#mk_side_effect_value self#cia (bterm_to_string dest))
+                TR.tfold
+                  ~ok:(fun dw ->
+                    self#env#mk_global_sideeffect_value self#cia dw "dest")
+                  ~error:(fun e ->
+                    begin
+                      log_error_result
+                        ~msg:(p2s (xxpredicate_to_pretty side_effect))
+                        ~tag:"get_sideeffect_assign"
+                        __FILE__ __LINE__ e;
+                      self#env#mk_side_effect_value self#cia "dest"
+                    end)
                   (numerical_to_doubleword n)
 	     | _ ->
 	        self#env#mk_side_effect_value self#cia (bterm_to_string dest) in

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -994,8 +994,16 @@ object (self)
   method mk_calltarget_value (tgt:call_target_t) =
     self#mk_variable (varmgr#make_calltarget_value tgt)
 
-  method mk_side_effect_value (iaddr:ctxt_iaddress_t) ?(global=false) (arg:string) =
-    self#mk_variable (varmgr#make_side_effect_value iaddr ~global arg)
+  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)
+
+  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)
+
+  method mk_side_effect_value (iaddr:ctxt_iaddress_t) (arg:string) =
+    self#mk_variable (varmgr#make_side_effect_value iaddr "sev" arg)
 
   method mk_field_value (sname:string) (offset:int) (fname:string) =
     self#mk_variable (varmgr#make_field_value sname offset fname)

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3477,6 +3477,12 @@ end
 
 (** {2 Assembly variable} *)
 
+type sideeffect_argument_location_t =
+  | SEGlobal of doubleword_int
+  | SEStack of numerical_t
+  | SEDescr of string                   (* default value, uninterpreted *)
+
+
 (** Assembly variable denotations.*)
 type assembly_variable_denotation_t =
   (* size (bytes) memory reference index *)
@@ -3555,11 +3561,11 @@ and constant_value_variable_t =
   | CallTargetValue of call_target_t
 
   | SideEffectValue of
-      ctxt_iaddress_t       (* callsite *)
-      * string              (* argument description *)
-      * bool                (* is-global address *)
-  (** [SideEffectValue (iaddr, name, is_global)] represents the value
-  assigned by the callee at call site [iaddr] to the argument with
+      ctxt_iaddress_t                    (* callsite *)
+      * string                           (* name of parameter *)
+      * 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
   name [name].*)
 
   | BridgeVariable of ctxt_iaddress_t * int      (* call site, argument index *)
@@ -3758,12 +3764,14 @@ class type vardictionary_int =
 
     method index_memory_offset: memory_offset_t -> int
     method index_memory_base: memory_base_t -> int
+    method index_sideeffect_argument_location: sideeffect_argument_location_t -> int
     method index_assembly_variable_denotation: assembly_variable_denotation_t -> int
     method index_constant_value_variable: constant_value_variable_t -> int
     method index_stack_access: stack_access_t -> int
 
     method get_memory_offset: int -> memory_offset_t
     method get_memory_base: int -> memory_base_t
+    method get_sideeffect_argument_location: int -> sideeffect_argument_location_t
     method get_assembly_variable_denotation: int -> assembly_variable_denotation_t
     method get_constant_value_variable: int -> constant_value_variable_t
 
@@ -3923,8 +3931,12 @@ object
   method make_calltarget_value: call_target_t -> assembly_variable_int
   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
+  method make_stack_sideeffect_value:
+           ctxt_iaddress_t -> string -> numerical_t -> assembly_variable_int
   method make_side_effect_value:
-           ctxt_iaddress_t -> ?global:bool -> string -> assembly_variable_int
+           ctxt_iaddress_t -> string -> string -> assembly_variable_int
   method make_field_value: string -> int -> string -> assembly_variable_int
 
   (** {2 Memory references}*)
@@ -4839,8 +4851,11 @@ class type function_environment_int =
     method mk_calltarget_value: call_target_t -> variable_t
     method mk_function_pointer_value:
              string -> string -> ctxt_iaddress_t -> variable_t
-    method mk_side_effect_value:
-             ctxt_iaddress_t -> ?global:bool-> string -> variable_t
+    method mk_global_sideeffect_value:
+             ctxt_iaddress_t -> doubleword_int -> string -> variable_t
+    method mk_stack_sideeffect_value:
+             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
     method mk_signed_symbolic_value: xpr_t -> int -> int -> variable_t

CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml

@@ -653,6 +653,25 @@ end
 let memory_offset_mcts: memory_offset_t mfts_int = new memory_offset_mcts_t
 
 
+class sideeffect_argument_location_mcts_t:[sideeffect_argument_location_t] mfts_int =
+object
+
+  inherit [sideeffect_argument_location_t] mcts_t "sideeffect_argument_location"
+
+  method !ts (s: sideeffect_argument_location_t) =
+    match s with
+    | SEGlobal _ -> "g"
+    | SEStack _ -> "s"
+    | SEDescr _ -> "d"
+
+  method !tags = ["d"; "g"; "s"]
+
+end
+
+let sideeffect_argument_location_mcts: sideeffect_argument_location_t mfts_int =
+  new sideeffect_argument_location_mcts_t
+
+
 class assembly_variable_denotation_mcts_t:[assembly_variable_denotation_t] mfts_int =
 object
 

CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli

@@ -5,7 +5,7 @@
    The MIT License (MIT)
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
-   Copyright (c) 2021-2024 Aarno Labs LLC
+   Copyright (c) 2021-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
@@ -96,6 +96,7 @@ val type_constraint_mcts: type_constraint_t mfts_int
 
 val memory_base_mcts: memory_base_t mfts_int
 val memory_offset_mcts: memory_offset_t mfts_int
+val sideeffect_argument_location_mcts: sideeffect_argument_location_t mfts_int
 val assembly_variable_denotation_mcts: assembly_variable_denotation_t mfts_int
 val constant_value_variable_mcts: constant_value_variable_t mfts_int
 val stack_access_mcts: stack_access_t mfts_int

CodeHawk/CHB/bchlib/bCHVarDictionary.ml

@@ -44,6 +44,8 @@ open BCHBasicTypes
 open BCHLibTypes
 open BCHSumTypeSerializer
 
+module TR = CHTraceResult
+
 
 let bcd = BCHBCDictionary.bcdictionary
 let bd = BCHDictionary.bdictionary
@@ -74,6 +76,8 @@ object (self)
   val xd = xd
   val memory_base_table = mk_index_table "memory-base-table"
   val memory_offset_table = mk_index_table "memory-offset-table"
+  val sideeffect_argument_location_table =
+    mk_index_table "sideeffect-argument-location-table"
   val assembly_variable_denotation_table =
     mk_index_table "assembly-variable-denotation-table"
   val constant_value_variable_table =
@@ -172,6 +176,38 @@ object (self)
     | "u" -> UnknownOffset
     | s -> raise_tag_error name s memory_offset_mcts#tags
 
+  method index_sideeffect_argument_location (s: sideeffect_argument_location_t) =
+    let tags = [sideeffect_argument_location_mcts#ts s] in
+    let key = match s with
+      | SEGlobal a -> (tags @ [a#to_hex_string], [])
+      | SEStack s -> (tags @ [s#toString], [])
+      | SEDescr d -> (tags @ [d], []) in
+    sideeffect_argument_location_table#add key
+
+  method get_sideeffect_argument_location (index: int) =
+    let name = "sideeffect_location" in
+    let (tags, _) = sideeffect_argument_location_table#retrieve index in
+    let t = t name tags in
+    match (t 0) with
+    | "d" -> SEDescr (t 1)
+    | "g" ->
+       TR.tfold
+         ~ok:(fun dw -> SEGlobal dw)
+         ~error:(fun e ->
+           begin
+             log_error_result
+               ~msg:"get_sideeffect_location"
+               ~tag:"vardictionary error"
+               __FILE__ __LINE__ e;
+             raise
+               (BCH_failure
+                  (LBLOCK [STR "Vardictionary: get_sideeffect_location: ";
+                           STR (String.concat "; " e)]))
+           end)
+         (BCHDoubleword.string_to_doubleword (t 1))
+    | "s" -> SEStack (CHNumerical.mkNumericalFromString (t 1))
+    | s -> raise_tag_error name s sideeffect_argument_location_mcts#tags
+
   method index_assembly_variable_denotation (v:assembly_variable_denotation_t) =
     let tags = [ assembly_variable_denotation_mcts#ts v ] in
     let key = match v with
@@ -182,7 +218,7 @@ object (self)
     assembly_variable_denotation_table#add key
 
   method get_assembly_variable_denotation (index:int) =
-    let name =  "assembly_variable_denotation" in
+    let name = "assembly_variable_denotation" in
     let (tags,args) = assembly_variable_denotation_table#retrieve index in
     let t = t name tags in
     let a = a name args in
@@ -207,8 +243,9 @@ 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, isglobal) ->
-         (tags @  [a ], [bd#index_string name; (if isglobal then 1 else 0)])
+      | SideEffectValue  (a, name, seloc) ->
+         (tags @  [a],
+          [bd#index_string name; 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])
@@ -233,7 +270,9 @@ object (self)
     | "ev" -> SyscallErrorReturnValue (t 1)
     | "fp" -> FunctionPointer (bd#get_string (a 0), bd#get_string (a 1), t 1)
     | "ct" -> CallTargetValue (id#get_call_target (a 0))
-    | "se" -> SideEffectValue (t 1, bd#get_string (a 0), (a 1) = 1)
+    | "se" ->
+       SideEffectValue
+         (t 1, bd#get_string (a 0), self#get_sideeffect_argument_location (a 1))
     | "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

@@ -235,14 +235,12 @@ object (self:'a)
 
   method is_global_sideeffect =
     match denotation with
-    | AuxiliaryVariable (SideEffectValue (_, _, isglobal)) -> isglobal
+    | AuxiliaryVariable (SideEffectValue (_, _, SEGlobal _)) -> true
     | _ -> false
 
   method get_global_sideeffect_target_address: doubleword_result =
     match denotation with
-    | AuxiliaryVariable (SideEffectValue (_, arg, true)) ->
-       let addr_r = string_to_doubleword arg in
-       tprop addr_r (__FILE__ ^ ":" ^ (string_of_int __LINE__))
+    | AuxiliaryVariable (SideEffectValue (_, _, SEGlobal dw)) -> Ok dw
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
               ^ "Variable is not a global sideeffect value: "
@@ -698,9 +696,19 @@ object (self)
   method make_calltarget_value (tgt:call_target_t) =
     self#mk_variable (AuxiliaryVariable (CallTargetValue tgt))
 
-  method make_side_effect_value
-           (iaddr:ctxt_iaddress_t) ?(global=false) (arg:string) =
-    self#mk_variable (AuxiliaryVariable (SideEffectValue (iaddr,arg,global)))
+  method make_global_sideeffect_value
+           (iaddr: ctxt_iaddress_t) (arg: string) (gaddr: doubleword_int) =
+    let sev = SideEffectValue (iaddr, arg, 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
+    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
+    self#mk_variable (AuxiliaryVariable sev)
 
   method make_field_value (sname:string) (offset:int) (fname:string) =
     self#mk_variable (AuxiliaryVariable (FieldValue (sname,offset,fname)))