CHT: fix warnings and add tests to dune files

static-analysis-engineering · Oct 7, 2024 · c5e6d7a · c5e6d7a
1 parent 3f1194e
commit c5e6d7a
Show file tree

Hide file tree

Showing 25 changed files with 62 additions and 219 deletions.
diff --git a/.gitignore b/.gitignore
@@ -25,6 +25,7 @@ _build/
 *.mli~
 *.sh~
 *.yaml~
+*.i~
 .gitignore~
 
 # binary analyzer executables

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml
@@ -58,12 +58,12 @@ let get_arm_int_param_next_state_test () =
     TS.new_testsuite
       (testname ^ "_get_int_paramloc_next_test") lastupdated;
 
-    List.iter (fun (title, nxtreg, xlocreg, xnxtreg, xnxtoff) ->
+    List.iter (fun (title, nxtreg, _xlocreg, xnxtreg, xnxtoff) ->
         TS.add_simple_test
           ~title
           (fun () ->
             let aas = {aas_start_state with aas_next_core_reg = Some nxtreg} in
-            let (par, naas) = get_arm_int_param_next_state 4 "name" t_int aas 1 in
+            let (_par, naas) = get_arm_int_param_next_state 4 "name" t_int aas 1 in
             let xnaas =
               {aas_start_state with
                 aas_next_core_reg = xnxtreg; aas_next_offset = xnxtoff} in
@@ -76,7 +76,7 @@ let get_arm_int_param_next_state_test () =
         let aas =
           {aas_start_state with
             aas_next_core_reg = None; aas_next_offset = Some 0} in
-        let (par, naas) = get_arm_int_param_next_state 4 "name" t_int aas 1 in
+        let (_par, naas) = get_arm_int_param_next_state 4 "name" t_int aas 1 in
         let xnaas = {aas with aas_next_offset = Some 4} in
         BA.equal_arm_argument_state ~expected:xnaas ~received:naas ());
 
@@ -105,14 +105,14 @@ let get_arm_struct_field_locations_test () =
 
     parse_cil_file ~removeUnused:false "header.i";
 
-    List.iter (fun (title, locations) ->
+    List.iter (fun (title, _locations) ->
         TS.add_simple_test
           ~title
           (fun () ->
             let cinfo = bcfiles#get_compinfo_by_name title in
             let finfo = List.hd cinfo.bcfields in
             let aas = push_field_pos aas_start_state finfo in
-            let (locs, naas) = get_arm_struct_field_locations finfo aas in
+            let (locs, _naas) = get_arm_struct_field_locations finfo aas in
             let xlocs = [
                 mk_register_parameter_location
                   ~position:[mk_field_position cinfo.bckey 0 (get_struct_field_name finfo)]
@@ -140,7 +140,7 @@ let get_arm_struct_param_next_state_test () =
             let cinfo = bcfiles#get_compinfo_by_name title in
             let btype = get_compinfo_struct_type cinfo in
             let size = CHTraceResult.tget_ok (size_of_btype btype) in
-            let (param, naas) =
+            let (param, _naas) =
               get_arm_struct_param_next_state
                 size "arg_1" btype aas_start_state 1 in
             let xlocs =

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml
@@ -28,19 +28,12 @@
 
 (* chlib *)
 open CHNumerical
-open CHPretty
-
-(* chutil *)
-open CHLogger
-open CHPrettyUtil
 
 (* xprlib *)
 open Xprt
-open XprToPretty
 open XprTypes
 
 (* bchlib *)
-open BCHBasicTypes
 open BCHBCFiles
 open BCHBCTypes
 open BCHConstantDefinitions
@@ -49,7 +42,6 @@ open BCHFloc
 open BCHFunctionData
 open BCHFunctionInfo
 open BCHLibTypes
-open BCHMemoryReference
 
 (* bchcil *)
 open BCHParseCilFile
@@ -63,11 +55,6 @@ let testname = "bCHFlocTest"
 let lastupdated = "2024-08-20"
 
 
-let x2p = xpr_formatter#pr_expr
-let p2s = pretty_to_string
-let x2s x = p2s (x2p x)
-
-
 let decompose_memvar_address_test () =
   let faddr = "0x1d6bfc" in
   let iaddr = "0x1d6cbc" in

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFunctionInterfaceTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFunctionInterfaceTest.ml
@@ -5,7 +5,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2023  Aarno Labs LLC
+   Copyright (c) 2023-2024  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
@@ -35,10 +35,6 @@
 
 (* chlib *)
 open CHPretty
-open CHNumerical
-
-(* tchblib *)
-open TCHSpecification
 
 (* bchlib *)
 open BCHBasicTypes
@@ -181,7 +177,7 @@ let function_signature_of_bvarinfo_arm () =
               else
                 raise
                   (BCH_failure (LBLOCK [STR title; STR " not found"])) in
-            let (xresult, fintf, tsig) =
+            let (xresult, _fintf, tsig) =
               try
                 let xresult = List.map BU.convert_fts_parameter_input result in
                 let fintf = FI.bvarinfo_to_function_interface bvinfo in

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHMemoryReferenceTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHMemoryReferenceTest.ml
@@ -28,26 +28,13 @@
 
 (* chlib *)
 open CHNumerical
-open CHPretty
-
-(* chutil *)
-open CHLogger
-open CHPrettyUtil
-
-(* xprlib *)
-open Xprt
-open XprToPretty
-open XprTypes
 
 (* bchlib *)
-open BCHBasicTypes
 open BCHBCFiles
 open BCHBCTypes
 open BCHConstantDefinitions
 open BCHDoubleword
-open BCHFloc
 open BCHFunctionData
-open BCHFunctionInfo
 open BCHLibTypes
 
 (* bchcil *)
@@ -65,11 +52,6 @@ let testname = "bCHMemoryReferenceTest"
 let lastupdated = "2024-08-21"
 
 
-let x2p = xpr_formatter#pr_expr
-let p2s = pretty_to_string
-let x2s x = p2s (x2p x)
-
-
 let mk_maximal_memory_offset_test () =
   begin
 

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHTypeConstraintStoreTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHTypeConstraintStoreTest.ml
@@ -36,8 +36,6 @@ open CHPretty
 (* bchlib *)
 open BCHBasicTypes
 open BCHBCFiles
-open BCHBCTypePretty
-open BCHCPURegisters
 open BCHFunctionInterface
 open BCHLibTypes
 open BCHSystemSettings

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml
@@ -28,14 +28,8 @@
 
 (* chlib *)
 open CHNumerical
-open CHPretty
-
-(* chutil *)
-open CHPrettyUtil
 
 (* xprlib *)
-open Xprt
-open XprToPretty
 open XprTypes
 open Xsimplify
 

diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/dune b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/dune
@@ -1,3 +1,14 @@
-(tests 
-  (names bCHDoublewordTest bCHImmediateTest bCHLocationTest bCHStreamWrapperTest)
-  (libraries bchlib chlib chutil tbchlib tchlib))
+(tests
+  (names
+	bCHDoublewordTest
+	bCHImmediateTest
+	bCHLocationTest
+	bCHStreamWrapperTest
+	bCHXprUtilTest
+	bCHMemoryReferenceTest
+	bCHFunctionInterfaceTest
+	bCHARMFunctionInterfaceTest
+	bCHTypeConstraintStoreTest
+	bCHFlocTest)
+  (deps header.i decompose_array_address.i)
+  (libraries bchcil bchlib xprlib chlib chutil tbchlib tchlib txprlib))
diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml
@@ -125,7 +125,7 @@ let thumb_function_setup
       | _ -> ()
     done;
     let _ = set_block_boundaries () in
-    let _ = construct_functions_arm ~construct_all_functions:false in
+    let _ = construct_functions_arm ~construct_all_functions:false () in
     get_arm_assembly_function faddr
   end
 

diff --git a/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHDwarfTest.ml b/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHDwarfTest.ml
@@ -5,7 +5,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
  
-   Copyright (c) 2023  Aarno Labs LLC
+   Copyright (c) 2023-2024  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
@@ -26,25 +26,15 @@
    SOFTWARE.
    ============================================================================= *)
 
-(* chlib *)
-open CHPretty
-
-(* chutil *)
-open CHXmlDocument
-open CHXmlReader
-
 (* bchlib *)
-open BCHBasicTypes
 open BCHDoubleword
-open BCHLibTypes
 open BCHStreamWrapper
 
 (* bchlibelf *)
 open BCHDwarf
 open BCHDwarfTypes
 open BCHDwarfUtils
 open BCHELFDebugAbbrevSection
-open BCHELFTypes
 open BCHELFSectionHeader
 
 (* tchlib *)
@@ -169,7 +159,7 @@ let decode_variable_die_test () =
             let sh = mk_elf_section_header () in
             let section = mk_elf_debug_abbrev_section astring sh in
             let abbreventry = section#get_abbrev_entry in
-            let fabbrev = fun (i: int) -> abbreventry in
+            let fabbrev = fun (_i: int) -> abbreventry in
             let chi = make_pushback_stream ~little_endian:true istring in
             let base = TR.tget_ok (string_to_doubleword base) in
             let var =

diff --git a/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHELFDebugAbbrevSectionTest.ml b/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHELFDebugAbbrevSectionTest.ml
@@ -5,7 +5,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
  
-   Copyright (c) 2023  Aarno Labs LLC
+   Copyright (c) 2023-2024  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
@@ -26,21 +26,8 @@
    SOFTWARE.
    ============================================================================= *)
 
-(* chlib *)
-open CHPretty
-
-(* chutil *)
-open CHXmlDocument
-open CHXmlReader
-
-(* bchlib *)
-open BCHBasicTypes
-open BCHLibTypes
-
 (* bchlibelf *)
-open BCHDwarfUtils
 open BCHELFDebugAbbrevSection
-open BCHELFTypes
 open BCHELFSectionHeader
 
 (* tchlib *)

diff --git a/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHELFDebugLocSectionTest.ml b/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/bCHELFDebugLocSectionTest.ml
@@ -1,22 +1,22 @@
 (* =============================================================================
-   CodeHawk Unit Testing Framework 
+   CodeHawk Unit Testing Framework
    Author: Henny Sipma
    Adapted from: Kaputt (https://kaputt.x9c.fr/index.html)
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
-   Copyright (c) 2023  Aarno Labs LLC
+
+   Copyright (c) 2023-2024  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
    in the Software without restriction, including without limitation the rights
    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
    copies of the Software, and to permit persons to whom the Software is
    furnished to do so, subject to the following conditions:
- 
+
    The above copyright notice and this permission notice shall be included in all
    copies or substantial portions of the Software.
-  
+
    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -26,21 +26,8 @@
    SOFTWARE.
    ============================================================================= *)
 
-(* chlib *)
-open CHPretty
-
-(* chutil *)
-open CHXmlDocument
-open CHXmlReader
-
-(* bchlib *)
-open BCHBasicTypes
-open BCHLibTypes
-
 (* bchlibelf *)
-open BCHDwarfUtils
 open BCHELFDebugLocSection
-open BCHELFTypes
 open BCHELFSectionHeader
 
 (* tchlib *)
@@ -142,11 +129,12 @@ let debug_location_list_test () =
           ~title
           (fun () ->
             let bytes = bytes ^ "000000000000000000" in
-            let bytestring = U.write_hex_bytes_to_bytestring bytes in            
+            let bytestring = U.write_hex_bytes_to_bytestring bytes in
             let sectionheader = mk_elf_section_header () in
             let section = mk_elf_debug_loc_section bytestring sectionheader in
             let loclist = section#get_location_list in
-            EA.equal_debug_location_list result loclist ())) tests;
+            EA.equal_debug_location_list
+              ~expected:result ~received:loclist ())) tests;
 
     TS.launch_tests ()
   end
@@ -158,4 +146,3 @@ let () =
     debug_location_list_test ();
     TS.exit_file ()
   end
-
diff --git a/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/dune b/CodeHawk/CHT/CHB_tests/bchlibelf_tests/txbchlibelf/dune
@@ -1,7 +1,3 @@
 (tests 
   (names bCHDwarfTest bCHELFDebugAbbrevSectionTest bCHELFDebugLocSectionTest)
   (libraries bchlib bchlibelf chlib chutil tbchlibelf tchlib))
-
-(env
-  (dev
-    (flags (:standard -warn-error -A))))
-Original file line number
+Diff line change
@@ Expand Up / @@ -25,6 +25,7 @@ _build/ @@
     *.mli~
     *.sh~
     *.yaml~
+    *.i~
     .gitignore~
     # binary analyzer executables
@@ Expand Down @@