Liftingsupport

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -699,17 +699,23 @@ object (self)
       let memoffset = numoffset#add offset in
       let memref_r = self#env#mk_base_sym_reference base in
       let memoff_r =
+        address_memory_offset
+          t_unknown ~tgtsize:(Some size) (num_constant_expr memoffset) in
+      (*
+        To keep representation unifor (i.e., to avoid aliasing) the creation
+        of variable representation against the type of the variable must be
+        delayed until reporting time.
         TR.tbind
           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
           (fun basevar ->
             let optbasetype = self#env#get_variable_type basevar in
-            let basetype =
+            let basetype = t_unknown in
               match optbasetype with
               | Some t when is_pointer t -> ptr_deref t
               | _ -> t_unknown in
-            address_memory_offset basetype
+            address_memory_offset t_unknown
               ~tgtsize:(Some size) (num_constant_expr memoffset))
-          (self#env#get_variable base#getSeqNumber) in
+          (self#env#get_variable base#getSeqNumber) in *)
       mk_memvar memref_r memoff_r
 
     else
@@ -1527,9 +1533,16 @@ object (self)
            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
            (fun v -> XVar v) (self#convert_variable_offsets ~size v)
       | XOp ((Xf "addressofvar"), [XVar v]) ->
+         let newx_r =
+           TR.tmap
+             ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+             (fun v -> XVar v) (self#convert_variable_offsets ~size v) in
          TR.tmap
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-           (fun v -> XVar v) (self#convert_variable_offsets ~size v)
+           (fun newx ->
+             match newx with
+             | XVar v -> XOp ((Xf "addressofvar"), [(XVar v)])
+             | _ -> exp)
+           newx_r
       | XOp (op, [xx]) -> TR.tmap (fun x -> XOp (op, [x])) (aux xx)
       | XOp (op, [x1; x2]) ->
          TR.tmap2 (fun x1 x2 -> XOp (op, [x1; x2])) (aux x1) (aux x2)
@@ -1550,12 +1563,15 @@ object (self)
     let knownpointers = List.filter self#f#is_base_pointer vars in
     match knownpointers with
     (* one known pointer, must be the base *)
-    | [base] when self#f#env#is_initial_stackpointer_value base ->
+    | [base] (* when self#f#env#is_initial_stackpointer_value base *) ->
        let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
        let memref_r = self#env#mk_base_variable_reference base in
        let memoff_r = address_memory_offset t_unknown offset in
        (memref_r, memoff_r)
 
+       (* resolving to type-based representations at this point may give
+          rise to aliasing; for example __ptr_deref_R[0]_in.field_4 may be aliased
+          with R[0]_in[4]_in
     | [base] ->
        let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
        let memref_r = self#env#mk_base_variable_reference base in
@@ -1582,6 +1598,7 @@ object (self)
                  ^ "base pointer: " ^ (x2s (XVar base)))
            (fun basetype -> address_memory_offset basetype offset)
            basetype_r in
+        *)
 
        (*
          (match offset with
@@ -1593,7 +1610,7 @@ object (self)
                     ^ "Offset from base "
                     ^ (x2s (XVar base))
                     ^ " not recognized: " ^ (x2s offset)]) in *)
-       (memref_r, memoff_r)
+    (* (memref_r, memoff_r) *)
 
     (* no known pointers, have to find a base *)
     | [] ->

CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2022-2024  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
@@ -197,11 +197,13 @@ object (self)
       H.iter
         (fun _ (var, locs) ->
           let locs = List.sort Stdlib.compare locs#toList in
-          self#add_fact (DefUseHigh (var,locs))) usehighlocs
+          self#add_fact (DefUseHigh (var, locs))) usehighlocs
     end
 
   method get_var_facts (var: variable_t): var_invariant_int list =
-    List.filter (fun f -> f#get_variable#equal var) self#get_facts
+    let varix = var#getName#getSeqNumber in
+    List.filter (fun f ->
+        f#get_variable#getName#getSeqNumber = varix) self#get_facts
 
   method get_var_reaching_defs (var: variable_t): var_invariant_int list =
     List.filter (fun f -> f#is_reaching_def) (self#get_var_facts var)

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,7 +95,7 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250314"
+  ~version:"0.6.0_20250316"
   ~date:"2025-03-14"
   ~licensee: None
   ~maxfilesize: None

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -2631,6 +2631,11 @@ object (self)
              (fun (acc, off) _reg ->
                let memop = arm_reg_deref ~with_offset:off basereg WR in
                let memlhs_r = memop#to_variable floc in
+               let memlhs_r =
+                 let r =
+                   TR.tbind
+                     (floc#convert_variable_offsets ~size:(Some 4)) memlhs_r in
+                 if Result.is_ok r then r else memlhs_r in
                (acc @ [memlhs_r], off + 4)) ([], 4) rl#get_register_op_list in
          let rdefs = List.map get_rdef_r (baserhs_r :: rrhss_rl) in
          let uses = List.map get_def_use_r (baselhs_r :: memlhss_rl) in
@@ -2757,7 +2762,13 @@ object (self)
 
       | StoreRegisterDual (c, rt, rt2, rn, rm, mem, mem2) ->
          let vmem_r = mem#to_variable floc in
+         let vmem_r =
+           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem_r in
+           if Result.is_ok r then r else vmem_r in
          let vmem2_r = mem2#to_variable floc in
+         let vmem2_r =
+           let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem2_r in
+           if Result.is_ok r then r else vmem2_r in
          let xaddr1_r = mem#to_address floc in
          let xaddr2_r = mem2#to_address floc in
          let xaddr1_r = TR.tmap rewrite_expr xaddr1_r in

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -144,6 +144,7 @@ object (self)
            if i < 128 then (SignedNeutral, 8)
            else if i < BCHDoubleword.e15 then (SignedNeutral, 16)
            else if i < BCHDoubleword.e31 then (SignedNeutral, 32)
+           else if i = 0xffffffff then (Signed, 32)
            else (SignedNeutral, 64) in
          TyTInt (sg, si) in