Liftingsupport

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250420"
-  ~date:"2025-04-20"
+  ~version:"0.6.0_20250502"
+  ~date:"2025-05-02"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml

@@ -616,6 +616,7 @@ object (self)
             ""
           end)
         (gloc#address_memory_offset ~tgtsize:(Some 4) offset) in
+    let vm1 (v: doubleword_int) = TR.to_option (v#subtract_int 1) in
     let render_gloc (a: doubleword_int) (v: doubleword_int): string =
       let addrprefix = "  " ^ (fixed_length_string a#to_hex_string 10) in
       let p_value =
@@ -634,9 +635,40 @@ object (self)
           ^ v#to_hex_string
           ^ name
           ^ ">"
+        else if (Option.is_some (vm1 v))
+                && functions_data#is_function_entry_point (Option.get (vm1 v)) then
+          let fentry = Option.get (vm1 v) in
+          let name =
+            if functions_data#has_function_name fentry then
+              let fndata = functions_data#get_function fentry in
+              ":" ^ fndata#get_function_name
+            else
+              "" in
+          "Faddr:<"
+          ^ v#to_hex_string
+          ^ name
+          ^ "(T)>"
+        else if memorymap#has_location v then
+          let gloc = memorymap#get_location v in
+          "GVAddr:<"
+          ^ v#to_hex_string
+          ^ ":"
+          ^ gloc#name
+          ^ ">"
+
         else if elf_header#is_code_address v then
+          let s =
+            match elf_header#get_string_at_address v with
+            | Some s ->
+               let len = String.length s in
+               if len < 50 then
+                 ":\"" ^ s ^ "\""
+               else
+                 ":\"" ^ (String.sub s 0 50) ^ "...\""
+            | _ -> "" in
           "Code:<"
           ^ v#to_hex_string
+          ^ s
           ^ ">"
         else if elf_header#is_data_address v then
           let s =
@@ -648,7 +680,7 @@ object (self)
                else
                  ":\"" ^ (String.sub s 0 50) ^ "...\""
             | _ -> "" in
-          "  Data:<"
+          "Data:<"
           ^ v#to_hex_string
           ^ s
           ^ ">"
@@ -664,7 +696,9 @@ object (self)
              match offset with
              | XConst (IntConst n) when n#equal numerical_zero ->
                 addrprefix
-                ^ "\n  Global variable:<"
+                ^ "\n"
+                ^ addrprefix
+                ^ "  Global variable:<"
                 ^ gloc#name
                 ^ ": "
                 ^ (btype_to_string gloc#btype)
@@ -743,6 +777,13 @@ object (self)
              "  " ^ (fixed_length_string !addr#to_hex_string 10) ^ "  align\n"
            else
              "" in
+         let render_string (s: string): string =
+           let len = String.length s in
+           if len <= 40 then
+             s
+           else
+             (String.sub s 0 40) ^ "... (length: " ^ (string_of_int len) ^ ")" in
+
          let _ =
            if prefix > 0 && (String.length s) >= prefix then
              ch#skip_bytes prefix in
@@ -754,6 +795,7 @@ object (self)
                  addr := !addr#add_int 4
                end
              done;
+             let addrstr_end = ref wordzero in
              ("\n" ^ (string_repeat "~" 80) ^ "\nData block (size: "
               ^ (string_of_int len) ^ " bytes)\n\n"
               ^ pprefix
@@ -772,6 +814,12 @@ object (self)
                           ^ (fixed_length_string v#to_hex_string 12)
                           ^ "> ... (cont'd)"
 
+                        else if a#lt !addrstr_end then
+                          addrprefix
+                          ^ "  <String:<"
+                          ^ (fixed_length_string v#to_hex_string 12)
+                          ^ "> ... (cont'd)"
+
                         else if Option.is_some (memorymap#containing_location a) then
                           render_gloc a v
 
@@ -802,6 +850,24 @@ object (self)
                           ^ v#to_hex_string
                           ^ name
                           ^ ">"
+                          ^ pdatarefstr
+
+                              (* handle thumb function addresses (+1) *)
+                        else if (Option.is_some (vm1 v))
+                                && functions_data#is_function_entry_point
+                                     (Option.get (vm1 v)) then
+                          let fentry = Option.get (vm1 v) in
+                          let name =
+                            if functions_data#has_function_name fentry then
+                              let fndata = functions_data#get_function fentry in
+                              ":" ^ fndata#get_function_name
+                            else
+                              "" in
+                          addrprefix
+                          ^ "  Faddr:<"
+                          ^ v#to_hex_string
+                          ^ name
+                          ^ "(T)>"
                           ^ pdatarefstr
 
                         else if memorymap#has_location v then
@@ -815,9 +881,20 @@ object (self)
                           ^ pdatarefstr
 
                         else if elf_header#is_code_address v then
+                          let s =
+                            match elf_header#get_string_at_address v with
+                            | Some s ->
+                               let len = String.length s in
+                               if len < 50 then
+                                 ":\"" ^ s ^ "\""
+                               else
+                                 ":\"" ^ (String.sub s 0 50) ^ "...\""
+                            | _ -> "" in
+
                           addrprefix
                           ^ "  Code:<"
                           ^ v#to_hex_string
+                          ^ s
                           ^ ">"
                           ^ (datarefstr a)
 
@@ -848,12 +925,15 @@ object (self)
                                   (elf_header#get_string_at_address a) then
                           let s =
                             Option.get (elf_header#get_string_at_address a) in
+                          let slen = String.length s in
+                          let slen = if slen > 40 then 40 else slen in
+                          let _ = addrstr_end := a#add_int slen in
                           begin
                             (addrprefix
                              ^ "  String:<"
                              ^ (fixed_length_string v#to_hex_string 12)
                              ^ ">: \""
-                             ^ s
+                             ^ (render_string s)
                              ^ "\"")
                             ^ pdatarefstr
                           end

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -1479,11 +1479,60 @@ object (self)
          (tags, args)
 
       | LoadMultipleIncrementBefore (wback, c, base, rl, _) ->
-         let reglhs_rl = rl#to_multiple_variable floc in
+         let lhsvars_rl = rl#to_multiple_variable floc in
          let basereg = base#get_register in
          let baselhs_r = base#to_variable floc in
          let baserhs_r = base#to_expr floc in
          let regcount = rl#get_register_count in
+         let (memrhss_r, rmemrhss_r, cmemrhss_r, _) =
+           List.fold_left
+             (fun (mems, rmems, cmems, off) _lhsvar ->
+               let memop = arm_reg_deref ~with_offset:off basereg RD in
+               let memrhs_r = memop#to_expr floc in
+               let rmemrhs_r = TR.tmap rewrite_expr memrhs_r in
+               let cmemrhs_r =
+                 TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rmemrhs_r in
+               (mems @ [memrhs_r],
+                rmems @ [rmemrhs_r],
+                cmems @ [cmemrhs_r],
+                off + 4)) ([], [], [], 4) lhsvars_rl in
+         let xaddrs_r =
+           List.init
+             rl#get_register_count
+             (fun i ->
+               let xaddr_r =
+                 TR.tmap
+                   (fun baserhs ->
+                     XOp (XPlus, [baserhs; int_constant_expr (i + 4)]))
+                   baserhs_r in
+               TR.tmap rewrite_expr xaddr_r) in
+         let cxaddrs_r =
+           List.map (fun xaddr_r ->
+               TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xaddr_r)
+             xaddrs_r in
+         let rdefs = List.map get_rdef_r (baserhs_r :: memrhss_r) in
+         let uses = List.map get_def_use_high_r (baselhs_r :: lhsvars_rl) in
+         let useshigh = List.map get_def_use_high_r (baselhs_r :: lhsvars_rl) in
+         let vars_r = baselhs_r :: lhsvars_rl in
+         let xprs_r = baserhs_r :: (memrhss_r @ rmemrhss_r @ xaddrs_r) in
+         let cxprs_r = cmemrhss_r @ cxaddrs_r in
+         let (tagstring, args) =
+           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
+         let tags = add_optional_subsumption tags in
+         let (tags, args) =
+           if wback then
+             let inc = 4 * regcount in
+             let xinc = int_constant_expr inc in
+             let baseresult_r =
+               TR.tmap (fun baserhs -> XOp (XPlus, [baserhs; xinc])) baserhs_r in
+             let rbaseresult_r = TR.tmap rewrite_expr baseresult_r in
+             add_base_update tags args baselhs_r inc rbaseresult_r
+           else
+             (tags, args) in
+         (tags, args)
+         (*
          let (memreads_r, _) =
            List.fold_left
              (fun (acc, off) _reglhs ->
@@ -1513,6 +1562,7 @@ object (self)
              () in
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
+          *)
 
       | LoadRegister _ when instr#is_aggregate_anchor ->
          let iaddr = instr#get_address in

CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml

@@ -2346,9 +2346,24 @@ let translate_arm_instruction
            match rtype with
            | TVoid _ -> []
            | _ ->
+              (* Return variables need to be treated somewhat differently
+                 than other 'initial-value' variables, because in the
+                 lifting to C code they get assigned to, while other
+                 'initial-value' variables always have their values
+                 and thus are by default not included in the use-high
+                 variables. *)
               let r0_op = arm_register_op AR0 RD in
-              let xr0 = r0_op#to_expr floc in
-              get_use_high_vars_r [xr0]
+              let xr0_r = r0_op#to_expr floc in
+              TR.tfold_default
+                (fun xr0 ->
+                  let xxr0 = floc#inv#rewrite_expr xr0 in
+                  match xxr0 with
+                  | XVar v when floc#env#is_return_value v ->
+                     [floc#f#env#mk_arm_register_variable AR0]
+                  | _ ->
+                     get_use_high_vars_r ~is_pop:true [xr0_r])
+                (get_use_high_vars_r ~is_pop:true [xr0_r])
+                xr0_r
          else
            [] in
        let popdefcmds =