CHB: fix warnings and remove some obsolete files

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

Hide file tree

Showing 43 changed files with 431 additions and 1,114 deletions.
diff --git a/CodeHawk/CHB/bchanalyze/Makefile b/CodeHawk/CHB/bchanalyze/Makefile
@@ -43,8 +43,6 @@ MLIS := \
 	bCHReachingDefs \
 	bCHDefUse \
 	bCHDefUseHigh \
-	bCHTypeConstantsDomainNoArrays \
-	bCHDesignation \
 	bCHFileIO \
 	bCHTrace \
 	bCHAnalyzeApp \
@@ -60,8 +58,6 @@ SOURCES := \
 	bCHReachingDefs \
 	bCHDefUse \
 	bCHDefUseHigh \
-	bCHTypeConstantsDomainNoArrays \
-	bCHDesignation \
 	bCHFileIO \
 	bCHTrace \
 	bCHAnalyzeApp \

diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalysisTypes.mli b/CodeHawk/CHB/bchanalyze/bCHAnalysisTypes.mli
@@ -29,20 +29,10 @@
 
 (* chlib *)
 open CHAtlas
-open CHIntervals
 open CHLanguage
 open CHNumericalConstraints
 open CHPretty
 
-(* chutil *)
-open CHXmlDocument
-
-(* bchlib *)
-open BCHLibTypes
-
-(* bchlibx86 *)
-open BCHLibx86Types
-
 
 class type constraint_set_int =
 object ('a)

diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml b/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml
@@ -41,7 +41,6 @@ open BCHDoubleword
 open BCHLibTypes
 open BCHFunctionInfo
 open BCHMetrics
-open BCHSystemInfo
 open BCHSystemSettings
 
 (* bchlibx86 *)
@@ -68,7 +67,6 @@ open BCHARMAssemblyFunctions
 open BCHARMCHIFSystem
 open BCHARMLoopStructure
 open BCHARMMetrics
-open BCHFnARMDictionary
 open BCHTranslateARMToCHIF
 
 (* bchlibpower32 *)
@@ -83,7 +81,6 @@ open BCHTranslatePowerToCHIF
 open BCHAnalyzeProcedure
 open BCHDefUse
 open BCHDefUseHigh
-open BCHDesignation
 open BCHExtractInvariants
 open BCHFileIO
 open BCHReachingDefs
@@ -534,7 +531,6 @@ let analyze_arm_function faddr f count =
       analyze_procedure_with_valuesets proc arm_chif_system#get_arm_system;
       (if system_settings#generate_varinvs then
          begin
-           analyze_procedure_with_designations proc arm_chif_system#get_arm_system;
            analyze_procedure_with_reaching_defs proc arm_chif_system#get_arm_system;
            analyze_procedure_with_flag_reaching_defs
              proc arm_chif_system#get_arm_system;
@@ -553,7 +549,6 @@ let analyze_arm_function faddr f count =
       extract_valuesets finfo bb_invariants#get_invariants;
       (if system_settings#generate_varinvs then
          begin
-           extract_designations finfo bb_invariants#get_invariants;
            extract_reaching_defs finfo bb_invariants#get_invariants;
            extract_flag_reaching_defs finfo bb_invariants#get_invariants;
            extract_def_use finfo bb_invariants#get_invariants;

diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml b/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml
@@ -1,9 +1,9 @@
 (* =============================================================================
-   CodeHawk Binary Analyzer 
+   CodeHawk Binary Analyzer
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
+
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny B. Sipma
    Copyright (c) 2021-2024 Aarno Labs LLC
@@ -14,10 +14,10 @@
    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
@@ -39,23 +39,25 @@ open CHAnalysisSetup
 (* bchanalyze *)
 open BCHAnalysisTypes
 
+[@@@warning "-27"]
+
 module H = Hashtbl
 
 
 class bb_invariants_t:bb_invariants_int =
 object
   val invariants = H.create 3
-    
+
   method reset = H.clear invariants
-    
+
   method add_invariant (opname:string) (domain:string) (inv:atlas_t) =
     let optable = if H.mem invariants opname then
-	H.find invariants opname 
+	H.find invariants opname
       else
 	let table = H.create 1 in
-	begin H.add invariants opname table ; table end in
+	begin H.add invariants opname table; table end in
     H.replace optable domain inv
-      
+
   method get_invariants = invariants
 
   method toPretty =
@@ -69,44 +71,48 @@ object
               result := p :: !result) varinvs) invariants;
       LBLOCK (List.rev !result)
     end
-    
+
 end
 
 let bb_invariants = new bb_invariants_t
 
-let default_opsemantics domain = 
+let default_opsemantics domain =
   fun ~invariant ~stable ~fwd_direction ~context ~operation ->
-    let _ = if stable then 
-	if operation.op_name#getBaseName = "invariant" then
-	  bb_invariants#add_invariant (List.hd (operation.op_name#getAttributes)) domain invariant in
+  let _ =
+    if stable then
+      if operation.op_name#getBaseName = "invariant" then
+	bb_invariants#add_invariant
+          (List.hd (operation.op_name#getAttributes)) domain invariant in
     invariant
 
-let analyze_procedure_with_linear_equalities (proc:procedure_int) (system:system_int) =
+let analyze_procedure_with_linear_equalities
+      (proc:procedure_int) (system:system_int) =
   let analysis_setup = mk_analysis_setup () in
   begin
-    analysis_setup#addLinearEqualities ;
-    analysis_setup#setOpSemantics (default_opsemantics "karr") ;
-    analysis_setup#analyze_procedure system proc 
+    analysis_setup#addLinearEqualities;
+    analysis_setup#setOpSemantics (default_opsemantics "karr");
+    analysis_setup#analyze_procedure system proc
   end
 
 let analyze_procedure_with_intervals (proc:procedure_int) (system:system_int) =
   let analysis_setup = mk_analysis_setup () in
   begin
-    analysis_setup#addIntervals ;
-    analysis_setup#setOpSemantics (default_opsemantics "intervals") ;
-    analysis_setup#analyze_procedure system proc 
+    analysis_setup#addIntervals;
+    analysis_setup#setOpSemantics (default_opsemantics "intervals");
+    analysis_setup#analyze_procedure system proc
   end
-    
+
 let analyze_procedure_with_valuesets (proc:procedure_int) (system:system_int) =
   let analysis_setup = mk_analysis_setup  () in
   begin
-    analysis_setup#addValueSets ;
-    analysis_setup#setOpSemantics (default_opsemantics "valuesets") ;
+    analysis_setup#addValueSets;
+    analysis_setup#setOpSemantics (default_opsemantics "valuesets");
     analysis_setup#analyze_procedure system proc
   end
 
 
-let analyze_procedure_with_symbolic_sets (proc: procedure_int) (system: system_int) =
+let analyze_procedure_with_symbolic_sets
+      (proc: procedure_int) (system: system_int) =
   let analysis_setup = mk_analysis_setup () in
   begin
     analysis_setup#addDomain "symbolicsets" (new symbolic_sets_domain_no_arrays_t);

diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.mli b/CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.mli
@@ -1,23 +1,23 @@
 (* =============================================================================
-   CodeHawk Binary Analyzer 
+   CodeHawk Binary Analyzer
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
+
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2022 Aarno Labs LLC
+   Copyright (c) 2021-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
@@ -29,14 +29,17 @@
 
 (* chlib *)
 open CHLanguage
-   
+
 (* bchanalyze *)
 open BCHAnalysisTypes
 
 
 val bb_invariants: bb_invariants_int
 
 val analyze_procedure_with_linear_equalities: procedure_int -> system_int -> unit
+
 val analyze_procedure_with_intervals: procedure_int -> system_int -> unit
+
 val analyze_procedure_with_valuesets: procedure_int -> system_int -> unit
+
 val analyze_procedure_with_symbolic_sets: procedure_int -> system_int -> unit
diff --git a/CodeHawk/CHB/bchanalyze/bCHDefUse.ml b/CodeHawk/CHB/bchanalyze/bCHDefUse.ml
@@ -1,9 +1,9 @@
 (* =============================================================================
-   CodeHawk Binary Analyzer 
+   CodeHawk Binary Analyzer
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
+
    Copyright (c) 2022-2024  Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -12,10 +12,10 @@
    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
@@ -28,12 +28,10 @@
 (* chlib *)
 open CHAtlas
 open CHCommon
-open CHDomain
 open CHIterator
 open CHLanguage
 open CHNonRelationalDomainNoArrays
 open CHNonRelationalDomainValues
-open CHOnlineCodeSet
 open CHSymbolicSets
 open CHPretty
 
@@ -44,6 +42,7 @@ open BCHLibTypes
 (* bchanalyze *)
 open BCHAnalyzeProcedure
 
+[@@@warning "-27"]
 
 module H = Hashtbl
 module LF = CHOnlineCodeSet.LanguageFactory
@@ -71,7 +70,7 @@ object (self: 'a)
   method private setValue' t v x =
     self#setValue t v (new non_relational_domain_value_t (SYM_SET_VAL x))
 
-  method special cmd args = {< >}
+  method special _cmd _args = {< >}
 
   method private importValue v =
     new non_relational_domain_value_t (SYM_SET_VAL (v#toSymbolicSet))
@@ -132,7 +131,7 @@ object (self: 'a)
       | _ ->
          default ()
 
-  method analyzeOperation
+  method !analyzeOperation
            ~(domain_name: string)
            ~(fwd_direction: bool)
            ~(operation: operation_t):'a =
@@ -146,7 +145,7 @@ object (self: 'a)
              self#abstractVariables table' [v]) operation.op_args;
          default ()
        end
-         
+
     | "use" ->
        let (v, sym) =
          match operation.op_args with
@@ -157,7 +156,10 @@ object (self: 'a)
          | _ ->
             raise
               (BCH_failure
-                 (LBLOCK [STR "Error in defuse:analyzeOperation"])) in
+                 (LBLOCK [
+                      STR "Error in defuse:analyzeOperation. ";
+                      STR "Domain name: ";
+                      STR domain_name])) in
        let symbols = (self#getValue' v)#getSymbols in
        (match symbols with
         | TOP ->
@@ -185,11 +187,11 @@ object (self: 'a)
                self#setValue' table' v newsyms;
                default ()
              end)
-         
+
     | _ ->
        default ()
 
-end          
+end
 
 
 let get_vardefuse (op: CHLanguage.operation_t):(variable_t * symbolic_exp_t) =
@@ -202,13 +204,13 @@ let get_vardefuse (op: CHLanguage.operation_t):(variable_t * symbolic_exp_t) =
           (LBLOCK [STR "Error in get_vardefuse"]))
 
 
-let symbolic_exp_to_pretty (s: symbolic_exp_t) =
+let _symbolic_exp_to_pretty (s: symbolic_exp_t) =
   match s with
   | SYM sym -> sym#toPretty
   | SYM_VAR v -> v#toPretty
 
 
-let get_opvar (op: operation_t) =
+let _get_opvar (op: operation_t) =
   match op.op_args with
   | [(_, v, _)] -> v#toPretty
   | _ -> STR "?"
@@ -229,7 +231,7 @@ let opsemantics (domain: string) =
          bb_invariants#add_invariant iaddr domain invariant in
      invariant
   | "def" | "clobber" ->
-     let (v, sym) = get_vardefuse operation in
+     let (v, _sym) = get_vardefuse operation in
      if fwd_direction then
        invariant#analyzeFwd (ABSTRACT_VARS [v])
      else
@@ -240,7 +242,7 @@ let opsemantics (domain: string) =
        invariant#analyzeFwd (ASSIGN_SYM (v, sym))
      else
        invariant#analyzeBwd (ASSIGN_SYM (v, sym))
-  | s ->
+  | _ ->
      invariant