diff --git a/CodeHawk/CHB/bchanalyze/Makefile b/CodeHawk/CHB/bchanalyze/Makefile index 4d5162d5..c428afca 100644 --- a/CodeHawk/CHB/bchanalyze/Makefile +++ b/CodeHawk/CHB/bchanalyze/Makefile @@ -41,8 +41,6 @@ MLIS := \ bCHExtractInvariants \ bCHAnalyzeProcedure \ bCHReachingDefs \ - bCHDefUse \ - bCHDefUseHigh \ bCHFileIO \ bCHTrace \ bCHAnalyzeApp \ @@ -56,8 +54,6 @@ SOURCES := \ bCHExtractInvariants \ bCHAnalyzeProcedure \ bCHReachingDefs \ - bCHDefUse \ - bCHDefUseHigh \ bCHFileIO \ bCHTrace \ bCHAnalyzeApp \ diff --git a/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml b/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml index 97816f93..fbadfb82 100644 --- a/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml +++ b/CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml @@ -79,8 +79,6 @@ open BCHTranslatePowerToCHIF (* bchanalyze *) open BCHAnalyzeProcedure -open BCHDefUse -open BCHDefUseHigh open BCHExtractInvariants open BCHFileIO open BCHReachingDefs @@ -356,24 +354,16 @@ let analyze_mips_function faddr f count = else pr_debug [STR " ... and valuesets"]); (if system_settings#generate_varinvs then - begin - analyze_procedure_with_reaching_defs - proc mips_chif_system#get_mips_system; - analyze_procedure_with_def_use proc mips_chif_system#get_mips_system; - analyze_procedure_with_def_use_high proc - mips_chif_system#get_mips_system - end); + analyze_procedure_with_reaching_defs + proc mips_chif_system#get_mips_system); (if !dointervals then extract_ranges finfo bb_invariants#get_invariants); (if !dorelational then extract_linear_equalities finfo bb_invariants#get_invariants); (if !dovaluesets then extract_valuesets finfo bb_invariants#get_invariants); (if system_settings#generate_varinvs then - begin - extract_reaching_defs finfo bb_invariants#get_invariants; - extract_def_use finfo bb_invariants#get_invariants; - extract_def_use_high finfo bb_invariants#get_invariants - end); + extract_reaching_defs finfo bb_invariants#get_invariants); + (try resolve_indirect_mips_calls f with IO.No_more_input -> @@ -533,16 +523,7 @@ let analyze_arm_function faddr f count = begin 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; - (if islarge then - chlog#add "skip def-use" (faddr#toPretty) - else - analyze_procedure_with_def_use proc arm_chif_system#get_arm_system); - (if islarge then - chlog#add "skip def-use-high" (faddr#toPretty) - else - analyze_procedure_with_def_use_high - proc arm_chif_system#get_arm_system) + proc arm_chif_system#get_arm_system end); extract_ranges finfo bb_invariants#get_invariants; extract_linear_equalities finfo bb_invariants#get_invariants; @@ -550,9 +531,7 @@ let analyze_arm_function faddr f count = (if system_settings#generate_varinvs then begin 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; - extract_def_use_high finfo bb_invariants#get_invariants + extract_flag_reaching_defs finfo bb_invariants#get_invariants end); finfo#reset_invariants; save_function_invariants finfo; @@ -660,14 +639,10 @@ let analyze_pwr_function analyze_procedure_with_linear_equalities proc pwr_chif_system#get_pwr_system; analyze_procedure_with_valuesets proc pwr_chif_system#get_pwr_system; analyze_procedure_with_reaching_defs proc pwr_chif_system#get_pwr_system; - analyze_procedure_with_def_use proc pwr_chif_system#get_pwr_system; - analyze_procedure_with_def_use_high proc pwr_chif_system#get_pwr_system; extract_ranges finfo bb_invariants#get_invariants; extract_reaching_defs finfo bb_invariants#get_invariants; extract_linear_equalities finfo bb_invariants#get_invariants; extract_valuesets finfo bb_invariants#get_invariants; - extract_def_use finfo bb_invariants#get_invariants; - extract_def_use_high finfo bb_invariants#get_invariants; finfo#reset_invariants; finfo#save; save_function_invariants finfo; diff --git a/CodeHawk/CHB/bchanalyze/bCHDefUse.ml b/CodeHawk/CHB/bchanalyze/bCHDefUse.ml deleted file mode 100644 index 37299aed..00000000 --- a/CodeHawk/CHB/bchanalyze/bCHDefUse.ml +++ /dev/null @@ -1,294 +0,0 @@ -(* ============================================================================= - 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 - 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -(* chlib *) -open CHAtlas -open CHCommon -open CHIterator -open CHLanguage -open CHNonRelationalDomainNoArrays -open CHNonRelationalDomainValues -open CHSymbolicSets -open CHPretty - -(* bchlib *) -open BCHBasicTypes -open BCHLibTypes - -(* bchanalyze *) -open BCHAnalyzeProcedure - -[@@@warning "-27"] - -module H = Hashtbl -module LF = CHOnlineCodeSet.LanguageFactory - - -class def_use_domain_no_arrays_t = -object (self: 'a) - - inherit non_relational_domain_t - - method private getValue' v = - let v_value = self#getValue v in - match v_value#getValue with - | SYM_SET_VAL i -> i - | TOP_VAL -> topSymbolicSet - | _ -> - raise - (CHFailure - (LBLOCK [ - STR "Symbolic set expected. "; - v#toPretty; - STR ": "; - v_value#toPretty])) - - 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 private importValue v = - new non_relational_domain_value_t (SYM_SET_VAL (v#toSymbolicSet)) - - method private analyzeFwd' (cmd: (code_int, cfg_int) command_t) = - if bottom then - self#mkBottom - else - let table' = table#clone in - let default () = - {< table = table' >} in - match cmd with - | ABSTRACT_VARS l -> - begin - self#abstractVariables table' l; - default() - end - | ASSIGN_SYM (x, SYM s) -> - let x_s = self#getValue' x in - let x_s' = x_s#delta ([s]) in - if x_s'#isBottom || x_s'#isTop then - begin - table'#remove x; - default () - end - else - begin - self#setValue' table' x x_s'; - default() - end - | _ -> - default () - - method private analyzeBwd' (cmd: (code_int, cfg_int) command_t) = - if bottom then - self#mkBottom - else - let table' = table#clone in - let default () = - {< table = table' >} in - match cmd with - | ABSTRACT_VARS l -> - begin - self#abstractVariables table' l; - default () - end - | ASSIGN_SYM (x, SYM s) -> - let x_s = self#getValue' x in - let x_s' = - if x_s#isTop then - new symbolic_set_t [s] - else - x_s#join (new symbolic_set_t [s]) in - begin - self#setValue' table' x x_s'; - default () - end - | _ -> - default () - - method !analyzeOperation - ~(domain_name: string) - ~(fwd_direction: bool) - ~(operation: operation_t):'a = - let name = operation.op_name#getBaseName in - let table' = table#clone in - let default () = {< table = table' >} in - match name with - | "def" | "clobber" -> - begin - List.iter (fun (_, v, _) -> - self#abstractVariables table' [v]) operation.op_args; - default () - end - - | "use" -> - let (v, sym) = - match operation.op_args with - | [(_, v, WRITE)] -> - let iaddr = List.hd operation.op_name#getAttributes in - let sym = new symbol_t iaddr in - (v, sym) - | _ -> - raise - (BCH_failure - (LBLOCK [ - STR "Error in defuse:analyzeOperation. "; - STR "Domain name: "; - STR domain_name])) in - let symbols = (self#getValue' v)#getSymbols in - (match symbols with - | TOP -> - if fwd_direction then - default () - else - begin - self#setValue' table' v (new symbolic_set_t [sym]); - default () - end - | BOTTOM -> default () - | SET s1 -> - let s1' = s1#clone in - if fwd_direction then - let _ = s1'#remove sym in - let newsyms = new symbolic_set_t s1'#toList in - begin - self#setValue' table' v newsyms; - default () - end - else - let _ = s1'#add sym in - let newsyms = new symbolic_set_t s1'#toList in - begin - self#setValue' table' v newsyms; - default () - end) - - | _ -> - default () - -end - - -let get_vardefuse (op: CHLanguage.operation_t):(variable_t * symbolic_exp_t) = - match op.op_args with - | [("dst", v, WRITE)] -> - (v, SYM (new symbol_t (List.hd op.op_name#getAttributes))) - | _ -> - raise - (BCH_failure - (LBLOCK [STR "Error in get_vardefuse"])) - - -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) = - match op.op_args with - | [(_, v, _)] -> v#toPretty - | _ -> STR "?" - - -let opsemantics (domain: string) = - fun - ~(invariant: CHAtlas.atlas_t) - ~(stable: bool) - ~(fwd_direction: bool) - ~(context: CHLanguage.symbol_t CHStack.stack_t) - ~(operation: CHLanguage.operation_t) -> - match operation.op_name#getBaseName with - | "bwd_invariant" -> - let _ = - if stable then - let iaddr = List.hd (operation.op_name#getAttributes) in - bb_invariants#add_invariant iaddr domain invariant in - invariant - | "def" | "clobber" -> - let (v, _sym) = get_vardefuse operation in - if fwd_direction then - invariant#analyzeFwd (ABSTRACT_VARS [v]) - else - invariant#analyzeBwd (ABSTRACT_VARS [v]) - | "use" -> - let (v, sym) = get_vardefuse operation in - if fwd_direction then - invariant#analyzeFwd (ASSIGN_SYM (v, sym)) - else - invariant#analyzeBwd (ASSIGN_SYM (v, sym)) - | _ -> - invariant - - -let analyze_procedure_with_def_use - (proc: procedure_int) (system: system_int) = - let strategy: iteration_strategy_t = { - widening = (fun _ -> true, ""); narrowing = (fun _ -> true)} in - let iterator = - new iterator_t - ~db_enabled:false - ~do_loop_counters:false - ~strategy - ~op_semantics:(opsemantics "defuse") system in - let code = LF.mkCode [CODE (new symbol_t "code", proc#getBody)] in - let init = [("defuse", new def_use_domain_no_arrays_t)] in - let _ = - try - iterator#runBwd - ~domains:["defuse"] - ~atlas:(new atlas_t ~sigmas:[] init) - (CODE (new symbol_t "code", code)) - with - | CHFailure p -> - raise (BCH_failure (LBLOCK [STR "Error in analyze def_use: "; p])) in - () - - -let extract_def_use - (finfo: function_info_int) - (invariants: (string, (string, atlas_t) H.t) H.t) = - H.iter (fun k v -> - if H.mem v "defuse" then - let inv = H.find v "defuse" in - let domain = inv#getDomain "defuse" in - let varObserver = domain#observer#getNonRelationalVariableObserver in - let vars = domain#observer#getObservedVariables in - List.iter (fun (v: variable_t) -> - let defuse = (varObserver v)#toSymbolicSet in - if defuse#isTop then - () - else - match defuse#getSymbols with - | SET symbols -> - let symbols = - List.sort (fun s1 s2 -> - Stdlib.compare - s1#getBaseName s2#getBaseName) symbols#toList in - finfo#fvarinv#add_def_use k v symbols - | _ -> ()) vars) invariants diff --git a/CodeHawk/CHB/bchanalyze/bCHDefUse.mli b/CodeHawk/CHB/bchanalyze/bCHDefUse.mli deleted file mode 100644 index 56ceea44..00000000 --- a/CodeHawk/CHB/bchanalyze/bCHDefUse.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* ============================================================================= - CodeHawk Binary Analyzer - Author: Henny Sipma - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2022-2023 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -(* chlib *) -open CHAtlas -open CHLanguage - -(* bchlib *) -open BCHLibTypes - - -val analyze_procedure_with_def_use: procedure_int -> system_int -> unit - -val extract_def_use: - function_info_int -> (string, (string, atlas_t) Hashtbl.t) Hashtbl.t -> unit diff --git a/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.ml b/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.ml deleted file mode 100644 index 21088779..00000000 --- a/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.ml +++ /dev/null @@ -1,291 +0,0 @@ -(* ============================================================================= - 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 - 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -(* chlib *) -open CHAtlas -open CHCommon -open CHIterator -open CHLanguage -open CHNonRelationalDomainNoArrays -open CHNonRelationalDomainValues -open CHSymbolicSets -open CHPretty - -(* bchlib *) -open BCHBasicTypes -open BCHLibTypes - -(* bchanalyze *) -open BCHAnalyzeProcedure - -[@@@warning "-27"] - -module H = Hashtbl -module LF = CHOnlineCodeSet.LanguageFactory - - -class def_use_high_domain_no_arrays_t = -object (self: 'a) - - inherit non_relational_domain_t - - method private getValue' v = - let v_value = self#getValue v in - match v_value#getValue with - | SYM_SET_VAL i -> i - | TOP_VAL -> topSymbolicSet - | _ -> - raise - (CHFailure - (LBLOCK [ - STR "Symbolic set expected. "; - v#toPretty; - STR ": "; - v_value#toPretty])) - - 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 private importValue v = - new non_relational_domain_value_t (SYM_SET_VAL (v#toSymbolicSet)) - - method private analyzeFwd' (cmd: (code_int, cfg_int) command_t) = - if bottom then - self#mkBottom - else - let table' = table#clone in - let default () = - {< table = table' >} in - match cmd with - | ABSTRACT_VARS l -> - begin - self#abstractVariables table' l; - default() - end - | ASSIGN_SYM (x, SYM s) -> - let x_s = self#getValue' x in - let x_s' = x_s#delta ([s]) in - if x_s'#isBottom || x_s#isTop then - begin - table'#remove x; - default () - end - else - begin - self#setValue' table' x x_s'; - default () - end - | _ -> - default () - - method private analyzeBwd' (cmd: (code_int, cfg_int) command_t) = - if bottom then - self#mkBottom - else - let table' = table#clone in - let default () = - {< table = table' >} in - match cmd with - | ABSTRACT_VARS l -> - begin - self#abstractVariables table' l; - default () - end - | ASSIGN_SYM (x, SYM s) -> - let x_s = self#getValue' x in - let x_s' = - if x_s#isTop then - new symbolic_set_t [s] - else - x_s#join (new symbolic_set_t [s]) in - begin - self#setValue' table' x x_s'; - default () - end - | _ -> - default () - - method !analyzeOperation - ~(domain_name: string) - ~(fwd_direction: bool) - ~(operation: operation_t):'a = - let name = operation.op_name#getBaseName in - let table' = table#clone in - let default () = {< table = table' >} in - match name with - | "def" -> - begin - List.iter (fun (_, v, _) -> - self#abstractVariables table' [v]) operation.op_args; - default () - end - - | "use_high" -> - let (v, sym) = - match operation.op_args with - | [(_, v, WRITE)] -> - let iaddr = List.hd operation.op_name#getAttributes in - let sym = new symbol_t iaddr in - (v, sym) - | _ -> - raise - (BCH_failure - (LBLOCK [ - STR "Error in defusehigh:analyzeOperation. "; - STR "Domain name: "; - STR domain_name - ])) in - let symbols = (self#getValue' v)#getSymbols in - (match symbols with - | TOP -> - if fwd_direction then - default () - else - begin - self#setValue' table' v (new symbolic_set_t [sym]); - default () - end - | BOTTOM -> default () - | SET s1 -> - let s1' = s1#clone in - if fwd_direction then - let _ = s1'#remove sym in - let newsyms = new symbolic_set_t s1'#toList in - begin - self#setValue' table' v newsyms; - default () - end - else - let _ = s1'#add sym in - let newsyms = new symbolic_set_t s1'#toList in - begin - self#setValue' table' v newsyms; - default () - end) - - | _ -> - default () - -end - - -let get_vardefuse (op: CHLanguage.operation_t):(variable_t * symbolic_exp_t) = - match op.op_args with - | [("dst", v, WRITE)] -> - (v, SYM (new symbol_t (List.hd op.op_name#getAttributes))) - | _ -> - raise - (BCH_failure - (LBLOCK [STR "Error in get_vardefuse"])) - - -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) = - match op.op_args with - | [(_, v, _)] -> v#toPretty - | _ -> STR "?" - - -let opsemantics (domain: string) = - fun - ~(invariant: CHAtlas.atlas_t) - ~(stable: bool) - ~(fwd_direction: bool) - ~(context: CHLanguage.symbol_t CHStack.stack_t) - ~(operation: CHLanguage.operation_t) -> - match operation.op_name#getBaseName with - | "bwd_invariant" -> - let _ = - if stable then - let iaddr = List.hd (operation.op_name#getAttributes) in - bb_invariants#add_invariant iaddr domain invariant in - invariant - | "def" | "clobber" -> - let (v, _sym) = get_vardefuse operation in - if fwd_direction then - invariant#analyzeFwd (ABSTRACT_VARS [v]) - else - invariant#analyzeBwd (ABSTRACT_VARS [v]) - | "use_high" -> - let (v, sym) = get_vardefuse operation in - if fwd_direction then - invariant#analyzeFwd (ASSIGN_SYM (v, sym)) - else - invariant#analyzeBwd (ASSIGN_SYM (v, sym)) - | _ -> - invariant - - -let analyze_procedure_with_def_use_high - (proc: procedure_int) (system: system_int) = - let strategy: iteration_strategy_t = { - widening = (fun _ -> true, ""); narrowing = (fun _ -> true)} in - let iterator = - new iterator_t - ~db_enabled:false - ~do_loop_counters:false - ~strategy - ~op_semantics:(opsemantics "defusehigh") system in - let code = LF.mkCode [CODE (new symbol_t "code", proc#getBody)] in - let init = [("defusehigh", new def_use_high_domain_no_arrays_t)] in - let _ = - iterator#runBwd - ~domains:["defusehigh"] - ~atlas:(new atlas_t ~sigmas:[] init) - (CODE (new symbol_t "code", code)) in - () - - -let extract_def_use_high - (finfo: function_info_int) - (invariants: (string, (string, atlas_t) H.t) H.t) = - H.iter (fun k v -> - if H.mem v "defusehigh" then - let inv = H.find v "defusehigh" in - let domain = inv#getDomain "defusehigh" in - let varObserver = domain#observer#getNonRelationalVariableObserver in - let vars = domain#observer#getObservedVariables in - List.iter (fun (v: variable_t) -> - let defuse = (varObserver v)#toSymbolicSet in - if defuse#isTop then - () - else - match defuse#getSymbols with - | SET symbols -> - let symbols = - List.sort (fun s1 s2 -> - Stdlib.compare - s1#getBaseName s2#getBaseName) symbols#toList in - finfo#fvarinv#add_def_use_high k v symbols - | _ -> ()) vars) invariants diff --git a/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.mli b/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.mli deleted file mode 100644 index 19c92d65..00000000 --- a/CodeHawk/CHB/bchanalyze/bCHDefUseHigh.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* ============================================================================= - 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 - 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 - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -(* chlib *) -open CHAtlas -open CHLanguage - -(* bchlib *) -open BCHLibTypes - - -val analyze_procedure_with_def_use_high: procedure_int -> system_int -> unit - -val extract_def_use_high: - function_info_int -> (string, (string, atlas_t) Hashtbl.t) Hashtbl.t -> unit diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index 6e04edb5..61baf471 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -61,7 +61,6 @@ object (self) val mutable names = [] val mutable non_returning = false - val mutable maybe_non_returning = false val mutable incomplete = false val mutable ida_provided = false val mutable user_provided = false @@ -79,8 +78,6 @@ object (self) method set_non_returning = non_returning <- true - method set_maybe_non_returning = maybe_non_returning <- true - method set_inlined = inlined <- true method set_by_preamble = by_preamble <- true @@ -171,8 +168,6 @@ object (self) method is_non_returning = non_returning - method is_maybe_non_returning = maybe_non_returning - method is_incomplete = incomplete method is_virtual = virtual_function diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 6a43e2c0..9342eb43 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1504,7 +1504,6 @@ class type function_data_int = (* setters *) method set_function_type: btype_t -> unit method set_non_returning: unit - method set_maybe_non_returning: unit method add_name: string -> unit method set_ida_provided: unit method set_user_provided: unit @@ -1542,7 +1541,6 @@ class type function_data_int = method has_callsites: bool method has_path_contexts: bool method is_non_returning: bool - method is_maybe_non_returning: bool method is_incomplete: bool method is_ida_provided: bool method is_user_provided: bool @@ -1610,7 +1608,34 @@ end (** {1 Invariants}*) -(** {2 Variable invariants} *) +(** {2 Variable invariants} + + Variable invariants are symbolic invariants including: + - reaching definitions + - flag reaching definitions (for architectures with processor flags) + - def-use relationships + - def-use-high relationships + + The reaching definitions are the traditional relationships between a + variable use and all locations where that variable may have been defined. + + The def-use relationships are the traditional relationships between + a variable definition and all locations where that variable may be used. + + The def-use-high relationships are similar to the def-use relationships, + but are only computed for variables that would appear in a source-code + lifting. + + The reaching definitions are computed directly by forward abstract + interpretation in a symbolic domain with the hooks embedded in the same + CHIF representation that is used for the regular (value) invariant + generation. + + The def-use and def-use-high relationships (normally computed by backward + analysis) are instead derived directly from the reaching definitions by + recording the uses (and high-uses) in the functioninfo and using these to + filter out the reverse relationships of the reaching definitions. +*) (** Pairing of a variable with a set of locations represented by symbols.*) type vardefuse_t = variable_t * symbol_t list @@ -1626,7 +1651,7 @@ type var_invariant_fact_t = (** list of locations where a high-level variable is used *) -(** Single variable invariant at a particular location.*) +(** Single variable invariant at a particular location (immutable).*) class type var_invariant_int = object ('a) method index: int @@ -1651,7 +1676,15 @@ class type var_invariant_int = end -(** All variable invariants at a particular location.*) +(** All variable invariants at a particular location. + + Mutable class that collects variable invariants at a particular location + (instruction address) in the code. Reaching defs are added as complete + facts, def-use facts are constructed one use-location at the time, as they + are retrieved from the reaching def facts. The collect_use_facts method + is called to package up these def-use facts when all reaching defs have + been processed. +*) class type location_var_invariant_int = object method reset: unit diff --git a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml index fe941cf2..b842819a 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml @@ -192,7 +192,6 @@ object (self) val mutable user_call_targets = 0 val mutable user_structs = 0 val mutable user_nonreturning = 0 - val mutable user_maybe_nonreturning = 0 val mutable user_classes = 0 val mutable encodings = [] val mutable inlined_functions = [] @@ -701,13 +700,6 @@ object (self) user_nonreturning <- List.length nrnode#getChildren end); - (if hasc "maybe-non-returning-functions" then - let mnrnode = getc "maybe-non-returning-functions" in - begin - self#read_xml_user_maybe_nonreturning_functions mnrnode; - user_maybe_nonreturning <- List.length mnrnode#getChildren - end); - (if hasc "non-returning-calls" then let nrnode = getc "non-returning-calls" in begin @@ -1465,22 +1457,6 @@ object (self) chlog#add "user-declared non-returning function" (geta n)#toPretty in fd#set_non_returning) (getcc "nr") - method private read_xml_user_maybe_nonreturning_functions - (node:xml_element_int) = - let geta n = - fail_tvalue - (trerror_record - (LBLOCK [ - STR "read_xml_user_maybe_nonreturning_functions: "; - STR (n#getAttribute "a")])) - (string_to_doubleword (n#getAttribute "a")) in - let getcc = node#getTaggedChildren in - List.iter (fun n -> - let fd = functions_data#add_function (geta n) in - let _ = - chlog#add "user-declared non-returning function" (geta n)#toPretty in - fd#set_maybe_non_returning) (getcc "mnr") - method private read_xml_nonreturning_calls (node:xml_element_int) = let geta n tag = geta_fail "read_xml_nonreturning_functions" n tag in let getcc = node#getTaggedChildren in diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index a3a0cfce..c6c19ac2 100644 --- 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_20241118" - ~date:"2024-11-18" + ~version:"0.6.0_20241119" + ~date:"2024-11-19" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml index 4f7a0668..09d97408 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml @@ -81,15 +81,6 @@ let get_successors [] (get_next_valid_instruction_address iaddr) in - let is_maybe_non_returning_call_instr = - match instr#get_opcode with - | BranchLink (ACCAlways, tgt) - | BranchLinkExchange (ACCAlways, tgt) when tgt#is_absolute_address -> - let tgtaddr = tgt#get_absolute_address in - ((functions_data#is_function_entry_point tgtaddr) - && (functions_data#get_function tgtaddr)#is_maybe_non_returning) - | _ -> false in - let next_from (va: doubleword_int) = log_tfold_default (mk_tracelog_spec @@ -135,12 +126,6 @@ let get_successors | Pop (_, _, rl, _) when rl#includes_pc -> (next ()) @ [wordmax] - (* maybe non-returning call instruction *) - | BranchLink _ | BranchLinkExchange _ - when is_maybe_non_returning_call_instr -> - let _ = chlog#add "maybe non returning" (iaddr#toPretty) in - (next ()) @ [wordmax] - (* return via LDM/LDMDB/LDMDA/LDMIB *) | LoadMultipleDecrementBefore (_, ACCAlways, _, rl, _) | LoadMultipleDecrementAfter (_, ACCAlways, _, rl, _) diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml index c91ba5da..70df91a6 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml @@ -466,17 +466,6 @@ let is_nr_call_instruction (instr:arm_assembly_instruction_int) = | _ -> false -let is_maybe_nr_call_instruction (instr: arm_assembly_instruction_int) = - match instr#get_opcode with - | BranchLink (ACCAlways, tgt) - | BranchLinkExchange (ACCAlways, tgt) when tgt#is_absolute_address -> - let tgtaddr = tgt#get_absolute_address in - ((functions_data#is_function_entry_point tgtaddr) - && (functions_data#get_function tgtaddr)#is_maybe_non_returning) - | _ -> false - - - let collect_function_entry_points () = let addresses = new DoublewordCollections.set_t in begin @@ -693,8 +682,7 @@ let set_block_boundaries () = *) | BranchLink _ | BranchLinkExchange _ - when is_nr_call_instruction instr - || is_maybe_nr_call_instruction instr -> + when is_nr_call_instruction instr -> set_block_entry (va#add_int 4) | _ -> ()) diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 3d80a199..557ab13e 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -50,7 +50,6 @@ open BCHCPURegisters open BCHDoubleword open BCHFloc open BCHFtsParameter -open BCHFunctionData open BCHFunctionInfo open BCHFunctionInterface open BCHLibTypes @@ -493,7 +492,6 @@ let translate_arm_instruction ~(funloc:location_int) ~(codepc:arm_code_pc_int) ~(blocklabel:symbol_t) - ~(exitlabel:symbol_t) ~(cmds:cmd_t list) = let (ctxtiaddr, instr) = codepc#get_next_instruction in let faddr = funloc#f in @@ -634,15 +632,6 @@ let translate_arm_instruction (floc#env#variables_in_expr xs) in vars @ acc) [] xprs in - let is_maybe_non_returning_call_instr = - match instr#get_opcode with - | BranchLink (ACCAlways, tgt) - | BranchLinkExchange (ACCAlways, tgt) when tgt#is_absolute_address -> - let tgtaddr = tgt#get_absolute_address in - ((functions_data#is_function_entry_point tgtaddr) - && (functions_data#get_function tgtaddr)#is_maybe_non_returning) - | _ -> false in - let flagdefs = let flags_set = get_arm_flags_set instr#get_opcode in List.map (fun f -> finfo#env#mk_flag_variable (ARMCCFlag f)) flags_set in @@ -1136,17 +1125,6 @@ let translate_arm_instruction * SelectInstrSet(targetInstrSet); * BranchWritePC(targetAddress); * ------------------------------------------------------------------------ *) - | BranchLink (_c, tgt) when is_maybe_non_returning_call_instr -> - (* TODO: incorporate condition *) - let elseaddr = codepc#get_false_branch_successor in - let callcmds = calltgt_cmds tgt in - let cmds = cmds @ (invop :: callcmds) @ [bwdinvop] @ pcassign in - let transaction = package_transaction finfo blocklabel cmds in - let elselabel = make_code_label elseaddr in - let nodes = [(blocklabel, [transaction])] in - let edges = [(blocklabel, exitlabel); (blocklabel, elselabel)] in - (nodes, edges, []) - | BranchLink (c, tgt) | BranchLinkExchange (c, tgt) when tgt#is_absolute_address -> if instr#is_inlined_call then @@ -4062,8 +4040,7 @@ object (self) let rec aux cmds = let (nodes,edges,newcmds) = try - translate_arm_instruction - ~funloc ~codepc ~blocklabel ~exitlabel ~cmds + translate_arm_instruction ~funloc ~codepc ~blocklabel ~cmds with | BCH_failure p -> let msg = diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli index 6e287aed..f5e94708 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli @@ -40,7 +40,6 @@ val translate_arm_instruction: funloc:location_int -> codepc:arm_code_pc_int -> blocklabel:symbol_t - -> exitlabel:symbol_t -> cmds:cmd_t list -> ((symbol_t * (code_t, 'a) command_t list) list