diff --git a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml index 32e19bdb..90b05399 100644 --- a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml @@ -27,6 +27,7 @@ (* chutil *) open CHFormatStringParser +open CHLogger open CHTraceResult open CHUtil @@ -584,7 +585,15 @@ let arm_vfp_params (funargs: bfunarg_t list): fts_parameter_t list = let fmt (index: int) = match BCHBCAttributesUtil.get_format_archetype attrs index with - | Some fmtstringtype -> fmtstringtype + | Some fmtstringtype -> + let _ = + log_diagnostics_result + ~tag:"arm_vfp_parameters" + __FILE__ __LINE__ + ["fmtstringtype: " + ^ (BCHFtsParameter.formatstring_type_to_string fmtstringtype); + "attr count: " ^ (string_of_int (List.length attrs))] in + fmtstringtype | _ -> NoFormat in let (_, _, params) = List.fold_left diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 6751f135..06e02e35 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -1040,63 +1040,116 @@ let get_access_sideeffect end -let get_chk_post_one +let get_chk_post_conditions (name: string) (fparams: fts_parameter_t list) (attrparams: b_attrparam_t list): xxpredicate_t list = let thisf = NamedConstant name in let rv = ReturnValue thisf in let zero = NumConstant CHNumerical.numerical_zero in - (* Resolve target term: bare predicate → return value; predicate + AInt → parameter *) - let target_result = - match attrparams with - | [ACons (pred, [])] -> Ok (pred, rv) - | [ACons (pred, []); AInt refindex] -> + let negone = NumConstant (CHNumerical.mkNumerical (-1)) in + let get_param (pl: b_attrparam_t list): bterm_t traceresult = + match pl with + | [] -> Ok rv + | [AInt 0] -> Ok rv + | [AInt refindex] when refindex > 0 -> let* par = get_par fparams refindex in - Ok (pred, ArgValue par) - | (ACons (tag, _)) :: _ -> - Error [(elocm __LINE__) ^ "chk_post tag not recognized: " ^ tag] + Ok (ArgValue par) | _ -> Error [(elocm __LINE__) ^ "chk_post params not recognized"; - attrparams_to_string "attrparams" attrparams] in - TR.tfold - ~error:(fun e -> - begin - log_diagnostics_result - ~tag:"get_chk_post_one:not recognized" - ~msg:name - __FILE__ __LINE__ - e; - [] - end) - ~ok:(fun (pred, target) -> - let negone = NumConstant (CHNumerical.mkNumerical (-1)) in - match pred with - | "not_null" -> [XXNotNull target] - | "null" -> [XXNull target] - | "non_negative" -> [XXNonNegative target] - | "not_zero" -> [XXNotZero target] - | "positive" -> [XXPositive target] - | "null_terminated" -> [XXNullTerminated target] - | "new_memory" -> [XXNewMemory (target, RunTimeValue)] - | "allocation_base" -> [XXAllocationBase target] - | "trusted_string" -> [XXTrustedString target] - | "trusted_os_cmd_string" -> [XXTrustedOsCmdString target] - | "tainted" -> [XXTainted target] - | "negone" -> [XXRelationalExpr (PEquals, target, negone)] - | "zero" -> [XXRelationalExpr (PEquals, target, zero)] - | "negative" -> [XXRelationalExpr (PLessThan, target, zero)] - | "nonpositive" -> [XXRelationalExpr (PLessEqual, target, zero)] - | tag -> - begin - log_diagnostics_result - ~tag:"get_chk_post_one:tag not recognized" - ~msg:name - __FILE__ __LINE__ - ["tag: " ^ tag]; - [] - end) - target_result + attrparams_to_string "attrparams" pl] in + let get_two_params (pl: b_attrparam_t list): (bterm_t * bterm_t) traceresult = + match pl with + | [AInt 0; AInt p2] -> + let* par = get_par fparams p2 in + Ok (rv, ArgValue par) + | [AInt p1; AInt p2] -> + let* par1 = get_par fparams p1 in + let* par2 = get_par fparams p2 in + Ok (ArgValue par1, ArgValue par2) + | _ -> + Error [(elocm __LINE__) ^ "chk_post params not recognized"; + attrparams_to_string "attrparams" pl] in + let xpred = + match attrparams with + | (ACons ("not_null", [])) :: refparams -> + TR.tmap (fun t -> [XXNotNull t]) (get_param refparams) + | (ACons ("null", [])) :: refparams -> + TR.tmap (fun t -> [XXNull t]) (get_param refparams) + | (ACons ("non_negative", [])) :: refparams -> + TR.tmap (fun t -> [XXNonNegative t]) (get_param refparams) + | (ACons ("not_zero", [])) :: refparams -> + TR.tmap (fun t -> [XXNotZero t]) (get_param refparams) + | (ACons ("positive", [])) :: refparams -> + TR.tmap (fun t -> [XXPositive t]) (get_param refparams) + | (ACons ("null_terminated", [])) :: refparams -> + TR.tmap (fun t -> [XXNullTerminated t]) (get_param refparams) + | (ACons ("new_memory", [])) :: ([_; _] as refparams) -> + TR.tmap + (fun (t, sizeparam) -> [XXNewMemory (t, sizeparam)]) + (get_two_params refparams) + | (ACons ("new_memory", [])) :: refparams -> + TR.tmap (fun t -> [XXNewMemory (t, RunTimeValue)]) (get_param refparams) + | (ACons ("new_memory", [AInt size])) :: refparams -> + let asize = NumConstant (CHNumerical.mkNumerical size) in + TR.tmap (fun t -> [XXNewMemory (t, asize)]) (get_param refparams) + | (ACons ("allocation_base", [])) :: refparams -> + TR.tmap (fun t -> [XXAllocationBase t]) (get_param refparams) + | (ACons ("trusted_string", [])) :: refparams -> + TR.tmap (fun t -> [XXTrustedString t]) (get_param refparams) + | (ACons ("trusted_os_cmd_string", [])) :: refparams -> + TR.tmap (fun t -> [XXTrustedOsCmdString t]) (get_param refparams) + | (ACons ("trusted_os_cmd_fmt_arg_string", [])) :: refparams -> + TR.tmap + (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, None)]) + (get_param refparams) + | (ACons ("trusted_os_cmd_fmt_arg_string", [ACons ("no_quotes", [])])) + :: refparams -> + TR.tmap + (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, None)]) + (get_param refparams) + | (ACons ("trusted_os_cmd_fmt_arg_string", + [ACons ("no_quotes", []); AInt size])) :: refparams -> + TR.tmap + (fun t -> [XXTrustedOsCmdFmtArgString (t, NO_QUOTES, Some size)]) + (get_param refparams) + | (ACons ("tainted", [])) :: refparams -> + TR.tmap (fun t -> [XXTainted t]) (get_param refparams) + | (ACons ("negone", [])) :: refparams -> + TR.tmap + (fun t -> [XXRelationalExpr (PEquals, t, negone)]) + (get_param refparams) + | (ACons ("zero", [])) :: refparams -> + TR.tmap + (fun t -> [XXRelationalExpr (PEquals, t, zero)]) + (get_param refparams) + | (ACons ("negative", [])) :: refparams -> + TR.tmap + (fun t -> [XXRelationalExpr (PLessThan, t, zero)]) + (get_param refparams) + | (ACons ("nonpositive", [])) :: refparams -> + TR.tmap + (fun t -> [XXRelationalExpr (PLessEqual, t, zero)]) + (get_param refparams) + | (ACons (tag, _)) :: _ -> + Error [(elocm __LINE__) + ^ "chk_post tag " ^ tag ^ " not recognized in " + ^ (attrparams_to_string "argparams" attrparams)] + | _ -> + Error [(elocm __LINE__) + ^ "chk_post attrparams not recognized: " + ^ (attrparams_to_string "argparams" attrparams)] in + match xpred with + | Ok xl -> xl + | Error e -> + begin + log_error_result + ~tag:"get_check_post_conditions" + ~msg:name + __FILE__ __LINE__ + [String.concat "; " e]; + [] + end let get_chk_qual_conditions @@ -1184,11 +1237,11 @@ let convert_b_attributes_to_function_conditions (xpre, side @ xside, xpost, xepost, xqual) | Attr ("chk_post", attrparams) -> - let post = get_chk_post_one name fparameters attrparams in + let post = get_chk_post_conditions name fparameters attrparams in (xpre, xside, post @ xpost, xepost, xqual) | Attr ("chk_epost", attrparams) -> - let epost = get_chk_post_one name fparameters attrparams in + let epost = get_chk_post_conditions name fparameters attrparams in (xpre, xside, xpost, epost @ xepost, xqual) | Attr ("chk_qual", attrparams) -> diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 2a8aa8a5..43766f83 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -188,8 +188,17 @@ object (self) finfo#update_summary (finfo#get_summary#add_register_parameter_location reg btype 4) in - let ftspar = finfo#get_summary#get_parameter_for_register reg in - Some (ArgValue ftspar)) + TR.tfold + ~ok:(fun ftspar -> Some (ArgValue ftspar)) + ~error:(fun e -> + begin + log_error_result + ~tag:"xpr_to_bterm" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + None + end) + (finfo#get_summary#get_parameter_for_register reg)) ~error:(fun e -> begin log_error_result @@ -232,15 +241,23 @@ object (self) match xpr with | XConst (IntConst n) -> Some (NumConstant n) | XVar v when self#finfo#env#is_initial_register_value v -> - log_tfold - (log_error "xpr_to_bterm" "invalid register") + TR.tfold ~ok:(fun reg -> let _ = self#finfo#update_summary (self#finfo#get_summary#add_register_parameter_location reg btype 4) in - let ftspar = self#finfo#get_summary#get_parameter_for_register reg in - Some (ArgValue ftspar)) + TR.tfold + ~ok:(fun ftspar -> Some (ArgValue ftspar)) + ~error:(fun e -> + begin + log_error_result + ~tag:"xpr_to_bterm" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + None + end) + (self#finfo#get_summary#get_parameter_for_register reg)) ~error:(fun _ -> None) (self#finfo#env#get_initial_register_value_register v) | XVar v when self#finfo#env#is_stack_parameter_value v -> @@ -378,6 +395,9 @@ object (self) | Some xpr -> match xpr with | XConst (IntConst n) -> + (* The callee is a variadic function. Retrieve the actual format + string and parse it to determine the number of variadic arguments + in the call.*) let dw = BCHDoubleword.numerical_mod_to_doubleword n in if BCHStrings.string_table#has_string dw then let fmtstring = BCHStrings.string_table#get_string dw in @@ -417,6 +437,82 @@ object (self) ["No constant format string found in string table"]; None end + | XVar v when self#finfo#env#is_initial_register_value v -> + (* There is no constant format string. Instead the format string + argument is received from the caller's parameter. Retrieve the + the specification of the parameter by externalizing the expression + to a parameter. If the parameter spec (as obtained from a + header file) is a retricted format string, reconstruct a minimal + format string from its argument spec list, and parse in the + same way as before.*) + let bterm_o = + (new arm_expression_externalizer_t finfo)#xpr_to_bterm + t_charptr (XVar v) in + (match bterm_o with + | Some (ArgValue ftspar) -> + (match ftspar.apar_fmt with + | RestrictedPrintFormat sl when sl <> [] -> + let fmtstring = + String.concat " " (List.map (fun s -> "%" ^ s) sl) in + let _ = + log_diagnostics_result + ~tag:"get_annotated_format_arguments:restricted_format" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["restricted fmtstring: " ^ fmtstring] in + let fmtspec = parse_formatstring fmtstring false in + if fmtspec#has_arguments then + let argspecs = fmtspec#get_arguments in + let argxprs = List.map (fun (_, x) -> x) callargs in + (match CHUtil.list_slice argxprs + index (List.length argspecs) with + | Some fmtargs -> + Some + (List.map2 + (fun argspec argxpr -> + let fw = + if argspec#has_fieldwidth then + argspec#get_fieldwidth + else + CHFormatStringParser.NoFieldwidth in + (argspec#get_conversion, fw, argxpr)) + argspecs fmtargs) + | _ -> + begin + log_diagnostics_result + ~tag:"get_annotated_format_arguments:no formatargs" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["restricted fmtstring: no arguments: " ^ fmtstring]; + None + end) + else + begin + log_diagnostics_result + ~tag:"get_annotated_format_arguments:restricted_format" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["restricted fmtstring: no arguments: " ^ fmtstring]; + None + end + | _ -> + begin + log_diagnostics_result + ~tag:"get_annotated_format_arguments: ftspar: no format" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["param: " ^ (fts_parameter_to_string ftspar)]; + None + end) + | _ -> + begin + log_diagnostics_result + ~tag:"get_annotated_format_arguments:initial_register_value" + ~msg:finfo#get_name + __FILE__ __LINE__ + ["format string: " ^ (p2s v#toPretty)]; + None + end) | _ -> begin log_diagnostics_result @@ -2233,8 +2329,10 @@ object (self) ~msg:(eloc __LINE__) (fun reg -> if self#f#get_summary#has_parameter_for_register reg then - let param = self#f#get_summary#get_parameter_for_register reg in - Ok param.apar_type + TR.tbind + ~msg:(eloc __LINE__) + (fun param -> Ok param.apar_type) + (self#f#get_summary#get_parameter_for_register reg) else let ty = self#env#get_variable_type v in match ty with @@ -3360,10 +3458,19 @@ object (self) [ABSTRACT_VARS [lhs]] else + let fndata = self#f#get_function_data in let rhs = + if fndata#has_regvar_freeze self#ia then + let _ = + log_diagnostics_result + ~tag:"get_assign_commands_r:freeze" + ~msg:self#cia + __FILE__ __LINE__ + ["lhs: " ^ (p2s lhs#toPretty)] in + XVar (self#f#env#mk_frozen_value lhs self#cia) (* if rhs is a composite symbolic expression, create a new variable for it *) - if self#is_composite_symbolic_value rhs then + else if self#is_composite_symbolic_value rhs then XVar (self#env#mk_symbolic_value rhs) else rhs in @@ -3372,7 +3479,7 @@ object (self) let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in - let fndata = self#f#get_function_data in + match fndata#get_regvar_intro self#ia with | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype -> TR.tfold diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index d9b57963..c9dafc6a 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -293,6 +293,13 @@ object (self) (fun rvi -> rvi.rvi_iaddr#equal iaddr && rvi.rvi_cast) a.regvarintros | _ -> false + method has_regvar_freeze (iaddr: doubleword_int): bool = + match self#get_function_annotation with + | Some a -> + List.exists + (fun rvi -> rvi.rvi_iaddr#equal iaddr && rvi.rvi_freeze) a.regvarintros + | _ -> false + method has_stackvar_type_cast (offset: int): bool = match self#get_function_annotation with | Some a -> @@ -683,6 +690,7 @@ let read_xml_regvar_intro (node: xml_element_int): regvar_intro_t traceresult = (fun dw -> let rvi_iaddr = dw in let rvi_name = get "name" in + let rvi_freeze = (has "freeze") && ((get "freeze") = "yes") in let (rvi_vartype, rvi_cast) = if has "typename" then let iscast = (has "cast") && ((get "cast") = "yes") in @@ -704,6 +712,7 @@ let read_xml_regvar_intro (node: xml_element_int): regvar_intro_t traceresult = Ok {rvi_iaddr = rvi_iaddr; rvi_name = rvi_name; rvi_cast = rvi_cast; + rvi_freeze = rvi_freeze; rvi_vartype = rvi_vartype}) (string_to_doubleword (get "iaddr")) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index b58ee381..3f9092e0 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -996,6 +996,10 @@ object (self) (var:variable_t) (taddr:ctxt_iaddress_t) (jaddr:ctxt_iaddress_t) = self#mk_variable (varmgr#make_frozen_test_value var taddr jaddr) + method mk_frozen_value + (var: variable_t) (iaddr: ctxt_iaddress_t): variable_t = + self#mk_variable (varmgr#make_frozen_value var iaddr) + method mk_special_variable (name:string) = self#mk_variable (varmgr#make_special_variable name) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml index 5dfa668d..6149fc05 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -147,7 +147,8 @@ let buffer_writer_callsite ~msg:(p2s loc#toPretty) __FILE__ __LINE__ ["xpr: " ^ (x2s xpr); - "memvar: " ^ (p2s memvar#toPretty)]; + "memvar: " ^ (p2s memvar#toPretty); + "stackslot: " ^ (slot#name ^ "@" ^ (string_of_int slot#offset))]; None end | _ -> @@ -373,7 +374,8 @@ let discharge_trusted_os_cmd_fmt_string ~tag:"discharge_trusted_os_cmd_fmt_string" ~msg:(p2s loc#toPretty) __FILE__ __LINE__ - ["x: " ^ (x2s x)]; + ["x: " ^ (x2s x); + "fmtarg count: " ^ (string_of_int (List.length fmtargs))]; status end | _ -> @@ -395,7 +397,7 @@ let trusted_os_cmd_fmt_arg_string_constant_string_stmt postcondition on the call that produced [x] as its return value. *) let trusted_os_cmd_fmt_arg_string_return_value_postcondition (finfo: function_info_int) - (_loc: location_int) + (loc: location_int) (x: xpr_t) (_quotes: quote_status_t) (_optlen: int option): po_status_t = @@ -419,18 +421,132 @@ let trusted_os_cmd_fmt_arg_string_return_value_postcondition Violated ("return value of " ^ ctinfo#get_name ^ " is potentially tainted") else Open) - ~error:(fun _ -> Open) + ~error:(fun e -> + begin + log_error_result + ~tag:"trusted_os_cmd_fmt_arg_string_return_value_postcondition" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); String.concat "; " e]; + Open + end) (finfo#env#get_call_site v) - | _ -> Open + | _ -> + Open -let trusted_os_cmd_fmt_arg_string_delegate_local - (_finfo: function_info_int) - (_loc: location_int) - (_x: xpr_t) - (_quotes: quote_status_t) +let trusted_os_cmd_fmt_arg_string_parameter_postcondition + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t) + (quotes: quote_status_t) (_optlen: int option): po_status_t = - Open + let floc = BCHFloc.get_finfo_floc finfo loc in + let tag = "trusted_os_cmd_fmt_arg_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 + | XXTrustedOsCmdFmtArgString (bterm, q, _) when q = quotes -> + if check_bterm 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 + | 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 trusted_os_cmd_fmt_arg_string_delegate_local + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t) + (quotes: quote_status_t) + (optlen: int option): po_status_t = + match buffer_writer_callsite finfo loc xpr with + | None -> + begin + log_diagnostics_result + ~tag:"trusted_os_cmd_fmt_arg_string_delegate_local:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["finfo: " ^ finfo#get_name; "xpr: " ^ (x2s xpr)]; + Open + end + | Some defloc -> + let deffloc = BCHFloc.get_finfo_floc finfo defloc in + if call_writes_to_buffer deffloc xpr then + begin + let new_xpo = XPOTrustedOsCmdFmtArgString (xpr, quotes, optlen) in + finfo#proofobligations#add_proofobligation defloc#ci new_xpo Open; + DelegatedLocal (defloc#ci, new_xpo) + end + else + Open let discharge_trusted_os_cmd_fmt_arg_string @@ -447,6 +563,12 @@ let discharge_trusted_os_cmd_fmt_arg_string trusted_os_cmd_fmt_arg_string_return_value_postcondition finfo loc x quotes optlen | _ -> status in + let status = + match status with + | Open -> + trusted_os_cmd_fmt_arg_string_parameter_postcondition + finfo loc x quotes optlen + | _ -> status in let status = match status with | Open -> @@ -479,11 +601,22 @@ let output_format_string_delegate ~ok:(fun reg -> let _ = finfo#add_register_parameter_location reg BCHBCTypeUtil.t_charptr 4 in - let ftspar = finfo#get_summary#get_parameter_for_register reg in - let dst = ArgValue ftspar in - let xpred = XXOutputFormatString dst in - let _ = finfo#add_precondition xpred in - Delegated xpred) + TR.tfold + ~ok:(fun ftspar -> + let dst = ArgValue ftspar in + let xpred = XXOutputFormatString dst in + let _ = finfo#add_precondition xpred in + Delegated xpred) + ~error:(fun e -> + begin + log_error_result + ~tag:"discharge_output_format_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + Open + end) + (finfo#get_summary#get_parameter_for_register reg)) ~error:(fun e -> begin log_error_result @@ -568,11 +701,22 @@ let restricted_output_format_string_delegate ~ok:(fun reg -> let _ = finfo#add_register_parameter_location reg BCHBCTypeUtil.t_charptr 4 in - let ftspar = finfo#get_summary#get_parameter_for_register reg in - let dst = ArgValue ftspar in - let xpred = XXRestrictedOutputFormatString (dst, sl) in - let _ = finfo#add_precondition xpred in - Delegated xpred) + TR.tfold + ~ok:(fun ftspar -> + let dst = ArgValue ftspar in + let xpred = XXRestrictedOutputFormatString (dst, sl) in + let _ = finfo#add_precondition xpred in + Delegated xpred) + ~error:(fun e -> + begin + log_error_result + ~tag:"discharge_restricted_output_format_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + Open + end) + (finfo#get_summary#get_parameter_for_register reg)) ~error:(fun e -> begin log_error_result diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index 5692bb51..f4cb5791 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.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 @@ -33,6 +33,7 @@ open CHPretty (* chutil *) open CHLogger open CHPrettyUtil +open CHTraceResult open CHXmlDocument open CHXmlReader @@ -47,6 +48,9 @@ open BCHFunctionSemantics open BCHLibTypes +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + let raise_xml_error (node:xml_element_int) (msg:pretty_t) = let error_msg = LBLOCK [ @@ -137,14 +141,16 @@ object (self:'a) method get_parameters = get_fts_parameters self#get_function_interface - method get_parameter_for_register (reg: register_t): fts_parameter_t = + (* This operation may fail in the first few analysis rounds if the parameter + is a variadic parameter and the full signature has not been constructed + from the format string.*) + method get_parameter_for_register (reg: register_t): fts_parameter_t traceresult = let rpar = get_register_parameter_for_register self#get_function_interface reg in match rpar with - | Some p -> p + | Some p -> Ok p | _ -> - raise - (BCH_failure - (LBLOCK [STR "Internal error: get_parameter_for_register"])) + Error [(elocm __LINE__) + ^ "get_parameter_for_register: " ^ (register_to_string reg)] method has_parameter_for_register (reg: register_t): bool = Option.is_some diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 1ec36617..b5797194 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1507,7 +1507,8 @@ type regvar_intro_t = { rvi_iaddr: doubleword_int; rvi_name: string; rvi_vartype: btype_t option; - rvi_cast: bool + rvi_cast: bool; + rvi_freeze: bool } (** Local stack variable introduced via userdata. @@ -1619,6 +1620,7 @@ class type function_data_int = method has_regvar_type_annotation: doubleword_int -> bool method get_regvar_type_annotation: doubleword_int -> btype_t traceresult method has_regvar_type_cast: doubleword_int -> bool + method has_regvar_freeze: doubleword_int -> bool method get_regvar_intro: doubleword_int -> regvar_intro_t option (** {2 Stack-variable introductions} *) @@ -2545,7 +2547,7 @@ object ('a) method get_parameters: fts_parameter_t list - method get_parameter_for_register: register_t -> fts_parameter_t + method get_parameter_for_register: register_t -> fts_parameter_t traceresult method has_parameter_for_register: register_t -> bool @@ -3756,6 +3758,13 @@ and constant_value_variable_t = that is used as a predicate for a conditional jump instruction (or other condition instruction) at address [j_iaddr]*) + | FrozenValue of variable_t * ctxt_iaddress_t + (** [FrozenValue (var, iaddr): frozen value of variable var at address iaddr. + The difference with a frozen test value is that this value is created + on demand to preserve a value to be used in invariants; the corresponding + variable does not get abstracted, as is the case with frozen test + variables.*) + | FunctionReturnValue of ctxt_iaddress_t (** [FunctionReturnValue iaddr]: return value from call at instruction address [iaddr]*) @@ -4108,6 +4117,9 @@ object -> ctxt_iaddress_t -> assembly_variable_int + method make_frozen_value: + variable_t -> ctxt_iaddress_t -> assembly_variable_int + (** [make_bridge_value addr argix] returns a bridge value for the variable [var] that is the stack argument with index [argix] (1-based) for a call (x86 only).*) @@ -5205,6 +5217,7 @@ class type function_environment_int = method mk_frozen_test_value: variable_t -> ctxt_iaddress_t -> ctxt_iaddress_t -> variable_t + method mk_frozen_value: variable_t -> ctxt_iaddress_t -> variable_t method mk_special_variable: string -> variable_t method mk_runtime_constant: string -> variable_t method mk_return_value: ctxt_iaddress_t -> variable_t diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 45eedab3..508f578c 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -799,6 +799,7 @@ object | InitialRegisterValue _ -> "ir" | InitialMemoryValue _ -> "iv" | FrozenTestValue _ -> "ft" + | FrozenValue _ -> "frv" | FunctionReturnValue _ -> "fr" | TypeCastValue _ -> "tc" | SyscallErrorReturnValue _ -> "ev" @@ -814,7 +815,7 @@ object | ChifTemp -> "chiftemp" method !tags = [ - "bv"; "chiftemp"; "ct"; "ev"; "fr"; "fp"; "ft"; "fv"; "ir"; + "bv"; "chiftemp"; "ct"; "ev"; "fp"; "fr"; "frv"; "ft"; "fv"; "ir"; "iv"; "rt"; "se" ; "sp"; "sv"; "ssv"; "tc"] end diff --git a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml index fa0a10b0..1b85e16b 100644 --- a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHVarDictionary.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 @@ -253,6 +253,7 @@ object (self) | InitialMemoryValue v -> (tags, [xd#index_variable v]) | FrozenTestValue (v, a1, a2) -> (tags @ [a1; a2], [xd#index_variable v]) + | FrozenValue (v, a) -> (tags @ [a], [xd#index_variable v]) | FunctionReturnValue a -> (tags @ [a], []) | TypeCastValue (iaddr, name, ty, reg) -> (tags @ [iaddr; name], [bcd#index_typ ty; bd#index_register reg]) @@ -284,6 +285,7 @@ object (self) | "ir" -> InitialRegisterValue (bd#get_register (a 0), a 1) | "iv" -> InitialMemoryValue (xd#get_variable (a 0)) | "ft" -> FrozenTestValue (xd#get_variable (a 0), t 1, t 2) + | "frv" -> FrozenValue (xd#get_variable (a 0), t 1) | "fr" -> FunctionReturnValue (t 1) | "tc" -> TypeCastValue (t 1, t 2, bcd#get_typ (a 0), bd#get_register (a 1)) | "ev" -> SyscallErrorReturnValue (t 1) diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 5cd052fa..91b1d1bd 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -107,7 +107,9 @@ object (self:'a) (if level = 0 then "" else "_" ^ (string_of_int level)) | InitialMemoryValue v -> v#getName#getBaseName ^ "_in" | FrozenTestValue (fv,taddr,jaddr) -> - fv#getName#getBaseName ^ "_val_" ^ taddr ^ "_amp_" ^ jaddr + fv#getName#getBaseName ^ "_val_" ^ taddr ^ "_amp_" ^ jaddr + | FrozenValue (fv, iaddr) -> + fv#getName#getBaseName ^ "_val_" ^ iaddr | FunctionPointer (fname,cname,address) -> "fp_" ^ fname ^ "_" ^ cname ^ "_" ^ address | FunctionReturnValue address -> "rtn_" ^ address @@ -196,6 +198,7 @@ object (self:'a) | InitialRegisterValue _ -> None | InitialMemoryValue _ -> None | FrozenTestValue _ -> None + | FrozenValue _ -> None | FunctionPointer _ -> None | FunctionReturnValue _ -> None | TypeCastValue (_, _, ty, _) -> Some ty @@ -327,6 +330,7 @@ object (self:'a) | InitialMemoryValue _ | FunctionReturnValue _ | TypeCastValue _ + | FrozenValue _ | CallTargetValue _ | SideEffectValue _ | FieldValue _ @@ -697,6 +701,10 @@ object (self) (var:variable_t) (taddr:ctxt_iaddress_t) (jaddr:ctxt_iaddress_t) = self#mk_variable (AuxiliaryVariable (FrozenTestValue (var, taddr, jaddr))) + method make_frozen_value + (var: variable_t) (iaddr: ctxt_iaddress_t): assembly_variable_int = + self#mk_variable (AuxiliaryVariable (FrozenValue (var, iaddr))) + method make_bridge_value (address:ctxt_iaddress_t) (argnr:int) = self#mk_variable (AuxiliaryVariable (BridgeVariable (address, argnr))) @@ -883,6 +891,11 @@ object (self) | (TypeCastValue _, _) -> -1 | (_, TypeCastValue _) -> 1 + | (FrozenValue (_, iaddr1), FrozenValue (_, iaddr2)) -> + Stdlib.compare iaddr1 iaddr2 + | (FrozenValue _, _) -> -1 + | (_, FrozenValue _) -> 1 + | (FunctionReturnValue _, FunctionReturnValue _) -> Stdlib.compare ix1 ix2 | (FunctionReturnValue _, _) -> -1 | (_, FunctionReturnValue _) -> 1 diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index a203fa99..6d908fba 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_20260619" - ~date:"2026-06-19" + ~version:"0.6.0_20260625" + ~date:"2026-06-25" ~licensee: None ~maxfilesize: None ()