CHB: add more support for conversion to C expressions

Author: sipma

CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml

@@ -54,6 +54,8 @@ open BCHNumericalConstraints
 module H = Hashtbl
 module TR = CHTraceResult
 
+let p2s = CHPrettyUtil.pretty_to_string
+
 
 module ConstraintCollections = CHCollections.Make
   (struct
@@ -442,17 +444,19 @@ let extract_valuesets
   H.iter (fun k v ->
     if H.mem v "valuesets" then
       let inv = H.find v "valuesets" in
-      let flocinv = finfo#finv#get_location_invariant k in
       let domain = inv#getDomain "valuesets" in
       let varObserver = domain#observer#getNonRelationalVariableObserver in
       let vars = domain#observer#getObservedVariables in
-      let knownvars = flocinv#get_known_variables in
-      let vars =
-        List.filter (fun v ->
-            not (v#isTmp || List.mem v knownvars)) vars in
+      let vars = List.filter (fun v -> not v#isTmp) vars in
       List.iter (fun (v:variable_t) ->
 	let valueset = (varObserver v)#toValueSet in
-	if valueset#isTop then () else
+	if valueset#isTop then
+          let _ =
+            log_diagnostics_result
+              ~tag:"value-sets: top"
+              __FILE__ __LINE__ [k ^ ": " ^ (p2s v#toPretty)] in
+          ()
+        else
 	  if valueset#removeZeroOffset#isSingleBase then
 	    let (base,offset) = valueset#removeZeroOffset#getSingleBase in
 	    let canbenull:bool = valueset#includesZero in

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -195,10 +195,16 @@ object (self)
                    ~(tgtbtype: btype_t option)
                    (c: bcompinfo_t)
                    (xoffset: xpr_t): memory_offset_t traceresult =
+    let is_void_tgtbtype =
+      match tgtbtype with
+      | Some (TVoid _) -> true
+      | _ -> false in
     let check_tgttype_compliance (t: btype_t) (s: int) =
       match tgtsize, tgtbtype with
       | None, None -> true
       | Some size, None -> size = s
+      | Some size, Some (TVoid _) -> size = s
+      | None, Some (TVoid _) -> true
       | None, Some ty -> btype_equal ty t
       | Some size, Some ty -> size = s && btype_equal ty t in
     let compliance_failure (t: btype_t) (s: int) =
@@ -246,7 +252,10 @@ object (self)
                      let offset = offset - foff in
                      tbind
                        (fun fldtype ->
-                         if offset = 0
+                         if offset = 0 && is_void_tgtbtype then
+                           Ok (Some (FieldOffset
+                                       ((finfo.bfname, finfo.bfckey), NoOffset)))
+                         else if offset = 0
                             && (is_scalar fldtype)
                             && (check_tgttype_compliance fldtype sz) then
                            Ok (Some (FieldOffset
@@ -305,6 +314,47 @@ object (self)
          Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
                 ^ " xoffset: " ^ (x2s xoffset)
                 ^ "; btype: " ^ (btype_to_string btype)]
+    | XOp (XPlus, [XOp (XMult, [XConst (IntConst n); XVar v]);
+                   XConst (IntConst m)]) when is_struct_type btype ->
+       let compinfo = get_struct_type_compinfo btype in
+       let fldoffset = XConst (IntConst m) in
+       let memoffset_r =
+         self#get_field_memory_offset_at
+           ~tgtsize:None ~tgtbtype:None compinfo fldoffset in
+       TR.tbind
+         (fun memoffset ->
+           match memoffset with
+           | FieldOffset ((fname, fckey), NoOffset) ->
+              let fcinfo = get_compinfo_by_key fckey in
+              let field = get_compinfo_field fcinfo fname in
+              let fieldtype = field.bftype in
+              if is_array_type fieldtype then
+                let eltype = get_element_type fieldtype in
+                let elsize_r = size_of_btype eltype in
+                TR.tbind
+                  (fun elsize ->
+                    if elsize = n#toInt then
+                      let aoffset = ArrayIndexOffset (XVar v, NoOffset) in
+                      let moffset =
+                        BCHMemoryReference.add_offset memoffset aoffset in
+                      Ok moffset
+                    else
+                      Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
+                             ^ "field: " ^ fname
+                             ^ "; fieldtype: " ^ (btype_to_string fieldtype)
+                             ^ "; elementsize: " ^ (string_of_int elsize)
+                             ^ "; expected: " ^ n#toString])
+                  elsize_r
+              else
+                Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                       ^ "not an array type"]
+           | _ ->
+              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
+                     ^ "fldoffset: " ^ (x2s fldoffset)
+                     ^ "; memoffset: "
+                     ^ (BCHMemoryReference.memory_offset_to_string memoffset)])
+         memoffset_r
+
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
                 ^ " xoffset: " ^ (x2s xoffset)

CodeHawk/CHB/bchlib/bCHLocationInvariant.ml

@@ -58,9 +58,13 @@ module H = Hashtbl
 module TR = CHTraceResult
 
 
-(* let x2p = XprToPretty.xpr_formatter#pr_expr *)
+let x2p = XprToPretty.xpr_formatter#pr_expr
 let tracked_locations = []
 
+let p2s = CHPrettyUtil.pretty_to_string
+let x2s x = p2s (x2p x)
+
+
 let track_location loc p =
   if List.mem loc tracked_locations then
     chlog#add ("tracked:" ^ loc) p
@@ -1068,6 +1072,11 @@ object (self)
     (self#get_location_invariant iaddr)#add_fact fact
 
   method add_symbolic_expr_fact (iaddr:string) (v:variable_t) (x:xpr_t) =
+    let _ =
+      log_diagnostics_result
+        ~tag:("add symbolic-expr fact for " ^ iaddr)
+        __FILE__ __LINE__
+        [(p2s v#toPretty) ^ ": " ^ (x2s x)] in
     self#add iaddr (NonRelationalFact (v,FSymbolicExpr x))
 
   method set_unreachable (iaddr:string) (domain:string) =
@@ -1091,6 +1100,13 @@ object (self)
            (base:symbol_t)
            (i:interval_t)
            (canbenull:bool) =
+    let _ =
+      log_diagnostics_result
+        ~tag:("add valueset fact for " ^ iaddr)
+        __FILE__ __LINE__
+        [(p2s v#toPretty) ^ ": "
+         ^ "base: " ^ (p2s base#toPretty)
+         ^ "; offset: " ^ (p2s i#toPretty)] in
     let fact =
       if i#isBottom then
 	Unreachable "valuesets"

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250401"
-  ~date:"2025-04-01"
+  ~version:"0.6.0_20250417"
+  ~date:"2025-04-17"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -649,9 +649,11 @@ object (self)
                    match xx with
                    | XVar _ -> xx
                    | _ ->
-                      TR.tfold_default
-                        (fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
-                        xx
+                      TR.tfold
+                        ~ok:(fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
+                        ~error:(fun e ->
+                          let _ = log_dc_error_result __FILE__ __LINE__ e in
+                          xx)
                         (floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
               else
                 xx in
@@ -770,21 +772,23 @@ object (self)
          let xrm_r = rm#to_expr floc in
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XPlus, [xrn; xrm])) xrn_r xrm_r in
+         let xxrn_r = TR.tmap rewrite_expr xrn_r in
+         let xxrm_r = TR.tmap rewrite_expr xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
+         let cresult_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
          let _ =
            TR.tfold_default
              (fun r -> ignore (get_string_reference floc r)) () rresult_r in
-         let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] in
-         let uses = get_def_use_r vrd_r in
-         let useshigh = get_def_use_high_r vrd_r in
+         let rdefs =
+           [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
+         let uses = [get_def_use_r vrd_r] in
+         let useshigh = [get_def_use_high_r vrd_r] in
+         let vars_r = [vrd_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in
+         let cxprs_r = [cresult_r] in
          let (tagstring, args) =
-           mk_instrx_data_r
-             ~vars_r:[vrd_r]
-             ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
-             ~rdefs:rdefs
-             ~uses:[uses]
-             ~useshigh:[useshigh]
-             () in
+           mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
@@ -2285,6 +2289,8 @@ object (self)
          let xrm_r = rm#to_expr floc in
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrm; xrn])) xrn_r xrm_r in
+         let xxrn_r = TR.tmap rewrite_expr xrn_r in
+         let xxrm_r = TR.tmap rewrite_expr xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
          let cresult_r =
            TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
@@ -2293,7 +2299,7 @@ object (self)
          let uses = [get_def_use_r vrd_r] in
          let useshigh = [get_def_use_high_r vrd_r] in
          let vars_r = [vrd_r] in
-         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
+         let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in
          let cxprs_r = [cresult_r] in
          let (tagstring, args) =
            mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in

CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml

@@ -2345,7 +2345,10 @@ let translate_arm_instruction
          if rl#includes_pc then
            match rtype with
            | TVoid _ -> []
-           | _ -> [floc#f#env#mk_arm_register_variable AR0]
+           | _ ->
+              let r0_op = arm_register_op AR0 RD in
+              let xr0 = r0_op#to_expr floc in
+              get_use_high_vars_r [xr0]
          else
            [] in
        let popdefcmds =