CHT:updates for changes in global variables

Author: sipma

CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml

@@ -71,6 +71,19 @@ let equal_doubleword =
   A.make_equal (fun dw1 dw2 -> dw1#equal dw2) (fun dw -> dw#to_hex_string)
 
 
+let equal_numerical
+      ?(msg="")
+      ~(expected: numerical_t)
+      ~(received: numerical_t)
+      () =
+  A.make_equal
+    (fun num1 num2 -> num1#equal num2)
+    (fun num -> num#toString)
+    ~msg
+    expected
+    received
+
+
 let equal_doubleword_result
       ?(msg="") (dw: doubleword_int) (dwr: doubleword_result) =
   if Result.is_error dwr then
@@ -125,10 +138,10 @@ let equal_string_imm_result_string
 
 let equal_array_index_offset
       ?(msg="")
-      ~(expected: (xpr_t * numerical_t) option)
-      ~(received: (xpr_t * numerical_t) option)
+      ~(expected: (xpr_t * xpr_t) option)
+      ~(received: (xpr_t * xpr_t) option)
       () =
-  let pri (x, n) = "(" ^ (x2s x) ^ ", " ^ n#toString ^ ")" in
+  let pri (x, r) = "(" ^ (x2s x) ^ ", " ^ (x2s r) ^ ")" in
   match (expected, received) with
   | (None, None) -> ()
   | (Some x, None) ->
@@ -137,8 +150,9 @@ let equal_array_index_offset
      A.fail_msg ("Expected None, but received Some " ^ (pri x))
   | (Some x1, Some x2) ->
      A.make_equal
-       (fun (x1, n1) (x2, n2) -> ((x2s x1) = (x2s x2)) && n1#equal n2)
-       (fun (x, n) -> "(" ^ (x2s x) ^ ", " ^ n#toString ^ ")")
+       (fun (x1, r1) (x2, r2) ->
+         ((x2s x1) = (x2s x2)) && Xprt.syntactically_equal r1 r2)
+       (fun (x, r) -> "(" ^ (x2s x) ^ ", " ^ (x2s r) ^ ")")
        ~msg
        x1
        x2
@@ -190,6 +204,22 @@ let equal_opt_meminfo
        x2
 
 
+let equal_opt_variable
+      ?(msg="")
+      ~(expected:(variable_t) option)
+      ~(received:(variable_t) option)
+      () =
+  let pri v = "(" ^ (p2s v#toPretty) ^ ")" in
+  match expected, received with
+  | None, None -> ()
+  | Some v, None ->
+     A.fail_msg ("Expected Some " ^ (pri v) ^ ", but received None")
+  | None, Some v ->
+     A.fail_msg ("Expected None, but received Some " ^ (pri v))
+  | Some v1, Some v2 ->
+     A.make_equal (fun v1 v2 -> v1#equal v2) pri ~msg v1 v2
+
+
 let equal_assignments
       ?(msg="")
       (finfo: function_info_int)

CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli

@@ -54,6 +54,12 @@ val e32: int
 
 val equal_doubleword: ?msg:string -> doubleword_int -> doubleword_int -> unit
 
+val equal_numerical:
+  ?msg:string
+  -> expected:numerical_t
+  -> received:numerical_t
+  -> unit
+  -> unit
 
 val equal_doubleword_result:
   ?msg:string -> doubleword_int -> doubleword_result -> unit
@@ -79,8 +85,8 @@ val equal_string_imm_result_string:
 
 val equal_array_index_offset:
   ?msg:string
-  -> expected:(xpr_t * numerical_t) option
-  -> received:(xpr_t * numerical_t) option
+  -> expected:(xpr_t * xpr_t) option
+  -> received:(xpr_t * xpr_t) option
   -> unit
   -> unit
 
@@ -101,6 +107,14 @@ val equal_opt_meminfo:
   -> unit
 
 
+val equal_opt_variable:
+  ?msg:string
+  -> expected:(variable_t) option
+  -> received:(variable_t) option
+  -> unit
+  -> unit
+
+
 val equal_assignments:
   ?msg:string
   -> function_info_int

CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml

@@ -26,17 +26,13 @@
    SOFTWARE.
    ============================================================================= *)
 
-(* chlib *)
-open CHNumerical
-
 (* xprlib *)
 open Xprt
 open XprTypes
 
 (* bchlib *)
 open BCHBCFiles
 open BCHBCTypes
-open BCHConstantDefinitions
 open BCHDoubleword
 open BCHFloc
 open BCHFunctionData
@@ -46,136 +42,155 @@ open BCHLibTypes
 (* bchcil *)
 open BCHParseCilFile
 
+module A = TCHAssertion
 module TR = CHTraceResult
 module TS = TCHTestSuite
 module XBA = TCHBchlibAssertion
 
+let mmap = BCHGlobalMemoryMap.global_memory_map
+
 
 let testname = "bCHFlocTest"
 let lastupdated = "2024-08-20"
 
 
-let decompose_memvar_address_test () =
+let get_var_at_address_test () =
+  let secaddr = TR.tget_ok (string_to_doubleword "0x500000") in
+  let secsize = TR.tget_ok (string_to_doubleword "0x100000") in
+  let _ =  mmap#set_section ~readonly:false ~initialized:false ".bss" secaddr secsize in
   let faddr = "0x1d6bfc" in
   let iaddr = "0x1d6cbc" in
   let gvaddr = "0x5e1e1c" in
   let dwfaddr = TR.tget_ok (string_to_doubleword faddr) in
   let dwiaddr = TR.tget_ok (string_to_doubleword iaddr) in
   let dwgvaddr = TR.tget_ok (string_to_doubleword gvaddr) in
-  let gvname = "x44_array" in
+  let dwgvxpr = num_constant_expr dwgvaddr#to_numerical in
   begin
     TS.new_testsuite
-      (testname ^ "_decompose_memvar_address_test") lastupdated;
+      (testname ^ "_get_var_at_address_test") lastupdated;
 
     parse_cil_file ~removeUnused:false "decompose_array_address.i";
     ignore (functions_data#add_function dwfaddr);
-
-    let arraysym = {
-        xconst_name = gvname;
-        xconst_value = dwgvaddr;
-        xconst_type =
-          if bcfiles#has_varinfo gvname then
-            let vinfo = bcfiles#get_varinfo gvname in
-            vinfo.bvtype
-          else
-            raise
-              (Invalid_argument "Error in arraysym");
-        xconst_desc = "decompose_memvar_address";
-        xconst_is_addr = true
-      } in
-    let _ = add_address arraysym in
     let compinfo = bcfiles#get_compinfo_by_name "x44_struct_t" in
-
     let finfo = get_function_info dwfaddr in
     let floc = get_floc_by_address dwfaddr dwiaddr in
-    let ty = get_symbolic_address_type_by_name gvname in
-    let basevar =
-      finfo#env#mk_global_memory_address
-        ~optname:(Some gvname) ~opttype:(Some ty) dwgvaddr#to_numerical in
-    let memref = TR.tget_ok (floc#f#env#mk_base_variable_reference basevar) in
+    let gvar = TR.tget_ok (finfo#env#mk_global_variable dwgvaddr#to_numerical) in
     let indexvar = finfo#env#mk_initial_register_value (ARMRegister AR0) in
     let indexxpr1 = XOp (XMinus, [XVar indexvar; int_constant_expr 1]) in
 
     TS.add_simple_test
       ~title:"constant-68"
       (fun () ->
-        let xpr = XOp (XPlus, [XVar basevar; int_constant_expr 68]) in
-        let xpsuboffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(int_constant_expr 1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xpr = XOp (XPlus, [dwgvxpr; int_constant_expr 68]) in
+        let xpr = Xsimplify.simplify_xpr xpr in
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in
+        let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(int_constant_expr 1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+          Ok received ->
+           XBA.equal_opt_variable
+             ~expected
+             ~received:(Some received)
+             ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
 
     TS.add_simple_test
       ~title:"constant-72"
       (fun () ->
-        let xpr = XOp (XPlus, [XVar basevar; int_constant_expr 72]) in
-        let xpsuboffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(int_constant_expr 1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xpr = XOp (XPlus, [dwgvxpr; int_constant_expr 72]) in
+        let xpr = Xsimplify.simplify_xpr xpr in
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in
+        let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(int_constant_expr 1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+          Ok received ->
+          XBA.equal_opt_variable
+            ~expected
+            ~received:(Some received)
+            ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
 
     TS.add_simple_test
       ~title:"var-68"
       (fun () ->
         let xpr =
-          XOp (XPlus, [XVar basevar;
+          XOp (XPlus, [dwgvxpr;
                        XOp (XMult, [int_constant_expr 68; XVar indexvar])]) in
-        let xpsuboffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(XVar indexvar, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in
+        let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(XVar indexvar, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+        | Ok received ->
+          XBA.equal_opt_variable
+            ~expected
+            ~received:(Some received)
+            ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
+
 
     TS.add_simple_test
       ~title:"varm1-68"
       (fun () ->
         let subxpr = XOp (XMult, [int_constant_expr 68; XVar indexvar]) in
         let subxpr = XOp (XMinus, [subxpr; int_constant_expr 68]) in
-        let xpr = XOp (XPlus, [XVar basevar; subxpr]) in
-        let xpsuboffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(indexxpr1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xpr = XOp (XPlus, [dwgvxpr; subxpr]) in
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in
+        let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+        | Ok received ->
+           XBA.equal_opt_variable
+             ~expected
+             ~received:(Some received)
+             ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
 
     TS.add_simple_test
       ~title:"varm1-64"
       (fun () ->
         let subxpr = XOp (XMult, [int_constant_expr 68; XVar indexvar]) in
         let subxpr = XOp (XMinus, [subxpr; int_constant_expr 64]) in
-        let xpr = XOp (XPlus, [XVar basevar; subxpr]) in
-        let xpsuboffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(indexxpr1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xpr = XOp (XPlus, [dwgvxpr; subxpr]) in
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in
+        let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+        | Ok received ->
+           XBA.equal_opt_variable
+             ~expected
+             ~received:(Some received)
+             ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
 
     TS.add_simple_test
       ~title:"varm1-60"
       (fun () ->
         let subxpr = XOp (XMult, [int_constant_expr 68; XVar indexvar]) in
         let subxpr = XOp (XMinus, [subxpr; int_constant_expr 60]) in
-        let xpr = XOp (XPlus, [XVar basevar; subxpr]) in
-        let xpsuboffset = ConstantOffset (numerical_zero, NoOffset) in
-        let xpsuboffset = FieldOffset (("buffer", compinfo.bckey), xpsuboffset) in
-        let xpmemoffset = ArrayIndexOffset(indexxpr1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
+        let xpr = XOp (XPlus, [dwgvxpr; subxpr]) in
+        let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_char xpr in
+        let xpoffset = ArrayIndexOffset (int_constant_expr 0, NoOffset) in
+        let xpoffset = FieldOffset (("buffer", compinfo.bckey), xpoffset) in
+        let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+        | Ok received ->
+           XBA.equal_opt_variable
+             ~expected
+             ~received:(Some received)
+             ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
 
     (* (((g_data_array + (0x4 * R0_in[4]_in)) + (0x40 * R0_in[4]_in)) - 0x40)) *)
 
@@ -184,24 +199,29 @@ let decompose_memvar_address_test () =
       (fun () ->
         let subxpr1 = XOp (XMult, [int_constant_expr 4; XVar indexvar]) in
         let subxpr2 = XOp (XMult, [int_constant_expr 64; XVar indexvar]) in
-        let xpr = XOp (XPlus, [XVar basevar; subxpr1]) in
+        let xpr = XOp (XPlus, [dwgvxpr; subxpr1]) in
         let xpr = XOp (XPlus, [xpr; subxpr2]) in
         let xpr = XOp (XMinus, [xpr; int_constant_expr 64]) in
-        let xpsuboffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
-        let xpmemoffset = ArrayIndexOffset(indexxpr1, xpsuboffset) in
-        let optmeminfo = floc#decompose_memvar_address xpr in
-        XBA.equal_opt_meminfo
-          ~expected: (Some (memref, xpmemoffset))
-          ~received: optmeminfo
-          ());
-
+        let xprvar = floc#get_var_at_address xpr in
+        let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in
+        let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in
+        let expected_r = finfo#env#add_memory_offset gvar xpoffset in
+        let expected = TR.to_option expected_r in
+        match xprvar with
+        | Ok received ->
+           XBA.equal_opt_variable
+             ~expected
+             ~received:(Some received)
+             ()
+        | Error e -> A.fail_msg ("Error: " ^ (String.concat "; " e)));
+ 
     TS.launch_tests ()
   end
 
 
 let () =
   begin
     TS.new_testfile testname lastupdated;
-    decompose_memvar_address_test ();
+    get_var_at_address_test ();
     TS.exit_file ()
   end