CHB: move functionality to global memory map

Author: sipma

CodeHawk/CHB/bchanalyze/bCHFileIO.ml

@@ -200,6 +200,19 @@ let save_global_state () =
     file_output#saveFile filename doc#toPretty
   end
 
+
+let save_global_memory_map () =
+  let filename = get_global_memory_map_filename () in
+  let doc = xmlDocument () in
+  let root = get_bch_root "global-locations" in
+  let gNode = xmlElement "global-locations" in
+  begin
+    BCHGlobalMemoryMap.global_memory_map#write_xml gNode;
+    doc#setNode root;
+    root#appendChildren [gNode];
+    file_output#saveFile filename doc#toPretty
+  end
+
 let save_system_info () =
   let filename = get_system_info_filename () in
   let doc = xmlDocument () in

CodeHawk/CHB/bchanalyze/bCHFileIO.mli

@@ -43,6 +43,7 @@ val save_functions_list: unit -> unit
 val save_arm_functions_list: unit -> unit
 
 val save_global_state: unit -> unit
+val save_global_memory_map: unit -> unit
 val save_system_info: unit -> unit
 val save_resultmetrics: xml_element_int -> unit
 val save_disassembly_status: unit -> unit

CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml

@@ -602,6 +602,8 @@ let main () =
             pr_timing [STR "system_info saved"];
             save_arm_dictionary ();
             pr_timing [STR "dictionary saved"];
+            save_global_memory_map ();
+            pr_timing [STR "global-locations saved"];
             save_interface_dictionary ();
             pr_timing [STR "interface dictionary saved"];
             save_bcdictionary ();
@@ -898,6 +900,8 @@ let main () =
         (* save_arm_assembly_instructions (); *)
         save_arm_dictionary ();
         pr_timing [STR "arm dictionary saved"];
+        save_global_memory_map ();
+        pr_timing [STR "global-locations saved"];
         save_bc_files ();
         pr_timing [STR "bc files saved"];
         save_interface_dictionary ();

CodeHawk/CHB/bchcmdline/bCHXInspectSummaries.ml

@@ -38,7 +38,6 @@ open CHLogger
 
 (* bchlib *)
 open BCHBasicTypes
-open BCHConstantDefinitions
 open BCHFunctionSummaryLibrary
 open BCHLibTypes
 open BCHSystemInfo
@@ -126,7 +125,7 @@ let print_statistics () =
 	STR "Type definitions: "; NL; type_definitions#toPretty; NL;
         STR "IO action categories: "; INT (List.length pActions); NL;
         STR "Parameter roles     : "; INT nParamRoles; NL;
-	constant_statistics_to_pretty ();  NL]
+	BCHConstantDefinitions.constant_statistics_to_pretty ();  NL]
   end
 
 let main () =

CodeHawk/CHB/bchlib/bCHDoubleword.ml

@@ -488,6 +488,11 @@ let numerical_to_doubleword (num:numerical_t): doubleword_result =
     "numerical_to_doubleword"
 
 
+let numerical_mod_to_doubleword (num: numerical_t): doubleword_int =
+  let num = num#modulo numerical_e32 in
+  TR.tget_ok (numerical_to_doubleword num)
+
+
 let dw_index_to_int (index:dw_index_t) = index
 
 

CodeHawk/CHB/bchlib/bCHDoubleword.mli

@@ -109,7 +109,7 @@ val big_int_to_doubleword: big_int -> doubleword_result
 val string_to_doubleword: string -> doubleword_result
 
 
-(**[numerical_to_doubleword num] converts num to a doubleword.
+(**[numerical_to_doubleword num] converts [num] to a doubleword.
 
    [num] must be less than [2^32] and greater than or equal [-2^31].
    Negative numbers are represented by their two's complement
@@ -118,6 +118,11 @@ val string_to_doubleword: string -> doubleword_result
 val numerical_to_doubleword: numerical_t -> doubleword_result
 
 
+(** [numerical_mod_to_doubleword num] converts [num] to a a doubleword.
+    [num] will be forced within the range [0..2^32-1] using wraparound.*)
+val numerical_mod_to_doubleword: numerical_t -> doubleword_int
+
+
 (** [numerical_to_hex_string num] converts num to a hexadecimal string
     representation via a doubleword representation.
 

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -599,22 +599,10 @@ object (self)
     let fintf = ctinfo#get_function_interface in
     let stackpars = get_stack_parameters fintf in
     let regpars = get_register_parameters fintf in
-    let _ =
-      chlog#add
-        "floc:get_call_arguments"
-        (LBLOCK [
-             self#l#toPretty;
-             STR "  ";
-             STR ctinfo#get_name;
-             STR ": ";
-             INT (List.length stackpars);
-             STR " stackparameters; ";
-             INT (List.length regpars);
-             STR " register parameters"]) in
-
     List.concat [(get_regargs regpars); (get_stackargs stackpars)]
 
   method get_call_args =
+    (* used in x86 only *)
     let ctinfo = self#get_call_target in
     if ctinfo#is_wrapped_app_call then
       self#get_wrapped_call_args

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -109,6 +109,8 @@ module DoublewordCollections = CHCollections.Make
 
 let id = BCHInterfaceDictionary.interface_dictionary
 
+let memmap = BCHGlobalMemoryMap.global_memory_map
+
 
 type po_anchor_t =                      (* proof obligation anchor *)
 | DirectAccess
@@ -850,7 +852,23 @@ object (self)
            ?(size=4)
            ?(offset=NoOffset)
            (base: numerical_t): variable_t traceresult =
-    let base = base#modulo (mkNumerical BCHDoubleword.e32) in
+    let dwbase =
+      fail_tfold
+        (trerror_record
+           (LBLOCK [
+                STR "Converting ";
+                base#toPretty;
+                STR " in finfo.mk_global_variable in function ";
+                faddr#toPretty]))
+        (fun b -> b)
+        (numerical_to_doubleword (base#modulo (mkNumerical BCHDoubleword.e32))) in
+    let default (gloc: global_location_int) =
+      let var =
+        self#mk_variable (varmgr#make_global_variable ~size ~offset base) in
+      let _ = self#set_variable_name var gloc#name in
+      Ok var in
+
+    (*
     match numerical_to_doubleword base with
     | Error e -> Error ("finfo.mk_global_variable" :: e)
     | Ok addr ->
@@ -880,6 +898,29 @@ object (self)
             | _ -> ());
            Ok var
          end in
+     *)
+    match memmap#containing_location dwbase with
+    | Some gloc ->
+       tfold
+         ~ok:(fun memoffset ->
+           let var =
+             self#mk_variable
+               (varmgr#make_global_variable
+                  ~offset:memoffset gloc#address#to_numerical) in
+           let _ = self#set_variable_name var gloc#name in
+           Ok var)
+         ~error:(fun sl ->
+           begin
+             chlog#add
+               "fenv#mk_global_variable: Error"
+               (LBLOCK [faddr#toPretty; STR ": "; STR (String.concat "; " sl)]);
+             default gloc
+           end)
+         (gloc#address_memory_offset dwbase)
+    | _ ->
+       Ok (self#mk_variable (varmgr#make_global_variable ~size ~offset base))
+      (*
+               |
 
        if is_in_global_structvar addr then
          (match get_structvar_base_offset addr with
@@ -951,6 +992,7 @@ object (self)
              default ())
        else
          default ()
+       *)
 
   method mk_global_memory_address
            ?(optname = None) ?(opttype=None) (n: numerical_t) =
@@ -2010,7 +2052,13 @@ object (self)
   method set_bc_summary (fs: function_summary_int) =
     begin
       appsummary <- fs;
-      env#set_argument_names fs#get_function_interface
+      env#set_argument_names fs#get_function_interface;
+      chlog#add
+        "set-bc-summary"
+        (LBLOCK [
+             function_interface_to_pretty fs#get_function_interface;
+             STR " with function signature ";
+             STR (btype_to_string fs#get_function_interface.fintf_type_signature.fts_returntype)])
     end
 
   method read_xml_user_summary (node:xml_element_int) =

CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml

@@ -40,7 +40,6 @@ open CHXmlDocument
 (* bchlib *)
 open BCHBasicTypes
 open BCHBCFiles
-open BCHConstantDefinitions
 open BCHBCTypeXml
 open BCHDemangler
 open BCHFunctionSummary
@@ -342,10 +341,10 @@ object (self)
 	  let root = doc#getRoot in
 	  if root#hasOneTaggedChild "symbolic-constants" then
 	    let node = root#getTaggedChild "symbolic-constants" in
-	    read_xml_symbolic_constants node
+	    BCHConstantDefinitions.read_xml_symbolic_constants node
 	  else if root#hasOneTaggedChild "symbolic-flags" then
 	    let node = root#getTaggedChild "symbolic-flags" in
-	    read_xml_symbolic_flags node
+	    BCHConstantDefinitions.read_xml_symbolic_flags node
 	  else
 	    raise
               (BCH_failure