CHB:ARM: disable hearistic for finding non-returning functions

static-analysis-engineering · Nov 27, 2024 · a2f4a42 · a2f4a42
1 parent f2525b1
commit a2f4a42
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 48 deletions.
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20241125"
-  ~date:"2024-11-25"
+  ~version:"0.6.0_20241127"
+  ~date:"2024-11-27"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml
@@ -56,7 +56,6 @@ open BCHELFTypes
 open BCHARMAssemblyFunctions
 open BCHARMAssemblyInstruction
 open BCHARMAssemblyInstructions
-open BCHARMCallSitesRecords
 open BCHARMInstructionAggregate
 open BCHARMPseudocode
 open BCHARMOpcodeRecords
@@ -455,6 +454,18 @@ let get_so_target (tgtaddr:doubleword_int) (_instr:arm_assembly_instruction_int)
     None
 
 
+let register_non_returning_functions () =
+  List.map (fun fndata ->
+      if fndata#is_non_returning then
+        ()
+      else if fndata#has_name then
+        let fname = fndata#get_function_name in
+        if function_summary_library#has_so_function fname then
+          let fsum = function_summary_library#get_so_function fname in
+          if fsum#is_nonreturning then
+            fndata#set_non_returning) functions_data#get_functions
+
+
 (* can be used before functions have been constructed *)
 let is_nr_call_instruction (instr:arm_assembly_instruction_int) =
   match instr#get_opcode with
@@ -947,9 +958,11 @@ let construct_functions_arm ?(construct_all_functions=false) () =
     List.iter
       (fun dw -> ignore (functions_data#add_function dw))
       (List.map (fun s -> TR.tget_ok (string_to_doubleword s)) fns_included) in
+  let _ = register_non_returning_functions () in
   let _ = collect_call_targets () in
   let _ = set_block_boundaries () in
   let _ = pr_timing [STR "block boundaries set"] in
+  (* Disabled for now; it generates too many spurious non-returning functions.
   let _ = !arm_assembly_instructions#collect_callsites in
   let _ = pr_timing [STR "callsites collected"] in
   let _ =
@@ -958,7 +971,7 @@ let construct_functions_arm ?(construct_all_functions=false) () =
         if functions_data#is_function_entry_point faddr then
           let fndata = functions_data#get_function faddr in
           fndata#set_non_returning) nonrfns in
-  let _ = pr_timing [STR "non-returning functions set"] in
+  let _ = pr_timing [STR "non-returning functions set"] in *)
   let fnentrypoints =
     if ((List.length fns_included) = 0) || construct_all_functions then
       functions_data#get_function_entry_points

diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -643,13 +643,14 @@ let translate_arm_instruction
     | Some dw -> (get_aggregate dw)#is_jumptable
     | _ -> false in
   let check_storage (_op: arm_operand_int) (v: variable_t) =
-    if (floc#env#is_unknown_memory_variable v) || v#isTemporary then
-      ch_error_log#add
-        "unknown storage location"
-        (LBLOCK [
-             floc#l#toPretty;
-             STR "  ";
-             STR (arm_opcode_to_string instr#get_opcode)]) in
+    if BCHSystemSettings.system_settings#collect_data then
+      if (floc#env#is_unknown_memory_variable v) || v#isTemporary then
+        ch_error_log#add
+          "unknown storage location"
+          (LBLOCK [
+               floc#l#toPretty;
+               STR "  ";
+               STR (arm_opcode_to_string instr#get_opcode)]) in
 
   let calltgt_cmds (_tgt: arm_operand_int): cmd_t list =
     let callargs = floc#get_call_arguments in
@@ -2803,18 +2804,19 @@ let translate_arm_instruction
          let xrn = rewrite_expr floc (rn#to_expr floc) in
          let xrm = rewrite_expr floc (rm#to_expr floc) in
          begin
-           ch_error_log#add
-             "assignment to unknown memory"
-             (LBLOCK [
-                  floc#l#toPretty;
-                  STR " STR [";
-                  rn#toPretty;
-                  STR ", ";
-                  rm#toPretty;
-                  STR "]; base: ";
-                  x2p xrn;
-                  STR ", offset: ";
-                  x2p xrm]);
+           (if BCHSystemSettings.system_settings#collect_data then
+              ch_error_log#add
+                "assignment to unknown memory"
+                (LBLOCK [
+                     floc#l#toPretty;
+                     STR " STR [";
+                     rn#toPretty;
+                     STR ", ";
+                     rm#toPretty;
+                     STR "]; base: ";
+                     x2p xrn;
+                     STR ", offset: ";
+                     x2p xrm]));
            []
          end
        else
@@ -2870,18 +2872,19 @@ let translate_arm_instruction
          let xrn = rewrite_expr floc (rn#to_expr floc) in
          let xrm = rewrite_expr floc (rm#to_expr floc) in
          begin
-           ch_error_log#add
-             "assignment to unknown memory"
-             (LBLOCK [
-                  floc#l#toPretty;
-                  STR " STRB [";
-                  rn#toPretty;
-                  STR ", ";
-                  rm#toPretty;
-                  STR "]; base: ";
-                  x2p xrn;
-                  STR ", offset: ";
-                  x2p xrm]);
+           (if BCHSystemSettings.system_settings#collect_data then
+              ch_error_log#add
+                "assignment to unknown memory"
+                (LBLOCK [
+                     floc#l#toPretty;
+                     STR " STRB [";
+                     rn#toPretty;
+                     STR ", ";
+                     rm#toPretty;
+                     STR "]; base: ";
+                     x2p xrn;
+                     STR ", offset: ";
+                     x2p xrm]));
            []
          end
        else
@@ -3033,18 +3036,19 @@ let translate_arm_instruction
          let xrn = rewrite_expr floc (rn#to_expr floc) in
          let xrm = rewrite_expr floc (rm#to_expr floc) in
          begin
-           ch_error_log#add
-             "assignment to unknown memory"
-             (LBLOCK [
-                  floc#l#toPretty;
-                  STR " STRH [";
-                  rn#toPretty;
-                  STR ", ";
-                  rm#toPretty;
-                  STR "]; base: ";
-                  x2p xrn;
-                  STR ", offset: ";
-                  x2p xrm]);
+           (if BCHSystemSettings.system_settings#collect_data then
+              ch_error_log#add
+                "assignment to unknown memory"
+                (LBLOCK [
+                     floc#l#toPretty;
+                     STR " STRH [";
+                     rn#toPretty;
+                     STR ", ";
+                     rm#toPretty;
+                     STR "]; base: ";
+                     x2p xrn;
+                     STR ", offset: ";
+                     x2p xrm]));
            []
          end
        else
@@ -3069,7 +3073,8 @@ let translate_arm_instruction
        if mem#is_offset_address_writeback then
          let addr_r = mem#to_updated_offset_address floc in
          log_tfold_default
-           (log_error "invalid write-back address" ((p2s floc#l#toPretty) ^ ": STRH"))
+           (log_error
+              "invalid write-back address" ((p2s floc#l#toPretty) ^ ": STRH"))
            (fun (_, addr) ->
              let rnreg = rn#to_register in
              let (vrn, ucmds) =