diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 762e1ac9..2dec08c7 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -734,6 +734,8 @@ object (self) method memrecorder = mk_memory_recorder self#f self#cia + method add_return = self#f#add_return self#cia + (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * * call targets * * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *) @@ -942,7 +944,10 @@ object (self) ~tag:"update_arm_varargs:no format arg info available" ~msg:self#cia __FILE__ __LINE__ - ["argxpr: " ^ (x2s (XVar v))] in + ["argxpr: " ^ (x2s (XVar v)); + "par_name: " ^ ftspar.apar_name; + "formatstring_type: " + ^ (formatstring_type_to_string ftspar.apar_fmt)] in None) | _ -> let _ = @@ -3734,16 +3739,48 @@ object (self) method private evaluate_fts_address_argument (p: fts_parameter_t):variable_t option = - let resolve_stack_address xpr tag = + let tag = "evaluate_fts_address_argument" in + let resolve_address_xpr (xpr: xpr_t): variable_t option = match xpr with - | XOp (XMinus, [XVar _v; XConst (IntConst n)]) when n#geq numerical_zero -> + (* xpr is an argument passed in to the caller via a register *) + | XVar v when self#f#env#is_initial_register_value v -> + TR.tfold + ~ok:(fun memvar -> + begin + log_diagnostics_result + ~tag:(tag ^ ":resolve_address_xpr:function parameter value") + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "xpr: " ^ (x2s xpr); + "memvar: " ^ (p2s memvar#toPretty)]; + Some memvar + end) + ~error:(fun e -> + begin + log_error_result + ~tag:(tag ^ ":resolve_address_xpr:function paramval: error") + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "xpr: " ^ (x2s xpr); + String.concat ", " e]; + None + end) + (self#f#env#mk_basevar_memory_variable v NoOffset) + + (* xpr is a stack address *) + | XOp (XMinus, [XVar v; XConst (IntConst n)]) + when self#f#env#is_initial_stackpointer_value v + && 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 stackvar = + self#f#env#mk_stackslot_variable stackslot NoOffset in let _ = log_diagnostics_result - ~tag:"evaluate_fts_address_argument:resolve_stack_address" + ~tag:(tag ^ ":resolve_address_xpr:stack") ~msg:(p2s self#l#toPretty) __FILE__ __LINE__ ["parameter: " ^ (fts_parameter_to_string p); @@ -3776,21 +3813,26 @@ object (self) | [RegisterParameter (r, _, _)] -> let argvar = self#env#mk_register_variable r in let xpr = self#rewrite_variable_to_external argvar in - resolve_stack_address xpr "evaluate_fts_address_argument" + resolve_address_xpr xpr | [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 -> + TR.tfold + ~ok:(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 + resolve_address_xpr xpr) + ~error:(fun e -> + begin + log_error_result + ~tag:"evaluate_fts_address_argument" + ~msg:self#cia + __FILE__ __LINE__ + ["offset: " ^ (string_of_int offset); String.concat ", " e]; + None + end) + (self#get_singleton_stackpointer_offset) | _ -> begin log_diagnostics_result diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 3f9092e0..cfb4aa24 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1700,6 +1700,7 @@ object (self) val stackframe = mk_function_stackframe fndata varmgr val proofobligations = mk_proofobligations faddr (mk_xpodictionary varmgr#vard#xd) + val mutable returnlocations = [] (* ------------------------------------------------------------------------- *) @@ -1714,6 +1715,12 @@ object (self) method stackframe = stackframe + method add_return (iaddr: ctxt_iaddress_t) = + if not (List.mem iaddr returnlocations) then + returnlocations <- iaddr :: returnlocations + + method return_locations = returnlocations + method xpod = self#proofobligations#xpod method proofobligations = proofobligations diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml index cdff664f..dd4550a2 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -31,6 +31,7 @@ open CHLanguage (* chutil *) open CHFormatStringParser open CHLogger +open CHTraceResult (* xprlib *) open XprTypes @@ -38,6 +39,7 @@ open Xsimplify (* bchlib *) open BCHBCTypes +open BCHBTerm open BCHExternalPredicate open BCHGlobalState open BCHLibTypes @@ -45,6 +47,10 @@ open BCHXPOPredicate module TR = CHTraceResult +let (let*) x f = CHTraceResult.tbind f x + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let p2s = CHPrettyUtil.pretty_to_string let x2p = XprToPretty.xpr_formatter#pr_expr @@ -171,6 +177,58 @@ let buffer_writer_callsite None end + +let external_buffer_writer_callsite + (finfo: function_info_int) + (loc: location_int) + (memvar: variable_t): location_int option = + let varinv = finfo#ivarinv loc#ci in + let rdfacts = List.filter (fun f -> f#is_reaching_def) varinv#get_facts in + let _ = + log_diagnostics_result + ~tag:"external_buffer_writer_callsite" + ~msg:loc#ci + __FILE__ __LINE__ + [String.concat ", " (List.map (fun f -> p2s f#toPretty) rdfacts)] in + let symvar = finfo#env#mk_symbolic_variable memvar in + let vinvs = varinv#get_var_reaching_defs symvar in + let defsites = + List.concat_map (fun vinv -> + List.filter_map (fun sym -> + let defcia = sym#getBaseName in + if defcia = "init" then + None + else if finfo#has_call_target defcia then + Some (BCHLocation.ctxt_string_to_location finfo#a defcia) + else + None) + vinv#get_reaching_defs) + vinvs in + (match defsites with + | [defloc] -> Some defloc + | [] -> + begin + log_diagnostics_result + ~tag:"buffer_writer_callsite:no defining locations" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["memvar: " ^ (p2s memvar#toPretty)]; + None + end + | _ -> + begin + log_diagnostics_result + ~tag:"buffer_writer_callsite:multiple defining locations" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["memvar: " ^ (p2s memvar#toPretty); + "defsites: " + ^ (String.concat ", " (List.map (fun l -> p2s l#toPretty) defsites))]; + None + end) + + + (* ========================================================================= Discharge strategies per PO type ========================================================================= *) @@ -274,11 +332,100 @@ let trusted_os_cmd_string_delegate_local Open +let trusted_os_cmd_string_parameter_postcondition + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + let tag = "trusted_os_cmd_string_parameter_postcondition" in + if not floc#has_call_target then + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); "not a call site"]; + Open + end + else + let ctinfo = floc#get_call_target in + match floc#get_bterm_evaluator with + | None -> + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); "no bterm evaluator found"]; + Open + end + | Some btermev -> + let check_bterm (bterm: bterm_t): bool = + match btermev#bterm_xpr bterm with + | Some xpost -> + let xpost' = floc#inv#rewrite_expr xpost in + (match simplify_xpr (XOp (XMinus, [xpost'; x])) with + | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero + | _ -> false) + | _ -> false in + List.fold_left (fun status post -> + match status with + | Open -> + (match post with + | XXTrustedOsCmdString bterm + | XXTrustedString bterm -> + if check_bterm bterm then + Discharged ( + "trusted-os-cmd-string postcondition from " + ^ ctinfo#get_name) + else + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); "xpr does not match term"]; + Open + end + | XXTainted bterm -> + if check_bterm bterm then + Violated ( + "postcondition of " + ^ ctinfo#get_name + ^ " states that value written may be tainted") + else + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); "xpr do not match"]; + Open + end + | p -> + begin + log_diagnostics_result + ~tag + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); + "pred: " ^ (p2s (xxpredicate_to_pretty p))]; + Open + end) + + | _ -> + status) Open ctinfo#get_postconditions + + let discharge_trusted_os_cmd_string (finfo: function_info_int) (loc: location_int) (x: xpr_t): po_status_t = let status = trusted_os_cmd_string_constant_string_stmt loc x in + let status = + match status with + | Open -> trusted_os_cmd_string_parameter_postcondition finfo loc x + | _ -> status in let status = match status with | Open -> trusted_os_cmd_string_delegate_local_instr finfo loc x @@ -465,13 +612,23 @@ let trusted_os_cmd_fmt_arg_string_parameter_postcondition Open end | Some btermev -> - let check_bterm (bterm: bterm_t): bool = + let check_bterm (p: xxpredicate_t) (bterm: bterm_t): bool = match btermev#bterm_xpr bterm with | Some xpost -> let xpost' = floc#inv#rewrite_expr xpost in (match simplify_xpr (XOp (XMinus, [xpost'; x])) with | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero - | _ -> false) + | _ -> + begin + log_diagnostics_result + ~tag:(tag ^ ": bterm mismatch") + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpred: " ^ (p2s (xxpredicate_to_pretty p)); + "xpost': " ^ (x2s xpost'); + "x: " ^ (x2s x)]; + false + end) | _ -> false in List.fold_left (fun status post -> match status with @@ -479,48 +636,30 @@ let trusted_os_cmd_fmt_arg_string_parameter_postcondition (match post with | XXTrustedOsCmdString bterm | XXTrustedString bterm -> - if check_bterm bterm then + if check_bterm post bterm then Discharged ( "trusted-os-cmd-string postcondition from " ^ ctinfo#get_name) else - begin - log_diagnostics_result - ~tag - ~msg:(p2s loc#toPretty) - __FILE__ __LINE__ - ["x: " ^ (x2s x); "xpr does not match term"]; - Open - end + Open + | XXTrustedOsCmdFmtArgString (bterm, q, _) when q = quotes -> - if check_bterm bterm then + if check_bterm post bterm then Discharged ( "trusted-os-cmd-fmt-arg-string postcondition from " ^ ctinfo#get_name) else - begin - log_diagnostics_result - ~tag - ~msg:(p2s loc#toPretty) - __FILE__ __LINE__ - ["x: " ^ (x2s x); "xpr do not match"]; - Open - end + Open + | XXTainted bterm -> - if check_bterm bterm then + if check_bterm post bterm then Violated ( "postcondition of " ^ ctinfo#get_name ^ " states that value written may be tainted") else - begin - log_diagnostics_result - ~tag - ~msg:(p2s loc#toPretty) - __FILE__ __LINE__ - ["x: " ^ (x2s x); "xpr do not match"]; - Open - end + Open + | p -> begin log_diagnostics_result @@ -1386,6 +1525,103 @@ let discharge_pass 0 openpos +(* ========================================================================== + Impose postconditions + ========================================================================== *) + +let bterm_to_variable + (finfo: function_info_int) (bterm: bterm_t): variable_t traceresult = + match bterm with + | ArgValue par -> + (match par.apar_location with + | [RegisterParameter (reg, _, _)] -> + Ok (finfo#env#mk_initial_register_value reg) + | [StackParameter (offset, _, _)] -> + let memref = finfo#env#mk_local_stack_reference in + let memvar = + finfo#env#mk_memory_variable memref (CHNumerical.mkNumerical offset) in + finfo#env#mk_initial_memory_value memvar + | _ -> + Error ["Unable to convert bterm to xpr: " ^ (bterm_to_string bterm)]) + | _ -> + Error ["Unable to convert bterm to xpr: " ^ (bterm_to_string bterm)] + + +let impose_trusted_os_cmd_string_pc + (finfo: function_info_int) + (bterm: bterm_t) + (returnlocs: ctxt_iaddress_t list):unit traceresult = + let* paramvar = bterm_to_variable finfo bterm in + let* memvar = finfo#env#mk_basevar_memory_variable paramvar NoOffset in + let errors = + List.fold_left (fun errors rcia -> + let loc = BCHLocation.ctxt_string_to_location finfo#get_address rcia in + match external_buffer_writer_callsite finfo loc memvar with + | Some defloc -> + let deffloc = BCHFloc.get_finfo_floc finfo defloc in + if call_writes_to_buffer deffloc (XVar paramvar) then + let xpo = XPOTrustedOsCmdString (XVar paramvar) in + begin + finfo#proofobligations#add_proofobligation defloc#ci xpo Open; + (log_diagnostics_result + ~tag:"impose_trusted_os_cmd_string_pc" + ~msg:(p2s defloc#toPretty) + __FILE__ __LINE__ + ["returnloc: " ^ rcia; + "xpo: " ^ (p2s (xpo_predicate_to_pretty xpo))]); + errors + end + else + [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; + "no buffer write"; + "returnloc: " ^ rcia; + "deffloc: " ^ (p2s deffloc#l#toPretty); + "memvar: " ^ (p2s memvar#toPretty)] @ errors + | _ -> + [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; + "no defloc"; + "returnloc: " ^ rcia; + "memvar: " ^ (p2s memvar#toPretty)] @ errors) + [] returnlocs in + match errors with + | [] -> Ok () + | e -> Error e + + +let impose_postconditions (finfo: function_info_int) = + let postconditions = finfo#get_summary#get_postconditions in + let returnlocs = finfo#return_locations in + let _ = + log_diagnostics_result + ~tag:"impose_postconditions" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["postconditions: " + ^ (String.concat "; " + (List.map + (fun p -> (p2s (xxpredicate_to_pretty p))) + postconditions)); + "return locations: " ^ (String.concat ", " returnlocs)] in + let errors = + List.fold_left (fun errors pc -> + match pc with + | XXTrustedOsCmdString bterm -> + (match impose_trusted_os_cmd_string_pc finfo bterm returnlocs with + | Ok _ -> errors + | Error e -> e @ errors) + | _ -> errors) [] postconditions in + let _ = + match errors with + | [] -> () + | _ -> + log_error_result + ~tag:"impose_postconditions" + ~msg:finfo#get_name + __FILE__ __LINE__ + errors in + () + + (* ========================================================================= Entry point ========================================================================= *) @@ -1405,6 +1641,7 @@ let discharge_pass let discharge_function_proofobligations ?(max_passes = 8) (finfo: function_info_int): unit = + let _ = impose_postconditions finfo in let rec loop n = if n = 0 then () diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index b917c5d7..e0e80daa 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -5807,6 +5807,12 @@ object (** Returns the object containing all active proof obligations.*) method proofobligations: proofobligations_int + (** Add the given address to the list of return locations.*) + method add_return: ctxt_iaddress_t -> unit + + (** Return instruction addresses in this function declared as return address.*) + method return_locations: ctxt_iaddress_t list + (** {1 Function invariants} *) @@ -6377,6 +6383,9 @@ class type floc_int = (** Returns the bytes of the instruction as a hexstring *) method get_instruction_bytes: string + (** Declares the current instruction to be a a return instruction *) + method add_return: unit + (** {1 Variables} *) (** {1 Invariants} *) diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 2cea2bf0..83785866 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_20260629" - ~date:"2026-06-29" + ~version:"0.6.0_20260703" + ~date:"2026-07-03" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index c69572c2..2dd33eb3 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -1302,7 +1302,8 @@ let translate_arm_instruction * BranchWritePC(targetAddress); * ------------------------------------------------------------------------ *) | BranchLink (c, tgt) - | BranchLinkExchange (c, tgt) when tgt#is_absolute_address -> + | BranchLinkExchange (c, tgt) + when tgt#is_absolute_address || floc#has_call_target -> if instr#is_inlined_call then default [] else @@ -2510,6 +2511,7 @@ let translate_arm_instruction xr0_r else [] in + let _ = if rl#includes_pc then floc#add_return in let popdefcmds = floc#get_vardef_commands ~defs:[splhs]