diff --git a/.github/workflows/dune.yaml b/.github/workflows/dune.yaml index 5fc9d68fc..63187bb20 100644 --- a/.github/workflows/dune.yaml +++ b/.github/workflows/dune.yaml @@ -9,11 +9,7 @@ jobs: strategy: matrix: ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - - "5.0.0" - - "5.1.1" + - "5.2.0" steps: - uses: actions/checkout@v1 - uses: ocaml/setup-ocaml@v3 @@ -43,11 +39,7 @@ jobs: strategy: matrix: ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - - "5.0.0" - - "5.1.1" + - "5.2.0" steps: - uses: actions/checkout@v2 with: @@ -71,11 +63,7 @@ jobs: strategy: matrix: ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - - "5.0.0" - - "5.1.1" + - "5.2.0" steps: - uses: actions/checkout@v2 with: diff --git a/.github/workflows/makefiles.yaml b/.github/workflows/makefiles.yaml deleted file mode 100644 index dca59e037..000000000 --- a/.github/workflows/makefiles.yaml +++ /dev/null @@ -1,87 +0,0 @@ -name: "Makefile CI" - -on: [pull_request, push] - -jobs: - build: - name: "Compile CodeHawk" - runs-on: ubuntu-latest - strategy: - matrix: - ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - steps: - - uses: actions/checkout@v1 - - uses: ocaml/setup-ocaml@v3 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - - name: Install dependencies - run: opam install extlib camlzip zarith ocamlbuild goblint-cil - - name: Compile CodeHawk - run: eval $(opam env) && cd CodeHawk && ./full_make_no_gui.sh - - name: Prepare tar file for upload - run: tar -cvf artifacts.tar CodeHawk/CHB/bchcmdline/chx86_analyze CodeHawk/CHC/cchcil/parseFile CodeHawk/CHC/cchcmdline/canalyzer - - name: Upload artifacts tar file - uses: actions/upload-artifact@v4 - with: - name: artifacts-${{ matrix.ocaml-compiler }} - path: artifacts.tar - b_orchestration: - name: "Run CodeHawk-Binary tests" - needs: build - runs-on: ubuntu-latest - strategy: - matrix: - ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - steps: - - uses: actions/checkout@v2 - with: - repository: static-analysis-engineering/CodeHawk-Binary - - name: Delete submitted prebuilts - run: rm -f chb/bin/binaries/linux/chx86_analyze - - name: Download artifacts tar - uses: actions/download-artifact@v4 - with: - name: artifacts-${{ matrix.ocaml-compiler }} - - name: Extract artifacts - run: | - tar xvf artifacts.tar - mv CodeHawk/CHB/bchcmdline/chx86_analyze chb/bin/binaries/linux/chx86_analyze - - name: Run binary analyzer tests - run: PYTHONPATH=$PWD chb/cmdline/chkx test runall - c_orchestration: - name: "Run CodeHawk-C tests" - needs: build - runs-on: ubuntu-latest - strategy: - matrix: - ocaml-compiler: - - "4.12.1" - - "4.13.1" - - "4.14.1" - steps: - - uses: actions/checkout@v2 - with: - repository: static-analysis-engineering/CodeHawk-C - - name: Delete submitted prebuilts - run: | - rm -f chc/bin/linux/parseFile - rm -f chc/bin/linux/canalyzer - - name: Download artifacts tar - uses: actions/download-artifact@v4 - with: - name: artifacts-${{ matrix.ocaml-compiler }} - - name: Extract artifacts - run: | - tar xvf artifacts.tar - mv CodeHawk/CHC/cchcil/parseFile chc/bin/linux/parseFile - mv CodeHawk/CHC/cchcmdline/canalyzer chc/bin/linux/canalyzer - - name: Run kendra test suite - run: | - PYTHONPATH=$PWD python3 chc/cmdline/chkc kendra test-sets | tee kendra_output.txt - diff kendra_output.txt tests/kendra/example_output/test_kendrasets.txt diff --git a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml index cf0cf84eb..32e19bdb4 100644 --- a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml @@ -630,6 +630,7 @@ let arm_vfp_params let get_arm_format_spec_parameters (cpars: fts_parameter_t list) + (isinput: bool) (argspecs: argspec_int list): fts_parameter_t list = let nextindex = (List.length cpars) + 1 in let update_core_reg aas (r: arm_reg_t) = @@ -707,30 +708,35 @@ let get_arm_format_spec_parameters aas_start_state cpars in let (_, pars, _, _) = List.fold_left (fun (aas, accpars, varargindex, nxtindex) argspec -> - let ftype = get_fmt_spec_type argspec in - let ftype = - if is_float ftype then - promote_float ftype - else if is_int ftype then - promote_int ftype - else - ftype in - let size_r = size_of_btype ftype in let name = "vararg_" ^ (string_of_int varargindex) in let (param, new_state) = - match size_r with - | Ok 4 -> get_arm_int_param_next_state 4 name ftype aas nxtindex - | Ok 8 -> get_long_int_param_next_state 8 name ftype aas varargindex - | Ok size -> - raise - (BCH_failure - (LBLOCK [ - STR "Var-arg size: "; INT size; STR " not supported"])) - | Error e -> - raise - (BCH_failure - (LBLOCK [ - STR "Error in var-args: "; STR (String.concat "; " e)])) in + if isinput then + let vtype = get_fmt_spec_type argspec in + let ftype = TPtr (vtype, []) in + get_arm_int_param_next_state 4 name ftype aas nxtindex + else + let ftype = get_fmt_spec_type argspec in + let ftype = + if is_float ftype then + promote_float ftype + else if is_int ftype then + promote_int ftype + else + ftype in + let size_r = size_of_btype ftype in + match size_r with + | Ok 4 -> get_arm_int_param_next_state 4 name ftype aas nxtindex + | Ok 8 -> get_long_int_param_next_state 8 name ftype aas varargindex + | Ok size -> + raise + (BCH_failure + (LBLOCK [ + STR "Var-arg size: "; INT size; STR " not supported"])) + | Error e -> + raise + (BCH_failure + (LBLOCK [ + STR "Error in var-args: "; STR (String.concat "; " e)])) in (new_state, param :: accpars, varargindex + 1, nxtindex + 1)) (fmtaas, [], 1, nextindex) argspecs in pars diff --git a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.mli b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.mli index 783eeaadc..8295d4c72 100644 --- a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.mli +++ b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.mli @@ -103,4 +103,4 @@ val arm_vfp_params: ?attrs:b_attributes_t -> ?varargs:bool -> bfunarg_t list -> fts_parameter_t list val get_arm_format_spec_parameters: - fts_parameter_t list -> argspec_int list -> fts_parameter_t list + fts_parameter_t list -> bool -> argspec_int list -> fts_parameter_t list diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 7f46de515..72b9eb4f9 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -646,17 +646,32 @@ object (self) ctinfo in if ctinfo#is_signature_valid then begin + let fintf = ctinfo#get_function_interface in + let sem = ctinfo#get_semantics in + let _ = + log_diagnostics_result + ~tag:"update-call-target" + ~msg:self#cia + __FILE__ __LINE__ + ["callee: " ^ ctinfo#get_name; + "pars: " + ^ (string_of_int + (List.length (get_fts_parameters fintf))); + "sideeffects: " + ^ (string_of_int + (List.length sem.fsem_sideeffects))] in (try - match self#update_varargs ctinfo#get_function_interface with - | Some fintf -> + match self#update_varargs fintf sem with + | Some (new_fintf, new_sem) -> let _ = chlog#add "update call target api" (LBLOCK [ self#l#toPretty; STR ": "; - (function_interface_to_pretty fintf)]) in - self#set_call_target (update_target_interface ctinfo fintf) + (function_interface_to_pretty new_fintf)]) in + self#set_call_target + (update_target_interface_and_semantics ctinfo new_fintf new_sem) | _ -> () with _ -> ()); @@ -664,9 +679,13 @@ object (self) else () - method private update_x86_varargs (_s: function_interface_t) = None + method private update_x86_varargs + (_fintf: function_interface_t) + (_sem: function_semantics_t) = None - method private update_arm_varargs (fintf: function_interface_t) = + method private update_arm_varargs + (fintf: function_interface_t) + (sem: function_semantics_t) = let args = self#get_call_arguments in let argcount = List.length args in if argcount = 0 then @@ -674,6 +693,14 @@ object (self) else let (lastpar, lastx) = List.nth args (argcount - 1) in let arg = if is_formatstring_parameter lastpar then Some lastx else None in + let _ = + log_diagnostics_result + ~tag:"update-arm-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["last-par: " ^ lastpar.apar_name; + "fmt: " ^ (formatstring_type_to_string lastpar.apar_fmt); + "is-fmtstring: " ^ (if Option.is_some arg then "yes" else "no")] in match arg with | Some (XConst (IntConst n)) -> log_tfold_default @@ -681,22 +708,77 @@ object (self) ~tag:"update_arm_varargs" (self#cia ^ ": constant: " ^ n#toString)) (fun addr -> - if string_table#has_string addr then + let in_table = string_table#has_string addr in + let _ = + log_diagnostics_result + ~tag:"update-arm-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-string addr: " ^ addr#to_hex_string; + "in-string-table: " ^ (if in_table then "yes" else "no")] in + if in_table then let fmtstring = string_table#get_string addr in - let fmtspec = parse_formatstring fmtstring false in + let isinput = is_scanformat_parameter lastpar in + let _ = + log_diagnostics_result + ~tag:"update-arm-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-string: \"" ^ fmtstring ^ "\""; + "isinput: " ^ (if isinput then "yes" else "no")] in + let fmtspec = parse_formatstring fmtstring isinput in + let _ = + log_diagnostics_result + ~tag:"update-arm-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-args found: " + ^ (string_of_int (List.length fmtspec#get_arguments))] in if fmtspec#has_arguments then let fmtargs = fmtspec#get_arguments in - let newfintf = add_format_spec_parameters fintf fmtargs in - Some newfintf + let orig_npar = List.length (get_fts_parameters fintf) in + let newfintf = add_format_spec_parameters fintf isinput fmtargs in + let new_sem = + if isinput then + let new_pars = + List.filteri + (fun i _ -> i >= orig_npar) + (get_fts_parameters newfintf) in + let new_ses = + List.map (fun p -> + match p.apar_type with + | TPtr (vtype, _) -> + XXBlockWrite + (vtype, ArgValue p, + IndexSize (NumConstant (mkNumerical 1))) + | _ -> + XXBlockWrite + (p.apar_type, ArgValue p, + IndexSize (NumConstant (mkNumerical 1)))) + new_pars in + {sem with + fsem_sideeffects = sem.fsem_sideeffects @ new_ses} + else + sem in + Some (newfintf, new_sem) else None else None) None (numerical_to_doubleword n) - | _ -> None + | _ -> + let _ = + log_diagnostics_result + ~tag:"update-arm-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["format string address is not a constant"] in + None - method private update_mips_varargs (fintf: function_interface_t) = + method private update_mips_varargs + (fintf: function_interface_t) + (sem: function_semantics_t) = let args = self#get_call_arguments in let argcount = List.length args in if argcount = 0 then @@ -704,6 +786,14 @@ object (self) else let (lastpar, lastx) = List.nth args (argcount - 1) in let arg = if is_formatstring_parameter lastpar then Some lastx else None in + let _ = + log_diagnostics_result + ~tag:"update-mips-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["last-par: " ^ lastpar.apar_name; + "fmt: " ^ (formatstring_type_to_string lastpar.apar_fmt); + "is-fmtstring: " ^ (if Option.is_some arg then "yes" else "no")] in match arg with | Some (XConst (IntConst n)) -> log_tfold_default @@ -711,32 +801,100 @@ object (self) ~tag:"update_mips_varargs" (self#cia ^ ": constant: " ^ n#toString)) (fun addr -> - if string_table#has_string addr then + let in_table = string_table#has_string addr in + let _ = + log_diagnostics_result + ~tag:"update-mips-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-string addr: " ^ addr#to_string; + "in-string-table: " ^ (if in_table then "yes" else "no")] in + if in_table then let fmtstring = string_table#get_string addr in - let fmtspec = parse_formatstring fmtstring false in + let isinput = is_scanformat_parameter lastpar in + let _ = + log_diagnostics_result + ~tag:"update-mips-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-string: \"" ^ fmtstring ^ "\""; + "isinput: " ^ (if isinput then "yes" else "no")] in + let fmtspec = parse_formatstring fmtstring isinput in + let _ = + log_diagnostics_result + ~tag:"update-mips-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["fmt-args found: " + ^ (string_of_int (List.length fmtspec#get_arguments))] in if fmtspec#has_arguments then let fmtargs = fmtspec#get_arguments in - let newfintf = add_format_spec_parameters fintf fmtargs in - Some newfintf + let orig_npar = List.length (get_fts_parameters fintf) in + let newfintf = add_format_spec_parameters fintf isinput fmtargs in + let new_sem = + if isinput then + let new_pars = + List.filteri + (fun i _ -> i >= orig_npar) + (get_fts_parameters newfintf) in + let new_ses = + List.map (fun p -> + match p.apar_type with + | TPtr (vtype, _) -> + XXBlockWrite + (vtype, ArgValue p, + IndexSize (NumConstant (mkNumerical 1))) + | _ -> + XXBlockWrite + (p.apar_type, ArgValue p, + IndexSize (NumConstant (mkNumerical 1)))) + new_pars in + {sem with + fsem_sideeffects = sem.fsem_sideeffects @ new_ses} + else + sem in + Some (newfintf, new_sem) else None else None) None (numerical_to_doubleword n) - | _ -> None + | _ -> + let _ = + log_diagnostics_result + ~tag:"update-mips-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["format string address is not a constant"] in + None - method private update_varargs (fintf: function_interface_t) = + method private update_varargs + (fintf: function_interface_t) + (sem: function_semantics_t) = let fts = fintf.fintf_type_signature in match fts.fts_va_list with - | Some _ -> None + | Some _ -> + let _ = + log_diagnostics_result + ~tag:"update-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["skipped (va_list already set)"] in + None | _ -> if system_settings#is_mips then - self#update_mips_varargs fintf + self#update_mips_varargs fintf sem else if system_settings#is_arm then - self#update_arm_varargs fintf + self#update_arm_varargs fintf sem else - self#update_x86_varargs fintf + let _ = + log_diagnostics_result + ~tag:"update-varargs" + ~msg:self#cia + __FILE__ __LINE__ + ["x86 vararg update not yet implemented"] in + self#update_x86_varargs fintf sem (* Power32 uses r3 through r10 as default argument registers *) (* @@ -3227,6 +3385,13 @@ object (self) [ABSTRACT_VARS [lhs]] else + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_assign_cmds: ASSIGN_NUM" + __FILE__ __LINE__ + ["lhs: " ^ (p2s lhs#toPretty); + "rhs: " ^ (p2s (numerical_exp_to_pretty rhs))] in rhsCmds @ [ASSIGN_NUM (lhs, rhs)] method get_ssa_assign_commands @@ -3329,37 +3494,63 @@ object (self) method private evaluate_fts_address_argument (p: fts_parameter_t):variable_t option = + let resolve_stack_address xpr tag = + match xpr with + | XOp (XMinus, [XVar _v; XConst (IntConst n)]) when n#geq numerical_zero -> + let spoffset = n#neg in + (match self#f#stackframe#containing_stackslot spoffset#toInt with + | Some stackslot -> + let stackvar = self#f#env#mk_stackslot_variable stackslot NoOffset in + let _ = + log_diagnostics_result + ~tag:"evaluate_fts_address_argument:resolve_stack_address" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "xpr: " ^ (x2s xpr); + "offset: " ^ (spoffset#toString); + "stackvar: " ^ (p2s stackvar#toPretty)] in + Some stackvar + | _ -> + begin + log_diagnostics_result + ~tag:(tag ^ ":no stackslot found") + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "xpr: " ^ (x2s xpr); + "offset: " ^ (spoffset#toString)]; + None + end) + | _ -> + begin + log_diagnostics_result + ~tag + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "xpr: " ^ (x2s xpr)]; + None + end in match p.apar_location with | [RegisterParameter (r, _, _)] -> let argvar = self#env#mk_register_variable r in let xpr = self#rewrite_variable_to_external argvar in - (match xpr with - | XOp (XMinus, [XVar _v; XConst (IntConst n)]) when n#geq numerical_zero -> - let spoffset = n#neg in - (match self#f#stackframe#containing_stackslot spoffset#toInt with - | Some stackslot -> - Some (self#f#env#mk_stackslot_variable stackslot NoOffset) - | _ -> - begin - log_diagnostics_result - ~tag:"evaluate_fts_address_argument:no stackslot found" - ~msg:(p2s self#l#toPretty) - __FILE__ __LINE__ - ["parameter: " ^ (fts_parameter_to_string p); - "external argvar: " ^ (x2s xpr); - "offset: " ^ (spoffset#toString)]; - None - end) - | _ -> - begin - log_diagnostics_result - ~tag:"evaluate_fts_address_argument" - ~msg:(p2s self#l#toPretty) - __FILE__ __LINE__ - ["parameter: " ^ (fts_parameter_to_string p); - "external argvar: " ^ (x2s xpr)]; - None - end) + resolve_stack_address xpr "evaluate_fts_address_argument" + | [StackParameter (offset, _, _)] -> + let memref = self#f#env#mk_local_stack_reference in + let p_offset = mkNumerical offset in + log_tfold_default + (mk_tracelog_spec + ~tag:"evaluate_fts_address_argument" + (self#cia ^ ": stack parameter at offset " ^ (string_of_int offset))) + (fun s_offset -> + let svar = + self#f#env#mk_memory_variable memref (s_offset#add p_offset) in + let xpr = self#inv#rewrite_expr (XVar svar) in + resolve_stack_address xpr "evaluate_fts_address_argument") + None + self#get_singleton_stackpointer_offset | _ -> begin log_diagnostics_result @@ -3666,6 +3857,16 @@ object (self) ~btype:(Some ty) self#cia numoffset (bterm_to_string dest) | _ -> self#env#mk_side_effect_value self#cia (bterm_to_string dest)) in + let _ = + log_diagnostics_result + ~tag:"get_sideeffect_assign:rhs" + ~msg:self#cia + __FILE__ __LINE__ + ["side-effect: " ^ (p2s (xxpredicate_to_pretty side_effect)); + "memVar: " ^ (p2s memVar#toPretty); + "rhs: " ^ (x2s (XVar rhs)); + "rhs-rewritten: " + ^ (x2s (self#inv#rewrite_expr (XVar rhs)))] in let seAssign = let _ = chlog#add @@ -3682,11 +3883,19 @@ object (self) let fldAssigns = [] in seAssign @ fldAssigns | _ -> + let btermxpr = + match termev#bterm_xpr dest with + | Some x -> x + | _ -> random_constant_expr in begin log_error_result ~msg:(p2s msg) ~tag:"side-effect ignored" - __FILE__ __LINE__ []; + __FILE__ __LINE__ + ["dest: " ^ (bterm_to_string dest); + "adest: " ^ (x2s adest); + "xpo: " ^ (p2s (BCHXPOPredicate.xpo_predicate_to_pretty xpo)); + "btermxpr: " ^ (x2s btermxpr)]; [] end end @@ -3906,14 +4115,14 @@ object (self) let globals = List.filter self#f#env#is_mutable_global_variable self#env#get_variables in let _ = - ch_diagnostics_log#add - "call: abstract globals" - (LBLOCK [ - self#l#toPretty; STR ": "; - pretty_print_list - globals - (fun v -> STR (self#f#env#variable_name_to_string v)) - "[" ", " "]"]) in + log_diagnostics_result + ~tag:"get_arm_call_commands:abstract globals" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["globals: " + ^ (String.concat + ", " + (List.map self#f#env#variable_name_to_string globals))] in [ABSTRACT_VARS globals] in let sideeffect_assigns = self#get_sideeffect_assigns termev self#get_call_target#get_semantics in diff --git a/CodeHawk/CHB/bchlib/bCHFtsParameter.ml b/CodeHawk/CHB/bchlib/bCHFtsParameter.ml index 8aa4d4243..2dd2a8a7b 100644 --- a/CodeHawk/CHB/bchlib/bCHFtsParameter.ml +++ b/CodeHawk/CHB/bchlib/bCHFtsParameter.ml @@ -86,7 +86,7 @@ let _arg_io_to_string (i:arg_io_t) = | ArgReadWrite -> "rw" -let _formatstring_type_to_string (t:formatstring_type_t) = +let formatstring_type_to_string (t:formatstring_type_t) = match t with | NoFormat -> "no" | PrintFormat -> "print" @@ -392,6 +392,12 @@ let is_formatstring_parameter (p: fts_parameter_t) = | _ -> true +let is_scanformat_parameter (p: fts_parameter_t) = + match p.apar_fmt with + | ScanFormat -> true + | _ -> false + + let is_floating_point_parameter (p: fts_parameter_t) = match p.apar_type with | TFloat _ -> true diff --git a/CodeHawk/CHB/bchlib/bCHFtsParameter.mli b/CodeHawk/CHB/bchlib/bCHFtsParameter.mli index 7db919279..032e59dcd 100644 --- a/CodeHawk/CHB/bchlib/bCHFtsParameter.mli +++ b/CodeHawk/CHB/bchlib/bCHFtsParameter.mli @@ -227,8 +227,12 @@ val is_register_parameter_for_register: fts_parameter_t -> register_t -> bool val is_arg_parameter: fts_parameter_t -> bool +val formatstring_type_to_string: formatstring_type_t -> string + val is_formatstring_parameter: fts_parameter_t -> bool +val is_scanformat_parameter: fts_parameter_t -> bool + val is_floating_point_parameter: fts_parameter_t -> bool diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index 20691fcde..68c1697c9 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1371,12 +1371,13 @@ let function_type_resolvents_to_bfuntype addition of (inferred) parameters to the function interface itself.*) let add_format_spec_parameters (fintf: function_interface_t) + (isinput: bool) (argspecs: argspec_int list): function_interface_t = let pars = get_fts_parameters fintf in let fmtpars = match system_settings#get_architecture with - | "arm" -> get_arm_format_spec_parameters pars argspecs - | "mips" -> get_mips_format_spec_parameters pars argspecs + | "arm" -> get_arm_format_spec_parameters pars isinput argspecs + | "mips" -> get_mips_format_spec_parameters pars isinput argspecs | arch -> let _ = ch_error_log#add diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli b/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli index ce8cfeaca..21db33905 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli @@ -153,7 +153,7 @@ val add_function_global_parameter_location: val add_format_spec_parameters: - function_interface_t -> argspec_int list -> function_interface_t + function_interface_t -> bool -> argspec_int list -> function_interface_t (** Modifies the types of the function type signature according to a type diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 1b21b353d..5ad87998c 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1911,6 +1911,7 @@ object ('a) method is_interval: bool method is_base_offset_value: bool method is_symbolic_expr: bool + method is_symbolic_side_effect_value: bool method is_linear_equality: bool method is_loopcounter_equality: bool method is_variable_equality: bool @@ -7181,6 +7182,7 @@ type file_results_t = { ffres_idadata: ida_data_t; ffres_fns_included: string list; ffres_fns_excluded: string list; + ffres_include_callees: bool; } diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml index 3e937ac85..52ce3c476 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -401,6 +401,12 @@ object (self:'a) | NonRelationalFact (_, FSymbolicExpr _) -> true | _ -> false + method is_symbolic_side_effect_value = + match fact with + | NonRelationalFact (_, FSymbolicExpr (XVar v)) -> + (String.sub v#getName#getBaseName 0 3) = "se_" + | _ -> false + method is_linear_equality = match fact with | RelationalFact _ -> true @@ -500,6 +506,9 @@ object (self) self#integrate_fact inv end + method private remove_fact (inv: invariant_int) = + H.remove facts (invd#index_invariant_fact inv#get_fact) + method remove_initial_value_fact (fvar: variable_t) (fval: variable_t) = let index = fvar#getName#getSeqNumber in if H.mem table index then @@ -522,104 +531,179 @@ object (self) else () - method private integrate_fact (inv:invariant_int) = - let add (v: variable_t) (f: invariant_int) = - let index = v#getName#getSeqNumber in - let entry = - if H.mem table index then - let e = H.find table index in - if List.exists (fun w -> (f#compare w) = 0) e then - e - (* remove base-offset value when a symbolic expression is found *) - else if f#is_symbolic_expr then + (* Integrate a non-relational fact f for variable v into the per-variable + table at this location. Six cases: + + Case 0: variable not yet seen at this location — create a singleton list. + + Case 1: exact duplicate — discard new fact (idempotency). Facts are + compared by their dictionary index, so this O(n) scan catches semantically + equal facts that were assigned a different index by the dictionary. + + Case 2: incoming fact is a symbolic expression (e.g., a side-effect value + written by an external call such as sscanf). Evict any existing constant + and base-offset facts for this variable from both the per-variable list + ('table') and the global fact index ('facts') via remove_fact. + + Background on the eviction: StackParameter vararg arguments require + additional analysis rounds before their side-effect value can be + established — one round to discover the expanded vararg interface, and one + more to create the stack location variable. By that time, constant facts + from earlier initialization have already propagated through all downstream + locations. When the symbolic expression finally arrives it must displace + both constant and base-offset facts. Register-parameter varargs do not + have this problem because their locations exist from the first analysis + round. + + Case 3: incoming fact is a symbolic expression. Evict any existing + base-offset facts for this variable from both the per-variable list + ('table') and the global fact index ('facts') via remove_fact. + + Cases 4 & 5: interval and base-offset facts follow a monotone-refinement + policy. At most one of each type is maintained per variable; a new fact + replaces the existing one only if it is strictly tighter (i.e., carries + more information). + + Case 6: all other fact types (InitialVarEquality, InitialVarDisEquality, + TestVarEquality) — append unconditionally; no conflict resolution is + needed for these types. *) + method private add_nonrelational_fact (v: variable_t) (f: invariant_int) = + let index = v#getName#getSeqNumber in + let entry = + if H.mem table index then + let e = H.find table index in + + (* Case 1: exact duplicate. *) + if List.exists (fun w -> (f#compare w) = 0) e then + e + + (* Case 2: side-effect value: evict all other invariants, as this + value is most likely discovered at a later time, invalidating existing + invariants for that variable *) + else if f#is_symbolic_side_effect_value then + let _ = + log_diagnostics_result + ~tag:"add_nonrelational_fact:symbolic_side_effect_value" + ~msg:iaddr + __FILE__ __LINE__ + ["inv: " ^ (p2s f#toPretty); + "removed: " + ^ (String.concat ", " (List.map (fun p -> p2s p#toPretty) e))] in + let _ = List.iter self#remove_fact e in + [f] + + (* Case 3: symbolic expression — evict base-offset values. *) + else if f#is_symbolic_expr then + let conflictingfacts = List.filter (fun p -> p#is_base_offset_value) e in + let otherfacts = List.filter (fun p -> not (p#is_base_offset_value)) e in + let _ = + log_diagnostics_result + ~tag:"add_nonrelational_fact:symbolic_expr" + ~msg:iaddr + __FILE__ __LINE__ + ["inv: " ^ (p2s f#toPretty); + "evicted: " + ^ (String.concat "; " + (List.map (fun p -> p2s p#toPretty) conflictingfacts)); + "remaining: " + ^ (String.concat "; " + (List.map (fun p -> p2s p#toPretty) otherfacts))] in + let _ = List.iter self#remove_fact conflictingfacts in + f :: otherfacts + + (* Case 4: interval — keep only the tightest interval. *) + else if f#is_interval then + let pfacts = List.filter (fun p -> p#is_interval) e in + (match pfacts with + | [] -> f :: e + | [p] when f#is_smaller p -> + f :: (List.filter (fun p -> not p#is_interval) e) + | [_] -> e + | _ -> + let msg = + LBLOCK [ + STR "Multiple interval facts: "; + pretty_print_list pfacts (fun p -> p#toPretty) "{" "," "}"; + STR " at "; + STR iaddr] in + begin + ch_error_log#add "interval facts" msg; + raise (BCH_failure msg) + end) + + (* Case 5: base-offset value — keep only the tightest. *) + else if f#is_base_offset_value then + let pfacts = List.filter (fun p -> p#is_base_offset_value) e in + (match pfacts with + | [] -> f :: e + | [p] when f#is_smaller p -> f :: (List.filter (fun p -> not p#is_base_offset_value) e) - (* only allow one interval in the set of facts *) - else if f#is_interval then - let pfacts = List.filter (fun p -> p#is_interval) e in - match pfacts with - | [] -> f :: e - | [p] when f#is_smaller p -> - f :: (List.filter (fun p -> not p#is_interval) e) - | [_] -> e - | _ -> - let msg = - LBLOCK [ - STR "Multiple interval facts: "; - pretty_print_list pfacts (fun p -> p#toPretty) "{" "," "}"; - STR " at "; - STR iaddr] in - begin - ch_error_log#add "interval facts" msg; - raise (BCH_failure msg) - end - else if f#is_base_offset_value then - let pfacts = List.filter (fun p -> p#is_base_offset_value) e in - match pfacts with - | [] -> f :: e - | [p] when f#is_smaller p -> - f :: (List.filter (fun p -> not p#is_base_offset_value) e) - | [_] -> e - | _ -> - let msg = - LBLOCK [ - STR "Multiple base-offset-value facts: "; - pretty_print_list pfacts - (fun p -> p#toPretty) "{" "," "}"] in - begin - ch_error_log#add "base-offset-value facts" msg; - raise (BCH_failure msg) - end - else - f :: e - else - [f] in - H.replace table index entry in - let add_relational_equality f = - if f#is_variable_equality then - let eqvars = f#get_variable_equality_variables in - match eqvars with - | [v1; v2] -> - let v1index = v1#getName#getSeqNumber in - let v2index = v2#getName#getSeqNumber in - if H.mem table v2index then - let v2facts = H.find table v2index in - let v1newfacts = - List.fold_left (fun a f -> - match f#get_fact with - | NonRelationalFact (_, _nrv) -> - let _ = - chlog#add - "transfer invariant" - (LBLOCK [ - STR iaddr; - STR ": "; - v1#toPretty; - STR " to "; - v2#toPretty; - STR ": "; - f#toPretty]) in - - (f#transfer v1) :: a - | _ -> a) [] v2facts in - if H.mem table v1index then - let v1facts = H.find table v1index in - List.iter (fun f -> add v1 f) (v1newfacts @ v1facts) - else - H.add table v1index v1newfacts - else - () - | _ -> () + | [_] -> e + | _ -> + let msg = + LBLOCK [ + STR "Multiple base-offset-value facts: "; + pretty_print_list pfacts (fun p -> p#toPretty) "{" "," "}"] in + begin + ch_error_log#add "base-offset-value facts" msg; + raise (BCH_failure msg) + end) + + (* Case 6: all other fact types — append unconditionally. *) + else + f :: e + + (* Case 0: first fact for this variable at this location. *) else - () in - begin - match inv#get_fact with - | NonRelationalFact (v, _) - | InitialVarEquality (v, _) - | InitialVarDisEquality (v, _) - | TestVarEquality (v, _, _, _) -> add v inv - | RelationalFact _ -> add_relational_equality inv + [f] in + H.replace table index entry + + (* Forward propagation for variable equalities: when v1 == v2 is established, + any non-relational facts already known for v2 are transferred to v1, so + downstream queries on v1 can immediately benefit from them. *) + method private add_relational_equality_fact (f: invariant_int) = + if f#is_variable_equality then + let eqvars = f#get_variable_equality_variables in + match eqvars with + | [v1; v2] -> + let v1index = v1#getName#getSeqNumber in + let v2index = v2#getName#getSeqNumber in + if H.mem table v2index then + let v2facts = H.find table v2index in + let v1newfacts = + List.fold_left (fun a nrf -> + match nrf#get_fact with + | NonRelationalFact (_, _nrv) -> + let _ = + log_diagnostics_result + ~tag:"add_relational_equality_fact:transfer invariant" + ~msg:iaddr + __FILE__ __LINE__ + ["v1: " ^ (p2s v1#toPretty); + "v2: " ^ (p2s v2#toPretty); + "fact: " ^ (p2s nrf#toPretty)] in + (nrf#transfer v1) :: a + | _ -> a) [] v2facts in + if H.mem table v1index then + let v1facts = H.find table v1index in + List.iter (fun nrf -> self#add_nonrelational_fact v1 nrf) + (v1newfacts @ v1facts) + else + H.add table v1index v1newfacts + else + () | _ -> () - end + else + () + + method private integrate_fact (inv: invariant_int) = + match inv#get_fact with + | NonRelationalFact (v, _) + | InitialVarEquality (v, _) + | InitialVarDisEquality (v, _) + | TestVarEquality (v, _, _, _) -> self#add_nonrelational_fact v inv + | RelationalFact _ -> self#add_relational_equality_fact inv + | _ -> () method private get_var_facts (v:variable_t) = let index = v#getName#getSeqNumber in diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli b/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli index 805119f83..d7fe82bad 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 diff --git a/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.ml index abe6f3846..0982384eb 100644 --- a/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.ml @@ -91,6 +91,7 @@ let get_mips_int_param_next_state let get_mips_format_spec_parameters (cpars: fts_parameter_t list) + (isinput: bool) (argspecs: argspec_int list): fts_parameter_t list = let nextindex = (List.length cpars) + 1 in let update_core_reg mas (r: mips_reg_t) = @@ -130,23 +131,28 @@ let get_mips_format_spec_parameters mas_start_state cpars in let (_, pars, _, _) = List.fold_left (fun (mas, accpars, varargindex, nxtindex) argspec -> - let ftype = get_fmt_spec_type argspec in - let size_r = size_of_btype ftype in let name = "vararg_" ^ (string_of_int varargindex) in let (param, new_state) = - match size_r with - | Ok 4 -> get_mips_int_param_next_state 4 name ftype mas nxtindex - | Ok size -> - raise - (BCH_failure - (LBLOCK [ - STR "Var-arg size: "; INT size; STR " not supported"])) - | Error e -> - raise - (BCH_failure - (LBLOCK [ - STR "Error in mips_format_spec_parameters: "; - STR (String.concat "; " e)])) in + if isinput then + let vtype = get_fmt_spec_type argspec in + let ftype = TPtr (vtype, []) in + get_mips_int_param_next_state 4 name ftype mas nxtindex + else + let ftype = get_fmt_spec_type argspec in + let size_r = size_of_btype ftype in + match size_r with + | Ok 4 -> get_mips_int_param_next_state 4 name ftype mas nxtindex + | Ok size -> + raise + (BCH_failure + (LBLOCK [ + STR "Var-arg size: "; INT size; STR " not supported"])) + | Error e -> + raise + (BCH_failure + (LBLOCK [ + STR "Error in mips_format_spec_parameters: "; + STR (String.concat "; " e)])) in (new_state, param :: accpars, varargindex + 1, nxtindex + 1)) (fmtmas, [], 1, nextindex) argspecs in pars diff --git a/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.mli b/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.mli index 86e5dbc07..b32bcd195 100644 --- a/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.mli +++ b/CodeHawk/CHB/bchlib/bCHMIPSFunctionInterface.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -33,4 +33,4 @@ open BCHLibTypes val get_mips_format_spec_parameters: - fts_parameter_t list -> argspec_int list -> fts_parameter_t list + fts_parameter_t list -> bool -> argspec_int list -> fts_parameter_t list diff --git a/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.ml b/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.ml index 162543ecb..6c767a9b0 100644 --- a/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.ml @@ -5,7 +5,7 @@ The MIT License (MIT) Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -185,6 +185,14 @@ let update_target_interface mk_call_target_info fintf semantics tgt +let update_target_interface_and_semantics + (ctinfo: call_target_info_int) + (fintf: function_interface_t) + (sem: function_semantics_t) = + let tgt = ctinfo#get_target in + mk_call_target_info fintf sem tgt + + let mk_call_target_info (ctgt: call_target_t): call_target_info_int = match ctgt with | StubTarget (DllFunction (dll, name)) -> mk_dll_target dll name diff --git a/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.mli b/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.mli index cd74be8cc..567cf97d7 100644 --- a/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.mli +++ b/CodeHawk/CHB/bchlib/bCHMakeCallTargetInfo.mli @@ -5,7 +5,7 @@ The MIT License (MIT) Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -147,3 +147,10 @@ val mk_call_target_info: call_target_t -> call_target_info_int is still consistent with the updated function interface.*) val update_target_interface: call_target_info_int -> function_interface_t -> call_target_info_int + + +val update_target_interface_and_semantics: + call_target_info_int + -> function_interface_t + -> function_semantics_t + -> call_target_info_int diff --git a/CodeHawk/CHB/bchlib/bCHMetrics.ml b/CodeHawk/CHB/bchlib/bCHMetrics.ml index 95caedea6..1f8a4cf26 100644 --- a/CodeHawk/CHB/bchlib/bCHMetrics.ml +++ b/CodeHawk/CHB/bchlib/bCHMetrics.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2023 Aarno Labs + Copyright (c) 2021-2026 Aarno Labs Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -388,7 +388,8 @@ object (self) ffres_idadata = { ida_function_entry_points = self#get_ida_function_entry_points}; ffres_fns_included = included_functions (); - ffres_fns_excluded = excluded_functions () + ffres_fns_excluded = excluded_functions (); + ffres_include_callees = fn_include_callees (); } method write_xml_analysis_stats (node:xml_element_int) = diff --git a/CodeHawk/CHB/bchlib/bCHMetrics.mli b/CodeHawk/CHB/bchlib/bCHMetrics.mli index 552ab325b..8ed55d9c7 100644 --- a/CodeHawk/CHB/bchlib/bCHMetrics.mli +++ b/CodeHawk/CHB/bchlib/bCHMetrics.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2023 Aarno Labs LLC + Copyright (c) 2022-2026 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 diff --git a/CodeHawk/CHB/bchlib/bCHMetricsHandler.ml b/CodeHawk/CHB/bchlib/bCHMetricsHandler.ml index db4da2ec4..24c824644 100644 --- a/CodeHawk/CHB/bchlib/bCHMetricsHandler.ml +++ b/CodeHawk/CHB/bchlib/bCHMetricsHandler.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs + Copyright (c) 2021-2026 Aarno Labs Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -1364,7 +1364,8 @@ object ffres_userdata = userdata_metrics_handler#init_value; ffres_idadata = ida_data_handler#init_value; ffres_fns_included = included_functions (); - ffres_fns_excluded = excluded_functions () + ffres_fns_excluded = excluded_functions (); + ffres_include_callees = fn_include_callees (); } method !write_xml (node:xml_element_int) (d:file_results_t) = @@ -1406,6 +1407,8 @@ object (if (List.length d.ffres_fns_included) > 0 then begin incNode#setAttribute "addrs" (String.concat "," d.ffres_fns_included); + (if d.ffres_include_callees then + incNode#setAttribute "include-callees" "yes"); append [incNode] end); (if (List.length d.ffres_fns_excluded) > 0 then @@ -1422,6 +1425,7 @@ object let getc = node#getTaggedChild in let getf tag = float_of_string (get tag) in let has = node#hasNamedAttribute in + let hasc = node#hasOneTaggedChild in { ffres_stable = if has "stable" then (get "stable") = "yes" else false; ffres_time = getf "time"; ffres_runs = @@ -1442,7 +1446,18 @@ object ffres_userdata = userdata_metrics_handler#read_xml (getc "userdata"); ffres_idadata = ida_data_handler#read_xml (getc "idadata"); ffres_fns_included = - if has "fns-included" then nsplit ',' (get "addrs") else []; + if hasc "fns-included" then + let fnsnode = getc "fns-included" in + nsplit ',' (fnsnode#getAttribute "addrs") else []; + ffres_include_callees = + (if hasc "fns-included" then + let fnsnode = getc "fns-included" in + if fnsnode#hasNamedAttribute "include-callees" then + (fnsnode#getAttribute "include-callees") = "yes" + else + false + else + false); ffres_fns_excluded = if has "fns-excluded" then nsplit ',' (get "addrs") else []; } diff --git a/CodeHawk/CHB/bchlib/bCHMetricsHandler.mli b/CodeHawk/CHB/bchlib/bCHMetricsHandler.mli index b3356a5ed..c97eee4eb 100644 --- a/CodeHawk/CHB/bchlib/bCHMetricsHandler.mli +++ b/CodeHawk/CHB/bchlib/bCHMetricsHandler.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2026 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 diff --git a/CodeHawk/CHB/bchlib/bCHPrecondition.ml b/CodeHawk/CHB/bchlib/bCHPrecondition.ml index f51f81be1..41a05bef9 100644 --- a/CodeHawk/CHB/bchlib/bCHPrecondition.ml +++ b/CodeHawk/CHB/bchlib/bCHPrecondition.ml @@ -148,7 +148,10 @@ let read_xml_par_preconditions | "allocation-base" -> [XXAllocationBase t] | "function-pointer" -> let typ = ty () in [XXFunctionPointer (typ, t)] - | "format-string" -> [XXOutputFormatString t] + | "format-string" -> + (match thispar.apar_fmt with + | ScanFormat -> [XXInputFormatString t] + | _ -> [XXOutputFormatString t]) | "includes" -> let name = node#getAttribute "name" in [XXIncludes (t,get_structconstant name)] diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 37f190711..f463a4e50 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_20260527" - ~date:"2026-05-27" + ~version:"0.6.0_20260601" + ~date:"2026-06-01" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 841106529..c69572c21 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -553,9 +553,12 @@ let translate_arm_instruction instruction. *) let floc = get_floc loc in - let log_dc_error_result (file: string) (line: int) (e: string list) = + let log_dc_error_result + ?(tag:string option) (file: string) (line: int) (e: string list) = if BCHSystemSettings.system_settings#collect_data then - log_error_result ~msg:(p2s floc#l#toPretty) file line e + match tag with + | Some tag -> log_error_result ~tag ~msg:(p2s floc#l#toPretty) file line e + | _ -> log_error_result ~msg:(p2s floc#l#toPretty) file line e else () in let pcv = TR.tget_ok ((pc_r RD)#to_variable floc) in @@ -737,7 +740,7 @@ let translate_arm_instruction else if is_pointer ptype then (* necessary step to create a stack slot if the address is a stack address. A side effect of get_var_at_address is to - create a stack slot. Without no reaching definitions are + create a stack slot. Without, no reaching definitions are created for the buffer at this stack address. To be done in a better way, eventually. *) @@ -775,31 +778,48 @@ let translate_arm_instruction STR " Parameter type not recognized in call translation"]))) ([], [], []) callargs in - let (xprdefs, xpuse, xpusehigh) = + (* Add uses for buffer reads, as expressed in the callee's preconditions *) + let (xpuse, xpusehigh) = let sem = floc#get_call_target#get_semantics in - List.fold_left (fun (accdefs, accuse, accusehigh) p -> + List.fold_left (fun (accuse, accusehigh) p -> + match p with + | XXBuffer (_, dest, _) -> + (match floc#evaluate_summary_address_term dest with + | Some memVar -> (memVar :: accuse, memVar :: accusehigh) + | _ -> + begin + log_dc_error_result + ~tag:"calltgt_cmds:buffer dest not evaluated" + __FILE__ __LINE__ + ["call target: " ^ floc#get_call_target#get_name; + "dest: " ^ (BCHBTerm.bterm_to_string dest)]; + (accuse, accusehigh) + end) + | _ -> (accuse, accusehigh)) (use, usehigh) sem.fsem_pre in + + (* Add rdefs for buffer writes, as expressed in the callee's side effects *) + let xprdefs = + let sem = floc#get_call_target#get_semantics in + List.fold_left (fun accdefs p -> match p with | XXBlockWrite (_, dest, _) -> (match floc#evaluate_summary_address_term dest with - | Some memVar -> (memVar :: accdefs, accuse, accusehigh) + | Some memVar -> memVar :: accdefs | _ -> begin - log_diagnostics_result + log_dc_error_result ~tag:"calltgt_cmds:blockwrite dest not evaluated" __FILE__ __LINE__ ["call target: " ^ floc#get_call_target#get_name; "dest: " ^ (BCHBTerm.bterm_to_string dest)]; - (accdefs, accuse, accusehigh) + accdefs end) - | XXBuffer (_, dest, _) -> - (match floc#evaluate_summary_address_term dest with - | Some memVar -> (accdefs, memVar :: accuse, memVar :: accusehigh) - | _ -> (accdefs, accuse, accusehigh)) - | _ -> (accdefs, accuse, accusehigh)) ([], [], []) sem.fsem_pre in + | _ -> accdefs) [] sem.fsem_sideeffects in let _ = log_diagnostics_result ~tag:"calltgt_cmds" + ~msg:(p2s floc#l#toPretty) __FILE__ __LINE__ ["call target: " ^ floc#get_call_target#get_name; "rdefs: " ^ (String.concat ", " @@ -810,9 +830,8 @@ let translate_arm_instruction (List.map (fun u -> p2s u#toPretty) xpusehigh)) ] in - let usehigh = - usehigh @ xpusehigh @ (get_use_high_vars (List.map snd callargs)) in - let use = use @ xpuse in + let usehigh = xpusehigh @ (get_use_high_vars (List.map snd callargs)) in + let use = xpuse in let vr1 = floc#f#env#mk_arm_register_variable AR1 in let vr2 = floc#f#env#mk_arm_register_variable AR2 in let vr3 = floc#f#env#mk_arm_register_variable AR3 in