From 2efbcbe12806b709f86f889d04fb54cd5af41164 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 5 May 2026 23:07:24 -0700 Subject: [PATCH 01/15] CHB: add infrastructure for TrustedOsCmdString --- CodeHawk/CHB/bchlib/bCHExternalPredicate.ml | 45 ++++++++++++++++++- CodeHawk/CHB/bchlib/bCHExternalPredicate.mli | 9 +++- CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 7 ++- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 13 ++++++ CodeHawk/CHB/bchlib/bCHPrecondition.ml | 24 +++++++++- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 16 ++++++- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli | 1 + CodeHawk/CHB/bchlib/bCHXPODictionary.ml | 5 ++- CodeHawk/CHB/bchlib/bCHXPOPredicate.ml | 13 ++++++ .../CHB/bchsummaries/so_functions/system.xml | 11 ++++- 10 files changed, 135 insertions(+), 9 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index c5abf9f33..373b41899 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml @@ -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 @@ -30,6 +30,7 @@ open CHPretty (* chutil *) open CHLogger +open CHTraceResult (* xprlib *) open XprTypes @@ -46,6 +47,27 @@ open BCHLibTypes open BCHUtilities + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + +let quote_status_to_string (q: quote_status_t): string = + match q with + | NO_QUOTES -> "NO_QUOTES" + | SINGLE_QUOTES -> "SINGLE_QUOTES" + | DOUBLE_QUOTES -> "DOUBLE_QUOTES" + + +let string_to_quote_status (s: string): quote_status_t traceresult = + match s with + | "NO_QUOTES" -> Ok NO_QUOTES + | "SINGLE_QUOTES" -> Ok SINGLE_QUOTES + | "DOUBLE_QUOTES" -> Ok DOUBLE_QUOTES + | _ -> + Error [(elocm __LINE__) ^ "Illegal quote_status: " ^ s] + + let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = let btc = bterm_compare in match (p1, p2) with @@ -151,6 +173,12 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = | (XXTainted t1, XXTainted t2) -> btc t1 t2 | (XXTainted _, _) -> -1 | (_, XXTainted _) -> 1 + | (XXTrustedString t1, XXTrustedString t2) -> btc t1 t2 + | (XXTrustedString _, _) -> -1 + | (_, XXTrustedString _) -> 1 + | (XXTrustedOsCmdString (t1, _, _), XXTrustedOsCmdString (t2, _, _)) -> btc t1 t2 + | (XXTrustedOsCmdString _, _) -> -1 + | (_, XXTrustedOsCmdString _) -> 1 | (XXValidMem t1, XXValidMem t2) -> btc t1 t2 | (XXValidMem _, _) -> -1 | (_, XXValidMem _) -> 1 @@ -198,6 +226,8 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list = | XXSetsErrno -> [] | XXStartsThread (t, tt) -> t :: tt | XXTainted t -> [t] + | XXTrustedString t -> [t] + | XXTrustedOsCmdString (t, _, _) -> [t] | XXValidMem t -> [t] | XXDisjunction pl -> List.concat (List.map xxpredicate_terms pl) | XXConditional (p1, p2) -> @@ -347,6 +377,16 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) = | XXSetsErrno -> STR "sets errno" | XXStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XXTainted t -> default "tainted" [t] + | XXTrustedString t -> default "trusted-string" [t] + | XXTrustedOsCmdString (t, isfmtstring, quotes) -> + LBLOCK [ + STR "trusted-os-cmd-string("; + btp t; + STR ", "; + STR (if isfmtstring then "true" else "false"); + STR ", "; + STR (quote_status_to_string quotes); + STR ")"] | XXValidMem t -> default "valid-mem" [t] | XXDisjunction pl -> pretty_print_list pl xxpredicate_to_pretty "[" " || " "]" @@ -391,6 +431,9 @@ let rec modify_types_xxp | XXSetsErrno -> XXSetsErrno | XXStartsThread (t, tt) -> XXStartsThread (mbt t, List.map mbt tt) | XXTainted t -> XXTainted (mbt t) + | XXTrustedString t -> XXTrustedString (mbt t) + | XXTrustedOsCmdString (t, isfmtstring, q) -> + XXTrustedOsCmdString (mbt t, isfmtstring, q) | XXValidMem t -> XXValidMem (mbt t) | XXDisjunction xl -> XXDisjunction (List.map mxp xl) | XXConditional (x1, x2) -> XXConditional (mxp x1, mxp x2) diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli b/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli index 8b03af2f2..0213ea47c 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.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 @@ -28,6 +28,9 @@ (* chlib *) open CHPretty +(* chutil *) +open CHTraceResult + (* xprlib *) open XprTypes @@ -79,6 +82,10 @@ val xxpredicate_terms: xxpredicate_t -> bterm_t list (** {1 Printing}*) +val quote_status_to_string: quote_status_t -> string + +val string_to_quote_status: string -> quote_status_t traceresult + val relational_op_to_string: relational_op_t -> string val relational_op_to_xml_string: relational_op_t -> string diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 6b1edf68b..5c9d70423 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 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 @@ -521,6 +521,9 @@ object (self) | XXSetsErrno -> (tags, []) | XXStartsThread (t, tl) -> (tags, List.map it (t::tl)) | XXTainted t -> (tags, [it t]) + | XXTrustedString t -> (tags, [it t]) + | XXTrustedOsCmdString (t, isfmtstring, q) -> + (tags @ [quote_status_mfts#ts q], [it t; if isfmtstring then 1 else 0]) | XXValidMem t -> (tags, [it t]) | XXDisjunction pl -> (tags, [self#index_xxpredicate_list pl]) | XXConditional (p1, p2) -> @@ -573,6 +576,8 @@ object (self) | "errno" -> XXSetsErrno | "st" -> XXStartsThread (gt (a 0), List.map gt (List.tl args)) | "t" -> XXTainted (gt (a 0)) + | "tc" -> XXTrustedOsCmdString (gt (a 0), (a 1) = 1, quote_status_mfts#fs (t 1)) + | "ts" -> XXTrustedString (gt (a 0)) | "v" -> XXValidMem (gt (a 0)) | "dis" -> XXDisjunction (self#get_xxpredicate_list (a 0)) | "con" -> XXConditional (self#get_xxpredicate (a 0), self#get_xxpredicate (a 1)) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index ea449c288..3236927fb 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2363,6 +2363,9 @@ type c_struct_constant_t = | FieldCallTarget of call_target_t +type quote_status_t = NO_QUOTES | SINGLE_QUOTES | DOUBLE_QUOTES + + (** Predicate over external terms to represent function preconditions, postconditions, and side effects.*) type xxpredicate_t = @@ -2408,6 +2411,7 @@ type xxpredicate_t = | XXNullTerminated of bterm_t (** term points to null-terminated string *) | XXOutputFormatString of bterm_t (** term points to format string for output (e.g., sprintf) *) + | XXRelationalExpr of relational_op_t * bterm_t * bterm_t (** relational expression *) | XXSetsErrno @@ -2415,8 +2419,15 @@ type xxpredicate_t = (** starts a thread with [t1] as start address and the remaining terms as parameters *) | XXTainted of bterm_t (** value of term is externally controlled *) + | XXTrustedString of bterm_t (** value of term is trusted *) + | XXTrustedOsCmdString of bterm_t * bool * quote_status_t + (** value of term is safe to pass as an argument to system(.), or is + safe to pass as a format argument with the given quotation status + if is_fmt_string is true. *) + | XXValidMem of bterm_t (** memory region pointed to be by term has not been freed *) + | XXDisjunction of xxpredicate_t list | XXConditional of xxpredicate_t * xxpredicate_t @@ -2598,6 +2609,8 @@ type xpo_predicate_t = | XPOSetsErrno | XPOStartsThread of xpr_t * xpr_t list | XPOTainted of xpr_t + | XPOTrustedString of xpr_t + | XPOTrustedOsCmdString of xpr_t * bool * quote_status_t | XPOValidMem of xpr_t | XPODisjunction of xpo_predicate_t list | XPOConditional of xpo_predicate_t * xpo_predicate_t diff --git a/CodeHawk/CHB/bchlib/bCHPrecondition.ml b/CodeHawk/CHB/bchlib/bCHPrecondition.ml index 489eecc3f..8a285d411 100644 --- a/CodeHawk/CHB/bchlib/bCHPrecondition.ml +++ b/CodeHawk/CHB/bchlib/bCHPrecondition.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. 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 @@ -47,6 +47,8 @@ open BCHExternalPredicate open BCHLibTypes open BCHTypeDefinitions +module TR = CHTraceResult + let raise_xml_error (node:xml_element_int) (msg:pretty_t) = let error_msg = @@ -223,7 +225,25 @@ let read_xml_precondition_xxpredicate let dest = gt (arg 1) in [XXBlockWrite (gty (arg 0), dest, gt (arg 2)); XXNotNull dest] | "deref-write-null" -> - [XXBlockWrite (gty (arg 0), gt (arg 1), gt (arg 2))] + [XXBlockWrite (gty (arg 0), gt (arg 1), gt (arg 2))] + | "trusted-os-cmd-string" -> + let s = gt (arg 0) in + let fmtstring = + (pNode#hasNamedAttribute "fmtstring") + && (pNode#getAttribute "fmtstring") = "true" in + if pNode#hasNamedAttribute "quotes" then + let a = pNode#getAttribute "quotes" in + TR.tfold + ~ok:(fun q -> [XXTrustedOsCmdString(s, fmtstring, q)]) + ~error:(fun e -> + raise_xml_error + node + (LBLOCK [ + STR "Problem in parsing trusted-os-cmd-string: "; + STR (String.concat ", " e)])) + (string_to_quote_status a) + else + [XXTrustedOsCmdString(s, fmtstring, NO_QUOTES)] | s -> raise_xml_error node diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index ca1415508..9b56c2e06 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -40,6 +40,14 @@ let calling_convention_mfts: calling_convention_t mfts_int = mk_mfts "calling_convention_t" [(StdCall, "s"); (CDecl, "c")] +let quote_status_mfts: quote_status_t mfts_int = + mk_mfts + "quote_status_t" + [(NO_QUOTES, "n"); + (SINGLE_QUOTES, "s"); + (DOUBLE_QUOTES, "d")] + + let relational_op_mfts: relational_op_t mfts_int = mk_mfts "relational_op_t" @@ -443,6 +451,8 @@ object | XXSetsErrno -> "errno" | XXStartsThread _ -> "st" | XXTainted _ -> "t" + | XXTrustedString _ -> "ts" + | XXTrustedOsCmdString _ -> "tc" | XXValidMem _ -> "v" | XXDisjunction _ -> "dis" | XXConditional _ -> "con" @@ -451,7 +461,7 @@ object "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; - "pos"; "sa"; "st"; "t"; "v"; "x" + "pos"; "sa"; "st"; "t"; "tc"; "ts"; "v"; "x" ] end @@ -496,6 +506,8 @@ object | XPOSetsErrno -> "errno" | XPOStartsThread _ -> "st" | XPOTainted _ -> "t" + | XPOTrustedString _ -> "ts" + | XPOTrustedOsCmdString _ -> "tc" | XPOValidMem _ -> "v" | XPODisjunction _ -> "dis" | XPOConditional _ -> "con" @@ -504,7 +516,7 @@ object "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; - "pos"; "sa"; "st"; "t"; "v"; "x" + "pos"; "sa"; "st"; "t"; "tc"; "ts"; "v"; "x" ] end diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli index a98e54b24..925bba104 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli @@ -37,6 +37,7 @@ val calling_convention_mfts: calling_convention_t mfts_int val arithmetic_op_mfts: arithmetic_op_t mfts_int val g_arithmetic_op_mfts: g_arithmetic_op mfts_int val relational_op_mfts: relational_op_t mfts_int +val quote_status_mfts: quote_status_t mfts_int val arg_io_mfts: arg_io_t mfts_int val formatstring_type_mfts: formatstring_type_t mfts_int diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index 4fd53751e..1ee0ea202 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -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 @@ -99,6 +99,9 @@ object (self) | XPOSetsErrno -> (tags, []) | XPOStartsThread (x, xl) -> (tags, (ix x) :: (List.map ix xl)) | XPOTainted x -> (tags, [ix x]) + | XPOTrustedString x -> (tags, [ix x]) + | XPOTrustedOsCmdString (x, isfmtstring, q) -> + (tags @ [quote_status_mfts#ts q], [ix x; if isfmtstring then 1 else 0]) | XPOValidMem x -> (tags, [ix x]) | XPODisjunction pl -> (tags, List.map self#index_xpo_predicate pl) | XPOConditional (p1, p2) -> diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index a8a3a3a5e..e00d90bee 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -92,6 +92,9 @@ let rec xxp_to_xpo_predicate | XXSetsErrno -> XPOSetsErrno | XXStartsThread (t1, t2) -> XPOStartsThread (btx t1, List.map btx t2) | XXTainted t -> XPOTainted (btx t) + | XXTrustedString t -> XPOTrustedString (btx t) + | XXTrustedOsCmdString (t, isfmtstring, quotes) -> + XPOTrustedOsCmdString (btx t, isfmtstring, quotes) | XXValidMem t -> XPOValidMem (btx t) | XXDisjunction xl -> XPODisjunction (List.map (xxp_to_xpo_predicate termev loc) xl) @@ -169,6 +172,16 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = | XPOSetsErrno -> STR "sets errno" | XPOStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XPOTainted t -> default "tainted" [t] + | XPOTrustedString t -> default "trusted" [t] + | XPOTrustedOsCmdString (t, isfmtstring, quotes) -> + LBLOCK [ + STR "trusted-os-cmd-string("; + x2p t; + STR ", "; + STR (if isfmtstring then "true" else "false"); + STR ", "; + STR (quote_status_to_string quotes); + STR ")"] | XPOValidMem t -> default "valid-mem" [t] | XPODisjunction pl -> pretty_print_list pl xpo_predicate_to_pretty "[" " || " "]" diff --git a/CodeHawk/CHB/bchsummaries/so_functions/system.xml b/CodeHawk/CHB/bchsummaries/so_functions/system.xml index bfbbfdd3a..44dbe7522 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/system.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/system.xml @@ -32,7 +32,16 @@ - + + 
+        
+          
+            
+            command
+          
+        
+
+ From eec65833f9dec56781c5c922b393b61691f80997 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 6 May 2026 11:44:18 -0700 Subject: [PATCH 02/15] CHB: proof obligation discharge of TrustedOsCmdString with constant strings --- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 7 +++++- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 13 ++++++++-- .../CHB/bchlibarm32/bCHARMAnalysisResults.ml | 3 ++- .../CHB/bchlibarm32/bCHARMDisassemblyUtils.ml | 17 ++++++++++++- .../bchlibarm32/bCHARMDisassemblyUtils.mli | 24 +++++++++++++++---- 5 files changed, 54 insertions(+), 10 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index b9cff4c11..a72f3ca14 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1711,11 +1711,16 @@ object (self) method proofobligations = proofobligations - method discharge_proofobligations = + method discharge_proofobligations + ?(get_elf_string_reference=(fun _ -> None)) () = let openpos = self#proofobligations#open_proofobligations in List.iter (fun po -> let newstatus = match po#xpo with + | XPOTrustedOsCmdString (x, false, _) -> + (match get_elf_string_reference x with + | Some s -> Discharged ("constant string: " ^ s) + | _ -> Open) | XPOBuffer ( _ty, XOp (XMinus, [XVar v; XConst (IntConst off)]), diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 3236927fb..7e724e9c9 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -5719,8 +5719,17 @@ object method proofobligations: proofobligations_int (** Attempts to discharge some open proof obligations and if successful - updates their status.*) - method discharge_proofobligations: unit + updates their status. The optional argument [get_elf_string_reference] + allows this function to check if an argument is a constant string in + the binary. A constant string in the binary is considered trusted. + + The reason that it is passed in as an argument is that the elf library + code is not directly accessible from this point. It means that this + function should preferably be called from a location that has access + to the elf library. +*) + method discharge_proofobligations: + ?get_elf_string_reference:(xpr_t -> string option) -> unit -> unit (** {1 Function invariants} *) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 07099e5db..813d19243 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -43,6 +43,7 @@ open BCHTypeConstraintStore (* bchlibarm32 *) open BCHARMAssemblyFunctions open BCHARMDictionary +open BCHARMDisassemblyUtils open BCHARMLoopStructure open BCHARMTypes open BCHFnARMDictionary @@ -225,7 +226,7 @@ object (self) mmap#write_xml_references faddr vard grNode; (* self#write_xml_btypes bNode; *) id#write_xml dNode; - finfo#discharge_proofobligations; + finfo#discharge_proofobligations ~get_elf_string_reference (); finfo#proofobligations#write_xml poNode; finfo#xpod#write_xml xpodNode; append [cNode; dNode; iiNode; jjNode; sfNode; grNode; xpodNode; poNode] diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.ml b/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.ml index 889c73ddb..da83079ad 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.ml @@ -167,7 +167,22 @@ let has_inverse_cc (cc: arm_opcode_cc_t): bool = Option.is_some (get_inverse_cc cc) -let get_string_reference (floc:floc_int) (xpr:xpr_t) = +let get_elf_string_reference (xpr: xpr_t): string option = + match xpr with + | XConst (IntConst num) -> + TR.tfold + ~ok:elf_header#get_string_at_address + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ + ["xpr: " ^ num#toString; String.concat ", " e]; + None + end) + (numerical_to_doubleword num) + | _ -> None + + +let get_string_reference (floc:floc_int) (xpr:xpr_t): string option = try match xpr with | XConst (IntConst num) -> diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.mli b/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.mli index 2fff60afe..c815221b7 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.mli @@ -1,10 +1,10 @@ (* ============================================================================= - CodeHawk Binary Analyzer + CodeHawk Binary Analyzer Author: Henny Sipma ------------------------------------------------------------------------------ The MIT License (MIT) - - 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 @@ -12,10 +12,10 @@ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -43,4 +43,18 @@ val get_inverse_cc: arm_opcode_cc_t -> arm_opcode_cc_t option val has_inverse_cc: arm_opcode_cc_t -> bool +(** [get_string_reference floc x] returns a string if [x] is a numerical constant + that is the virtual address of a constant string in an ELF read-only section. + In addition it adds an entry to the string table kept by each [floc] that + this string is referenced by the instruction at the [floc] location. *) val get_string_reference: floc_int -> xpr_t -> string option + +(** [get_elf_string_reference x] returns a string if [x] is a numerical constant + that is the virtual address of a constant string in an ELF read-only section. + + This function is a simpler version of [get_string_reference] above in that + it does not need a [floc] and thus can be used in a wider context, e.g., to + discharge proof obligations. It assumes that the value to which it is applied + has been strengthened with invariants and simplified before application, as + this function has no access to invariants.*) +val get_elf_string_reference: xpr_t -> string option From d47e7e994bbf34ecf7ef069c3f8a4d78e3d0c7c6 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 6 May 2026 14:50:02 -0700 Subject: [PATCH 03/15] CHB: delegate format-string po to api --- .../CHB/bchlib/bCHCallSemanticsRecorder.ml | 14 +++++++++++ CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 25 +++++++++++++++++++ 2 files changed, 39 insertions(+) diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index cd4431c34..1b5f26a9c 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml @@ -136,6 +136,15 @@ object (self) else Open | _ -> Open) + | XPOTrustedString x | XPOTrustedOsCmdString (x, false, _) -> + (match x with + | XConst (IntConst n) -> + let dw = numerical_mod_to_doubleword n in + if string_table#has_string dw then + Discharged ("constant string: " ^ (string_table#get_string dw)) + else + Open + | _ -> Open) | XPOOutputFormatString x -> (match x with | XConst (IntConst n) -> @@ -165,6 +174,11 @@ object (self) | _ -> Open) | _ -> Open + (* Relies on the expression externalizer, which, at present, has only been + implemented for mips. + An alternative for delegating proof obligations is in the method + discharge_proofobligations in function_info. + Eventually these two methods should be merged or at least unified.*) method private delegate_precondition (xpo: xpo_predicate_t): po_status_t = match xpo with | XPONotNull x -> diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index a72f3ca14..62a3342b1 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1721,6 +1721,31 @@ object (self) (match get_elf_string_reference x with | Some s -> Discharged ("constant string: " ^ s) | _ -> Open) + | XPOOutputFormatString (XVar v) + when self#env#is_initial_register_value v -> + TR.tfold + ~ok:(fun reg -> + let _ = + self#update_summary + (self#get_summary#add_register_parameter_location + reg t_charptr 4) in + let ftspar = self#get_summary#get_parameter_for_register reg in + let dst = ArgValue ftspar in + let xpred = XXOutputFormatString dst in + let updatedsummary = self#get_summary#add_precondition xpred in + let _ = self#update_summary updatedsummary in + Delegated xpred) + ~error:(fun e -> + begin + log_error_result + ~tag:"delegate_proofobligation" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + String.concat ", " e]; + Open + end) + (self#env#get_initial_register_value_register v) + | XPOBuffer ( _ty, XOp (XMinus, [XVar v; XConst (IntConst off)]), From ba7747f93924b9925a750d692ff209910bd99392 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 6 May 2026 16:29:52 -0700 Subject: [PATCH 04/15] CHB: add format string to function capabilities --- CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml | 14 ++++++++++++++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 1 + CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 3 ++- CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml | 4 +++- CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml | 8 +++++++- 5 files changed, 27 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index 25bb060ff..0eb513ae3 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -361,6 +361,20 @@ let get_type_arg_mode && (Option.get param.apar_index) = argindex -> Some (ArgDerefWrite None) | _ -> None) None predicates in + let mode = + if Option.is_none mode then + List.fold_left (fun acc p -> + match acc with + | Some _ -> acc + | _ -> + match p with + | XXOutputFormatString (ArgValue param) + when Option.is_some param.apar_index + && (Option.get param.apar_index) = argindex -> + Some ArgOutputFormatString + | _ -> None) None predicates + else + mode in let mode = if Option.is_none mode then List.fold_left (fun acc p -> diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 7e724e9c9..0573a4c23 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -3260,6 +3260,7 @@ type type_arg_mode_t = | ArgDeallocate | ArgFunctionPointer | ArgScalarValue + | ArgOutputFormatString type type_operation_kind_t = diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 9b56c2e06..1a4248bda 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -543,8 +543,9 @@ object | ArgDeallocate -> "d" | ArgFunctionPointer -> "fp" | ArgScalarValue -> "s" + | ArgOutputFormatString -> "fmt" - method !tags = ["d"; "fp"; "r"; "rw"; "s"; "w"] + method !tags = ["d"; "fmt"; "fp"; "r"; "rw"; "s"; "w"] end diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml index 338c27fb7..f4ee9ce4c 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml @@ -93,7 +93,8 @@ object (self) | ArgDerefWrite optsize -> (tags, [index_opt optsize]) | ArgDeallocate | ArgFunctionPointer - | ArgScalarValue -> (tags, []) in + | ArgScalarValue + | ArgOutputFormatString -> (tags, []) in type_arg_mode_table#add key method get_type_arg_mode (index: int): type_arg_mode_t = @@ -104,6 +105,7 @@ object (self) let getsize () = if (a 0) = (-1) then None else Some (a 0) in match (t 0) with | "d" -> ArgDeallocate + | "fmt" -> ArgOutputFormatString | "fp" -> ArgFunctionPointer | "r" -> ArgDerefRead (getsize ()) | "rw" -> ArgDerefReadWrite (getsize ()) diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index cb10a15cf..cbfb44a37 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -71,6 +71,9 @@ let _type_arg_mode_compare (m1: type_arg_mode_t) (m2: type_arg_mode_t): int = | (ArgFunctionPointer, _) -> -1 | (_, ArgFunctionPointer) -> 1 | (ArgScalarValue, ArgScalarValue) -> 0 + | (ArgScalarValue, _) -> -1 + | (_, ArgScalarValue) -> 1 + | (ArgOutputFormatString, ArgOutputFormatString) -> 0 let type_cap_label_compare (c1: type_cap_label_t) (c2: type_cap_label_t) = @@ -145,6 +148,7 @@ let type_arg_mode_to_string (m: type_arg_mode_t) = | ArgDeallocate -> "d" | ArgFunctionPointer -> "fp" | ArgScalarValue -> "sv" + | ArgOutputFormatString -> "ofs" let type_operation_kind_to_string (op: type_operation_kind_t) = @@ -478,7 +482,9 @@ let convert_function_capabilities_to_attributes | ArgDerefWrite size -> mkcons "write_only" size | ArgDeallocate -> ACons ("deallocate", []) | ArgFunctionPointer -> ACons ("fp", []) - | ArgScalarValue -> ACons ("sv", []) in + | ArgScalarValue -> ACons ("sv", []) + | ArgOutputFormatString -> ACons ("printf_format_string", []) + in let result = new CHUtils.IntCollections.set_t in let _ = List.iter (fun cap -> From 8ea4083d9150d77f1ee3e6c467ed4bc200d745cd Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 6 May 2026 19:37:28 -0700 Subject: [PATCH 05/15] CHB: convert preconditions to attributes --- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 19 +++++++++++++++++++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 2 ++ .../CHB/bchlibarm32/bCHARMAnalysisResults.ml | 14 ++++++++------ 3 files changed, 29 insertions(+), 6 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 62a3342b1..bd52fb8f1 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1823,6 +1823,25 @@ object (self) po#update_status newstatus end) openpos + method convert_preconditions_to_attributes = + let delegatedpos = self#proofobligations#delegated_proofobligations in + List.fold_left (fun acc po -> + match po#status with + | Delegated xpred -> + (match xpred with + | XXOutputFormatString (ArgValue par) -> + let argindex = par.apar_index in + (match argindex with + | Some argindex -> + let attr = + Attr ("chk_pre", + [ACons ("output_format_string", []); + AInt argindex]) in + attr :: acc + | _ -> acc) + | _ -> acc) + | _ -> acc) [] delegatedpos + method set_instruction_bytes (ia:ctxt_iaddress_t) (b:string) = H.add instrbytes ia b diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 0573a4c23..5ad0bcbb4 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -5732,6 +5732,8 @@ object method discharge_proofobligations: ?get_elf_string_reference:(xpr_t -> string option) -> unit -> unit + method convert_preconditions_to_attributes: b_attributes_t + (** {1 Function invariants} *) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 813d19243..748c8af21 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -311,6 +311,12 @@ object (self) typeconstraints#record_type_constraints; (ignore (typeconstraintstore#get_function_type_constraints faddr)); (ignore (typeconstraintstore#evaluate_function_type faddr)); + fndata#set_reglhs_types (typeconstraintstore#resolve_reglhs_types faddr); + fndata#set_stack_offset_types + (typeconstraintstore#resolve_local_stack_lhs_types faddr); + fnadata#write_xml_register_types node fndata#get_reglhs_types; + fnadata#write_xml_stack_types node fndata#get_stack_offset_types; + fnadata#write_xml node; (if mksignature then let fname = BCHFunctionData.get_default_functionsummary_name_dw @@ -321,13 +327,9 @@ object (self) fname resolvents in let (regtypes, _) = resolvents in let attrs = List.concat (List.map (fun (_, _, a) -> a) regtypes) in + let attrs = (finfo#convert_preconditions_to_attributes) @ attrs in BCHBCFiles.bcfiles#add_fundef ~attrs fname ftype); - fndata#set_reglhs_types (typeconstraintstore#resolve_reglhs_types faddr); - fndata#set_stack_offset_types - (typeconstraintstore#resolve_local_stack_lhs_types faddr); - fnadata#write_xml_register_types node fndata#get_reglhs_types; - fnadata#write_xml_stack_types node fndata#get_stack_offset_types; - fnadata#write_xml node; + node#setAttribute "a" faddr; save_app_function_results_file faddr node; save_vars faddr vard From 77c4ff4f0d6364f33dbc23c087a290a290897695 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 09:51:13 -0700 Subject: [PATCH 06/15] CHB: consolidate proof obligation discharge --- CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 1044 +++++++++++++++++ .../CHB/bchlib/bCHFunctionPODischarge.mli | 125 ++ 2 files changed, 1169 insertions(+) create mode 100644 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml create mode 100644 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.mli diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml new file mode 100644 index 000000000..49258723e --- /dev/null +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -0,0 +1,1044 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage + +(* chutil *) +open CHLogger + +(* xprlib *) +open XprTypes +open Xsimplify + +(* bchlib *) +open BCHBCTypes +open BCHExternalPredicate +open BCHGlobalState +open BCHLibTypes +open BCHXPOPredicate + +module TR = CHTraceResult + + +let p2s = CHPrettyUtil.pretty_to_string +let x2p = XprToPretty.xpr_formatter#pr_expr +let x2s x = p2s (x2p x) + +(* ========================================================================= + General utilities + ========================================================================= *) + +(** [get_constant_string x] returns a string if the expression is a constant + address that is present in the string table. + + Note: during analysis constant strings present in the binary that are + referenced in instructions are collected in BCHString.string_table. Care + should be taken that the proof obligation discharge is performed after + that process is completed. *) +let get_constant_string (loc: location_int) (x: xpr_t): string option = + match x with + | XConst (IntConst n) -> + let dw = BCHDoubleword.numerical_mod_to_doubleword n in + if BCHStrings.string_table#has_string dw then + Some (BCHStrings.string_table#get_string dw) + else + begin + log_diagnostics_result + ~tag:"get_constant_string:string not found" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["address: " ^ n#toString]; + None + end + | _ -> None + + +let call_writes_to_buffer (floc: floc_int) (buffer: xpr_t): bool = + if not floc#has_call_target then + false + else + let ctinfo = floc#get_call_target in + match floc#get_bterm_evaluator with + | None -> false + | Some btermev -> + List.exists (fun se -> + match se with + | XXBlockWrite (_, bterm, _) -> + (match btermev#bterm_xpr bterm with + | Some xse -> + let xse' = floc#inv#rewrite_expr xse in + (* Check address equality by simplifying the difference *) + (match simplify_xpr (XOp (XMinus, [xse'; buffer])) with + | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero + | _ -> false) + | _ -> false) + | _ -> false) + ctinfo#get_sideeffects + + +(* ========================================================================= + Reaching-definition utilities + ========================================================================= *) + +(** [buffer_writer_callsite finfo cia xpr] searches for the call site + that last wrote to the memory buffer whose address is [xpr] at + instruction [cia]. + + For a stack buffer (i.e., [xpr] is an expression relative to the + initial stack pointer), the memory variable for the corresponding stack + slot is obtained from the function's stackframe, and its reaching + definitions are queried. + + On success, returns the call-site location.*) +let buffer_writer_callsite + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): location_int option = + match finfo#stackframe#xpr_containing_stackslot xpr with + | Some slot -> + let memvar = finfo#env#mk_stackslot_variable slot NoOffset in + let symvar = finfo#env#mk_symbolic_variable memvar in + let varinv = finfo#ivarinv loc#ci 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__ + ["xpr: " ^ (x2s xpr); + "memvar: " ^ (p2s memvar#toPretty)]; + None + end + | _ -> + begin + log_diagnostics_result + ~tag:"buffer_writer_callsite:multiple defining locations" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); + "memvar: " ^ (p2s memvar#toPretty); + "defsites: " + ^ (String.concat ", " (List.map (fun l -> p2s l#toPretty) defsites))]; + None + end) + | None -> + begin + log_diagnostics_result + ~tag:"buffer_writer_callsite:not a stack buffer" + ~msg:(p2s loc#toPretty) __FILE__ __LINE__["xpr: " ^ (x2s xpr)]; + None + end + +(* ========================================================================= + Discharge strategies per PO type + ========================================================================= *) + +(** Discharge strategies for a single open proof obligation. + + Each strategy returns a [po_status_t]: + - stmt: [Discharged msg]: closed, evidence in [msg] + - delegate_local: [DelegatedLocal (cia, xpo)]: transferred to another + instruction or another argument in the same instruction + - delegate_api: [Delegated xxp]: transferred to the current function's + own preconditions + - delegate_global: [DelegatedGlobal (dw, xxp)]: registered in the global + state at address [dw] + - [Open]: unable to discharge + *) + +(* ------------------------------------------------------------------------- + XPOTrustedOsCmdString + ------------------------------------------------------------------------- *) + +let trusted_os_cmd_string_constant_string_stmt + (loc: location_int) (x: xpr_t): po_status_t = + match get_constant_string loc x with + | Some s -> Discharged ("constant string: " ^ s) + | _ -> Open + + +let trusted_os_cmd_string_delegate_local_instr + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + let btermev = floc#get_bterm_evaluator in + if not floc#has_call_target then + Open + else if Option.is_none btermev then + Open + else + let btermev = Option.get btermev in + let ctinfo = floc#get_call_target in + if call_writes_to_buffer floc xpr then + (* the string value is written by the instruction itself (like in, + e.g., sprintf) so the proof obligation must be transferred to + the source of that output.*) + List.fold_left (fun acc se -> + match acc with + | Open -> + (match se with + | XXWritesStringFromFmtString (dst, src, fmtkind, optlen) -> + (match (btermev#bterm_xpr dst, btermev#bterm_xpr src) with + | (Some dstptr, Some srcptr) -> + let dstptr' = floc#inv#rewrite_expr dstptr in + let iswrite = + (match simplify_xpr (XOp (XMinus, [dstptr'; xpr])) with + | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero + | _ -> false) in + if iswrite then + let xlen = + match optlen with + | Some len -> btermev#bterm_xpr len + | _ -> None in + let new_xpo = + XPOTrustedOsCmdFmtString (srcptr, fmtkind, xlen) in + let _ = + finfo#proofobligations#add_proofobligation + floc#l#ci new_xpo Open in + DelegatedLocal (loc#ci, new_xpo) + else + Open + | _ -> Open) + | _ -> Open) + | _ -> acc) Open ctinfo#get_sideeffects + else + Open + + +let trusted_os_cmd_string_delegate_local + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + match buffer_writer_callsite finfo loc xpr with + | None -> Open + | Some defloc -> + (* Check that the call at defloc has a BlockWrite side effect on the + same buffer. Use the invariant at defloc to evaluate expressions. *) + let deffloc = BCHFloc.get_finfo_floc finfo defloc in + if call_writes_to_buffer deffloc xpr then + begin + (* Create a new open PO at the writer call site *) + let new_xpo = XPOTrustedOsCmdString xpr in + finfo#proofobligations#add_proofobligation defloc#ci new_xpo Open; + (* The original PO is delegated to the xxpredicate form *) + DelegatedLocal (defloc#ci, new_xpo) + end + else + Open + + +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_delegate_local_instr finfo loc x + | _ -> status in + let status = + match status with + | Open -> trusted_os_cmd_string_delegate_local finfo loc x + | _ -> status in + status + + +(* ------------------------------------------------------------------------- + XPOTrustedOsCmdFmtString + ------------------------------------------------------------------------- *) + +(* A format string is considered to construct a safe string to pass to a call + to [system] if it does not contain any %s format specifiers.*) +let trusted_os_cmd_fmt_string_no_string_conversions + (loc: location_int) (x: xpr_t): po_status_t = + match get_constant_string loc x with + | Some s -> + let formatspec = CHFormatStringParser.parse_formatstring s false in + if List.exists (fun a -> + match a#get_conversion with + | CHFormatStringParser.StringConverter -> true + | _ -> false) formatspec#get_arguments then + Open + else + Discharged ("constant format string without string converters: " ^ s) + | _ -> + Open + + +let trusted_os_cmd_fmt_string_va_list_delegate + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t) + (optlen: xpr_t option): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + let xpxt_opt = floc#get_expression_externalizer in + match xpxt_opt with + | Some xpxt -> + let xoptlen = + match optlen with + | Some len -> xpxt#xpr_to_bterm BCHBCTypeUtil.t_int len + | _ -> None in + (match xpxt#xpr_to_bterm BCHBCTypeUtil.t_charptr x with + | Some xfmt -> + let xpred = XXTrustedOsCmdFmtString (xfmt, FMT_ARGS, xoptlen) in + let updatedsummary = finfo#get_summary#add_precondition xpred in + let _ = finfo#update_summary updatedsummary in + Delegated (xpred) + | _ -> Open) + | _ -> Open + + +let discharge_trusted_os_cmd_fmt_string + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t) + (kind: format_args_kind_t) + (optlen: xpr_t option): po_status_t = + let status = trusted_os_cmd_fmt_string_no_string_conversions loc x in + let status = + match status with + | Open -> + (match kind with + | VA_LIST -> + trusted_os_cmd_fmt_string_va_list_delegate finfo loc x optlen + | _ -> Open) + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discharge_trusted_os_cmd_fmt_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x)]; + status + end + | _ -> + status + + +(* ------------------------------------------------------------------------- + XPOOutputFormatString + ------------------------------------------------------------------------- *) + +(** Direct discharge: format string is a constant string.*) +let output_format_string_constant_string_stmt + (loc: location_int) (x: xpr_t): po_status_t = + match get_constant_string loc x with + | Some s -> Discharged ("constant string: " ^ s) + | _ -> Open + + +(* Delegate to a precondition on a the calling function.*) +let output_format_string_delegate + (finfo: function_info_int) + (loc: location_int) + (x: xpr_t): po_status_t = + match x with + | XVar v when finfo#env#is_initial_register_value v -> + TR.tfold + ~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) + ~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#env#get_initial_register_value_register v) + | _ -> + Open + + +let discharge_output_format_string + (finfo: function_info_int) (loc: location_int) (xpr: xpr_t): po_status_t = + let status = output_format_string_constant_string_stmt loc xpr in + let status = + match status with + | Open -> output_format_string_delegate finfo loc xpr + | _ -> status in + status + + +(* ------------------------------------------------------------------------- + XPOBuffer / XPOBlockWrite (stack size check) + ------------------------------------------------------------------------- *) + +(** Discharge a buffer or block-write PO by checking the stack frame: if the + required size fits within the available slot, discharge; if it exceeds the + slot, the PO is violated. *) +let discharge_stack_buffer + (finfo: function_info_int) + (loc: location_int) + (ty: btype_t) + (v: variable_t) + (off: CHNumerical.numerical_t) + (size: CHNumerical.numerical_t) + (tag: string): po_status_t = + let buffer = finfo#stackframe#get_max_slot_size off#neg#toInt in + match buffer with + | Some slotsize -> + if size#toInt <= slotsize then + Discharged ( + "buffer size " ^ size#toString + ^ " fits in available space of " + ^ (string_of_int slotsize) ^ " bytes") + else + Violated ( + "buffer size " + ^ size#toString ^ " is too large; available space is " + ^ (string_of_int slotsize) ^ " bytes") + | None -> + let _ = + log_diagnostics_result + ~tag:("discharge_stack_buffer:" ^ tag ^ ":open") + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["unable to determine buffer size at offset " ^ off#toString; + "v: " ^ (p2s v#toPretty); + "ty: " ^ (BCHBCTypePretty.btype_to_string ty)] in + Open + + +let blockwrite_buffer_discharge_stack_buffer + (finfo: function_info_int) + (loc: location_int) + (ty: BCHBCTypes.btype_t) + (xpr: xpr_t) + (bwlen: xpr_t): po_status_t = + match (xpr, bwlen) with + | (XOp (XMinus, [XVar v; XConst (IntConst off)]), XConst (IntConst size)) + when finfo#env#is_initial_stackpointer_value v -> + discharge_stack_buffer finfo loc ty v off size "blockwrite" + | _ -> + begin + log_diagnostics_result + ~tag:"blockwrite_buffer_discharge_stack_buffer:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + Open + end + +(* ------------------------------------------------------------------------- + XPOBlockWrite + ------------------------------------------------------------------------- *) + +(** Discharge [XPOBlockWrite(ty, XVar v, bwlen)] when [v] is an initial + register value: promote to a precondition / side effect of the current + function (interprocedural delegation). *) +let blockwrite_delegate + (finfo: function_info_int) + (loc: location_int) + (ty: BCHBCTypes.btype_t) + (xpr: xpr_t) + (bwlen: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + match floc#get_expression_externalizer with + | None -> + begin + log_diagnostics_result + ~tag:"blockwrite_delegate:no expression_externalizer" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + Open + end + | Some xprxt -> + (match xprxt#xpr_to_bterm ty xpr with + | Some (NumConstant n) when n#gt CHNumerical.numerical_zero -> + let dw = BCHDoubleword.numerical_mod_to_doubleword n in + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with + | Some (NumConstant ns) -> + let xxp = XXBlockWrite (ty, NumConstant n, NumConstant ns) in + begin + global_system_state#add_precondition dw loc xxp; + log_diagnostics_result + ~tag:"blockwrite_delegate:delegate_global" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; + "xxp: " ^ (p2s (xxpredicate_to_pretty xxp))]; + DelegatedGlobal (dw, xxp) + end + | _ -> + begin + log_diagnostics_result + ~tag:"blockwrite_delegate:delegate_global:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; "bwlen: " ^ (x2s bwlen)]; + Open + end) + | Some dst -> + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with + | Some lenterm -> + let xpred = XXBlockWrite (ty, dst, lenterm) in + begin + finfo#add_precondition xpred; + finfo#add_sideeffect xpred; + Delegated xpred + end + | _ -> + begin + log_diagnostics_result + ~tag:"blockwrite_delegate:dest:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dst: " ^ (BCHBTerm.bterm_to_string dst); "bwlen: " ^ (x2s bwlen)]; + Open + end) + | _ -> + begin + log_diagnostics_result + ~tag:"blockwrite_delegate:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + Open + end) + + +let discharge_blockwrite + (finfo: function_info_int) + (loc: location_int) + (ty: btype_t) + (xpr: xpr_t) + (bwlen: xpr_t): po_status_t = + let status = + blockwrite_buffer_discharge_stack_buffer finfo loc ty xpr bwlen in + let status = + match status with + | Open -> blockwrite_delegate finfo loc ty xpr bwlen + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discharge_blockwrite:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + status + end + | _ -> + status + +(* ------------------------------------------------------------------------- + XPOBuffer + ------------------------------------------------------------------------- *) + +let buffer_delegate + (finfo: function_info_int) + (loc: location_int) + (ty: BCHBCTypes.btype_t) + (xpr: xpr_t) + (bwlen: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + match floc#get_expression_externalizer with + | None -> + begin + log_diagnostics_result + ~tag:"buffer_delegate:no expression_externalizer" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + Open + end + | Some xprxt -> + (match xprxt#xpr_to_bterm ty xpr with + | Some (NumConstant n) when n#gt CHNumerical.numerical_zero -> + let dw = BCHDoubleword.numerical_mod_to_doubleword n in + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with + | Some (NumConstant ns) -> + let xxp = XXBuffer (ty, NumConstant n, NumConstant ns) in + begin + global_system_state#add_precondition dw loc xxp; + log_diagnostics_result + ~tag:"buffer_delegate:delegate_global" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; + "xxp: " ^ (p2s (xxpredicate_to_pretty xxp))]; + DelegatedGlobal (dw, xxp) + end + | _ -> + begin + log_diagnostics_result + ~tag:"buffer_delegate:delegate_global:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; "bwlen: " ^ (x2s bwlen)]; + Open + end) + | Some dst -> + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with + | Some lenterm -> + let xpred = XXBuffer (ty, dst, lenterm) in + let _ = finfo#add_precondition xpred in + Delegated xpred + | _ -> + begin + log_diagnostics_result + ~tag:"buffer_delegate:dest:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dst: " ^ (BCHBTerm.bterm_to_string dst); "bwlen: " ^ (x2s bwlen)]; + Open + end) + | _ -> + begin + log_diagnostics_result + ~tag:"buffer_delegate:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + Open + end) + + +let discharge_buffer + (finfo: function_info_int) + (loc: location_int) + (ty: btype_t) + (xpr: xpr_t) + (bwlen: xpr_t): po_status_t = + let status = + blockwrite_buffer_discharge_stack_buffer finfo loc ty xpr bwlen in + let status = + match status with + | Open -> buffer_delegate finfo loc ty xpr bwlen + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discharge_buffer:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "bwlen: " ^ (x2s bwlen)]; + status + end + | _ -> + status + +(* ------------------------------------------------------------------------- + XPONotNull + ------------------------------------------------------------------------- *) + +let not_null_constant_address (loc: location_int) (xpr: xpr_t): po_status_t = + match xpr with + | XConst (IntConst n) -> + let _ = + log_diagnostics_result + ~tag:"not_null_constant_address" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["address: " ^ n#toString] in + Discharged ("constant address: " ^ n#toString) + | _ -> + Open + + +let not_null_stack_address + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + match xpr with + | XOp (XMinus, [XVar v; _]) when finfo#env#is_initial_stackpointer_value v -> + let _ = + log_diagnostics_result + ~tag:"not_null_stack_address" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["address: " ^ (x2s xpr)] in + Discharged ("stack address: " ^ (x2s xpr)) + | _ -> + Open + + +let not_null_delegate + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + match floc#get_expression_externalizer with + | None -> + begin + log_diagnostics_result + ~tag:"not_null_delegate:no expression_externalizer" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr)]; + Open + end + | Some xprxt -> + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_voidptr xpr with + | Some (NumConstant n) when n#gt CHNumerical.numerical_zero -> + Discharged ("constant address: " ^ n#toString) + | Some t -> + let xxp = XXNotNull t in + let _ = finfo#add_precondition xxp in + Delegated xxp + | _ -> + begin + log_diagnostics_result + ~tag:"not_null_delegate:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr)]; + Open + end) + + +let discharge_not_null + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + let status = not_null_constant_address loc xpr in + let status = + match status with + | Open -> not_null_stack_address finfo loc xpr + | _ -> status in + let status = + match status with + | Open -> not_null_delegate finfo loc xpr + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discharge_not_null:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr)]; + status + end + | _ -> + status + +(* ------------------------------------------------------------------------- + XPONullTerminated + ------------------------------------------------------------------------- *) + +let null_terminated_constant_string + (loc: location_int) (xpr: xpr_t): po_status_t = + match get_constant_string loc xpr with + | Some s -> + begin + log_diagnostics_result + ~tag:"null_terminated_constant_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["string: " ^ s]; + Discharged ("constant string: " ^ s) + end + | _ -> + Open + + +let null_terminated_delegate + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + match floc#get_expression_externalizer with + | None -> + begin + log_diagnostics_result + ~tag:"null_termiatned_delegate:no expression_externalizer" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr)]; + Open + end + | Some xprxt -> + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_voidptr xpr with + | Some (NumConstant n) when n#gt CHNumerical.numerical_zero -> + Discharged ("constant address: " ^ n#toString) + | Some t -> + let xxp = XXNullTerminated t in + let _ = finfo#add_precondition xxp in + Delegated xxp + | _ -> + begin + log_diagnostics_result + ~tag:"null_terminated_delegate:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr)]; + Open + end) + + +let discharge_null_terminated + (finfo: function_info_int) + (loc: location_int) + (xpr: xpr_t): po_status_t = + let status = null_terminated_constant_string loc xpr in + let status = + match status with + | Open -> null_terminated_delegate finfo loc xpr + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discharge_null_terminated:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr)]; + status + end + | _ -> + status + +(* ------------------------------------------------------------------------- + XPOInitializedRange + ------------------------------------------------------------------------- *) + +let initialized_range_constant_string + (loc: location_int) (xpr: xpr_t): po_status_t = + match get_constant_string loc xpr with + | Some s -> + begin + log_diagnostics_result + ~tag:"initialized_range_constant_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["string: " ^ s]; + Discharged ("constant string: " ^ s) + end + | _ -> + Open + + +let initialized_range_delegate + (finfo: function_info_int) + (loc: location_int) + (ty: BCHBCTypes.btype_t) + (xpr: xpr_t) + (size: xpr_t): po_status_t = + let floc = BCHFloc.get_finfo_floc finfo loc in + match floc#get_expression_externalizer with + | None -> + begin + log_diagnostics_result + ~tag:"initialized_range_delegate:no expression_externalizer" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "size: " ^ (x2s size)]; + Open + end + | Some xprxt -> + (match xprxt#xpr_to_bterm ty xpr with + | Some (NumConstant n) when n#gt CHNumerical.numerical_zero -> + let dw = BCHDoubleword.numerical_mod_to_doubleword n in + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int size with + | Some (NumConstant ns) -> + let xxp = XXInitializedRange (ty, NumConstant n, NumConstant ns) in + begin + global_system_state#add_precondition dw loc xxp; + log_diagnostics_result + ~tag:"buffer_delegate:delegate_global" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; + "xxp: " ^ (p2s (xxpredicate_to_pretty xxp))]; + DelegatedGlobal (dw, xxp) + end + | _ -> + begin + log_diagnostics_result + ~tag:"initialized_range_delegate:delegate_global:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dw: " ^ dw#to_hex_string; "size: " ^ (x2s size)]; + Open + end) + | Some dst -> + (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int size with + | Some lenterm -> + let xpred = XXInitializedRange (ty, dst, lenterm) in + let _ = finfo#add_precondition xpred in + Delegated xpred + | _ -> + begin + log_diagnostics_result + ~tag:"initialized_range_delegate:dest:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["dst: " ^ (BCHBTerm.bterm_to_string dst); "size: " ^ (x2s size)]; + Open + end) + | _ -> + begin + log_diagnostics_result + ~tag:"initialized_range_delegate:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "size: " ^ (x2s size)]; + Open + end) + + +let discharge_initialized_range + (finfo: function_info_int) + (loc: location_int) + (ty: btype_t) + (xpr: xpr_t) + (size: xpr_t): po_status_t = + let status = initialized_range_constant_string loc xpr in + let status = + match status with + | Open -> initialized_range_delegate finfo loc ty xpr size + | _ -> status in + match status with + | Open -> + begin + log_diagnostics_result + ~tag:"discarhge_initialized_range:open" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ ["xpr: " ^ (x2s xpr); "size: " ^ (x2s size)]; + Open + end + | _ -> + status + +(* ========================================================================= + Main dispatch + ========================================================================= *) + +(** Attempt to discharge or delegate a single open proof obligation. + + Returns the new status, or [Open] if unable to discharge. *) +let discharge_one + (finfo: function_info_int) + (po: proofobligation_int): po_status_t = + match po#xpo with + + | XPOTrustedOsCmdString x -> + discharge_trusted_os_cmd_string finfo po#loc x + + | XPOTrustedOsCmdFmtString (x, kind, optlen) -> + discharge_trusted_os_cmd_fmt_string finfo po#loc x kind optlen + + | XPOOutputFormatString x -> + discharge_output_format_string finfo po#loc x + + | XPOBlockWrite (ty, x, bwlen) -> + discharge_blockwrite finfo po#loc ty x bwlen + + | XPOBuffer (ty, x, bwlen) -> + discharge_buffer finfo po#loc ty x bwlen + + | XPONotNull x -> + discharge_not_null finfo po#loc x + + | XPONullTerminated x -> + discharge_null_terminated finfo po#loc x + + | XPOInitializedRange (ty, x, size) -> + discharge_initialized_range finfo po#loc ty x size + + | _ -> Open + + +(* ========================================================================= + Fixpoint iteration + ========================================================================= *) + +(** Run one discharge pass over all currently open proof obligations. + Returns the number of obligations whose status changed. *) +let discharge_pass + (finfo: function_info_int): int = + let openpos = finfo#proofobligations#open_proofobligations in + List.fold_left (fun changed po -> + let newstatus = discharge_one finfo po in + match newstatus with + | Open -> changed + | _ -> + begin + log_diagnostics_result + ~tag:"discharge_pass" + ~msg:(p2s po#loc#toPretty) + __FILE__ __LINE__ + ["xpo: " ^ (p2s (xpo_predicate_to_pretty po#xpo)); + "status: " + ^ (p2s (BCHProofObligations.po_status_to_pretty newstatus))]; + po#update_status newstatus; + changed + 1 + end) + 0 openpos + + +(* ========================================================================= + Entry point + ========================================================================= *) + +(** Discharge all open proof obligations for [finfo], iterating to fixpoint. + + Each pass may close some obligations directly and create new ones via + intra-function delegation (e.g., by adding a [XPOTrustedOsCmdString] at + the [sprintf] call site that wrote the buffer questioned at a [system] + call site). Iteration continues until a pass produces no changes, at + which point the remaining open obligations cannot be decided within the + function. + + [max_passes] is a safety bound on iteration depth (default 8); in + practice the chain system → sprintf → format-arg resolves in at most 3 + passes. *) +let discharge_function_proofobligations + ?(max_passes = 8) + (finfo: function_info_int): unit = + let rec loop n = + if n = 0 then + () + else + let changed = discharge_pass finfo in + if changed > 0 then loop (n - 1) + in + loop max_passes diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.mli b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.mli new file mode 100644 index 000000000..a3421f189 --- /dev/null +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.mli @@ -0,0 +1,125 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + + +(** Post-analysis proof-obligation discharge for a single function. + + This module contains the principal implementation for discharging proof + obligations at the function level. Several passes may be made through the + function if proof obligations are delegated to other instructions within + the code using reaching definitions. + + Three discharge strategies are applied, in order of locality: + + 1. {b Direct discharge (stmt)}: The PO can be closed using information + available with the instruction itself. This may include function + arguments obtained through invariant propagation. + + 2. {b Intra-procedural delegation}: The PO on a call or call argument is + delegated to another instruction or to another argument in the same + call. The PO considered is closed and a new (open) PO is created for + the target of the delegation, to be possibly discharged in the next + pass. + + Intra-instruction delegation is typically enabled by call target side + effects. An example is: the PO [XPOTrustedOsCmdString(cmd)] on the + destination buffer of a (v)s(n)printf call can be transferred to a + PO [XPOTrustedOsCmdFmtString(fmt,.,.)] on the format string. + + Inter-instruction delegation is typically enabled by reaching + definitions rather than invariants. Invariants would already be + available at the instruction itself. Reaching definitions allow + POs to be transferred to, for example, multiple joining branches, + where invariants would lose information. + + 3. {b Inter-procedural delegation}: If all arguments to the PO are + received as arguments to the calling function (as established by + invariants), the PO is delegated to the function api and converted + into a precondition of the function. These preconditions will then + be converted into POs on the callers of the function in the next + analysis round. + + {b Proof obligations currently supported:} + + - [XPOTrustedOsCmdString(cmd)]: [cmd] is safe to use as an argument to + [system] + + - [XPOTrustedOsCmdFmtString(fmt, kind, size)]: the format string [fmt] + constructs a string that is safe to use as an argument to [system]. + The [kind] determines the location of the format arguments: [VA_LIST] + (as in [vsprintf]) or [FMT_ARGS] (as in [sprintf]). The [size] argument + is optional; if present it denotes the maximum length of the string + that can be formed. + A format string [fmt] is considered to construct a string that is safe + to pass to a call to [system] if it does not contain any %s format + specifiers. + + - [XPOOutputFormatString(fmt)]: the format string [fmt] is a constant + string. + + - [XPOBlockWrite (ty, buffer, size)]: at least [size] bytes can be safely + written to [buffer]. + + - [XPOBuffer (ty, buffer, size)]: at least [size] bytes can be safely + read from [buffer]. + + - [XPONotNull (ptr)]: [ptr] is not null. + + - [XPONullTerminated (ptr)]: the string address [ptr] points to a string + that is null-terminated. + + - [XPOInitializedRange (ty, ptr, size)]: the address [ptr] points to a + buffer that has been initialized to at least [size] bytes. + + {b Side effects:} + + The discharge of proof obligations has the following side effects on other + parts of the code: + + 1. Update of the status of the proof obligation in the proof obligations + storage in [BCHProofObligations] if the status changes. + + 2. Addition of a function parameter to the calling function api for all + parameters that occur in a delegated PO (in [BCHFunctionInfo]). This has + no effect if the function api was derived externally (e.g., from a header + file), or if the parameter was added before. + + 3. Creation of a precondition on the calling function api if a PO is + delegated to the function api (in [BCHFunctionInfo]). + + 4. Creation of an [XXBlockWrite] side effect on the calling function api + if an [XPOBlockWrite] PO is delegated to the function function api + (in [BCHFunctionInfo]). + *) + +(** Main entry point for discharging proof obligations. [max_passes] denotes + the maximum number of passes made to resolve proof obligations delegated + locally within the function. The default value is 8. In practice a fixed + point will be reached with a value of at most 3 and iteration will stop + at that point.*) +val discharge_function_proofobligations: + ?max_passes:int -> BCHLibTypes.function_info_int -> unit From a2a55fd9f81ac16d939a9b3f906a22cce085f842 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 09:55:03 -0700 Subject: [PATCH 07/15] CHB: introduce command injection predicates --- CodeHawk/CHB/bchlib/bCHExternalPredicate.ml | 74 +++++++++++++++++-- CodeHawk/CHB/bchlib/bCHExternalPredicate.mli | 4 + CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 25 ++++++- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 55 +++++++++----- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 15 +++- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli | 1 + CodeHawk/CHB/bchlib/bCHXPODictionary.ml | 11 ++- CodeHawk/CHB/bchlib/bCHXPOPredicate.ml | 43 +++++++++-- 8 files changed, 188 insertions(+), 40 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index 373b41899..b89044b9d 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml @@ -68,6 +68,21 @@ let string_to_quote_status (s: string): quote_status_t traceresult = Error [(elocm __LINE__) ^ "Illegal quote_status: " ^ s] +let format_args_kind_to_string (f: format_args_kind_t): string = + match f with + | VA_LIST -> "VA_LIST" + | FMT_ARGS -> "FMT_ARGS" + + +let string_to_format_args_kind (s: string): format_args_kind_t traceresult = + match s with + | "VA_LIST" -> Ok VA_LIST + | "FMT_ARGS" -> Ok FMT_ARGS + | _ -> + Error [(elocm __LINE__) ^ "Illegal format_args_kind: " ^ s] + + + let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = let btc = bterm_compare in match (p1, p2) with @@ -176,9 +191,26 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = | (XXTrustedString t1, XXTrustedString t2) -> btc t1 t2 | (XXTrustedString _, _) -> -1 | (_, XXTrustedString _) -> 1 - | (XXTrustedOsCmdString (t1, _, _), XXTrustedOsCmdString (t2, _, _)) -> btc t1 t2 + | (XXTrustedOsCmdString t1, XXTrustedOsCmdString t2) -> btc t1 t2 | (XXTrustedOsCmdString _, _) -> -1 | (_, XXTrustedOsCmdString _) -> 1 + | (XXTrustedOsCmdFmtString (t1, _, _), XXTrustedOsCmdFmtString (t2, _, _)) -> + btc t1 t2 + | (XXTrustedOsCmdFmtString _, _) -> -1 + | (_, XXTrustedOsCmdFmtString _) -> 1 + | (XXTrustedOsCmdFmtArgString (t1, _, _), XXTrustedOsCmdFmtArgString (t2, _, _)) -> + btc t1 t2 + | (XXTrustedOsCmdFmtArgString _, _) -> -1 + | (_, XXTrustedOsCmdFmtArgString _) -> 1 + | (XXWritesStringFromFmtString (t11, t12, _, _), + XXWritesStringFromFmtString (t21, t22, _, _)) -> + let l1 = btc t11 t21 in + if l1 = 0 then + btc t12 t22 + else + l1 + | (XXWritesStringFromFmtString _, _) -> -1 + | (_, XXWritesStringFromFmtString _) -> 1 | (XXValidMem t1, XXValidMem t2) -> btc t1 t2 | (XXValidMem _, _) -> -1 | (_, XXValidMem _) -> 1 @@ -227,7 +259,10 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list = | XXStartsThread (t, tt) -> t :: tt | XXTainted t -> [t] | XXTrustedString t -> [t] - | XXTrustedOsCmdString (t, _, _) -> [t] + | XXTrustedOsCmdString t -> [t] + | XXTrustedOsCmdFmtString (t, _, _) -> [t] + | XXTrustedOsCmdFmtArgString (t, _, _) -> [t] + | XXWritesStringFromFmtString (t1, t2, _, _) -> [t1; t2] | XXValidMem t -> [t] | XXDisjunction pl -> List.concat (List.map xxpredicate_terms pl) | XXConditional (p1, p2) -> @@ -378,14 +413,34 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) = | XXStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XXTainted t -> default "tainted" [t] | XXTrustedString t -> default "trusted-string" [t] - | XXTrustedOsCmdString (t, isfmtstring, quotes) -> + | XXTrustedOsCmdString t -> default "trusted-os-cmd-string" [t] + | XXTrustedOsCmdFmtString (t, kind, optlen) -> LBLOCK [ - STR "trusted-os-cmd-string("; + STR "trusted-os-cmd-fmt-string("; btp t; STR ", "; - STR (if isfmtstring then "true" else "false"); + STR (format_args_kind_to_string kind); + STR ", "; + (match optlen with Some i -> btp i | _ -> STR "_"); + STR ")"] + | XXTrustedOsCmdFmtArgString (t, quotes, optlen) -> + LBLOCK [ + STR "trusted-os-cmd-fmt-arg-string("; + btp t; STR ", "; STR (quote_status_to_string quotes); + STR ", "; + (match optlen with Some i -> INT i | _ -> STR "_"); + STR ")"] + | XXWritesStringFromFmtString (t1, t2, kind, optlen) -> + LBLOCK [ + STR "writes-string-from-format-string("; + btp t1; + STR ", "; + btp t2; + STR (format_args_kind_to_string kind); + STR ", "; + (match optlen with Some i -> btp i | _ -> STR "_"); STR ")"] | XXValidMem t -> default "valid-mem" [t] | XXDisjunction pl -> @@ -432,8 +487,13 @@ let rec modify_types_xxp | XXStartsThread (t, tt) -> XXStartsThread (mbt t, List.map mbt tt) | XXTainted t -> XXTainted (mbt t) | XXTrustedString t -> XXTrustedString (mbt t) - | XXTrustedOsCmdString (t, isfmtstring, q) -> - XXTrustedOsCmdString (mbt t, isfmtstring, q) + | XXTrustedOsCmdString t -> XXTrustedOsCmdString (mbt t) + | XXTrustedOsCmdFmtString (t, kind, optlen) -> + XXTrustedOsCmdFmtString (mbt t, kind, optlen) + | XXTrustedOsCmdFmtArgString (t, quotes, optlen) -> + XXTrustedOsCmdFmtArgString (mbt t, quotes, optlen) + | XXWritesStringFromFmtString (t1, t2, kind, optlen) -> + XXWritesStringFromFmtString (mbt t1, mbt t2, kind, optlen) | XXValidMem t -> XXValidMem (mbt t) | XXDisjunction xl -> XXDisjunction (List.map mxp xl) | XXConditional (x1, x2) -> XXConditional (mxp x1, mxp x2) diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli b/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli index 0213ea47c..1168e5400 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.mli @@ -86,6 +86,10 @@ val quote_status_to_string: quote_status_t -> string val string_to_quote_status: string -> quote_status_t traceresult +val format_args_kind_to_string: format_args_kind_t -> string + +val string_to_format_args_kind: string -> format_args_kind_t traceresult + val relational_op_to_string: relational_op_t -> string val relational_op_to_xml_string: relational_op_t -> string diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 5c9d70423..95b85b6db 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -487,6 +487,8 @@ object (self) method index_xxpredicate (p: xxpredicate_t) = let ib b = if b then 1 else 0 in let it = self#index_bterm in + let optit optbt = match optbt with Some bt -> it bt | _ -> -1 in + let ioptlen optlen = match optlen with Some i -> i | _ -> -1 in let ity = bcd#index_typ in let tags = [xxpredicate_mcts#ts p] in let key = match p with @@ -522,8 +524,14 @@ object (self) | XXStartsThread (t, tl) -> (tags, List.map it (t::tl)) | XXTainted t -> (tags, [it t]) | XXTrustedString t -> (tags, [it t]) - | XXTrustedOsCmdString (t, isfmtstring, q) -> - (tags @ [quote_status_mfts#ts q], [it t; if isfmtstring then 1 else 0]) + | XXTrustedOsCmdString t -> (tags, [it t]) + | XXTrustedOsCmdFmtString (t, kind, optlen) -> + (tags @ [format_args_kind_mfts#ts kind], [it t; optit optlen]) + | XXTrustedOsCmdFmtArgString (t, quotes, optlen) -> + (tags @ [quote_status_mfts#ts quotes], [it t; ioptlen optlen]) + | XXWritesStringFromFmtString (dest, fmt, kind, optlen) -> + (tags @ [format_args_kind_mfts#ts kind], + [it dest; it fmt; optit optlen]) | XXValidMem t -> (tags, [it t]) | XXDisjunction pl -> (tags, [self#index_xxpredicate_list pl]) | XXConditional (p1, p2) -> @@ -544,7 +552,9 @@ object (self) let t = t name tags in let a = a name args in let gt = self#get_bterm in + let gt_opt i = if i >= 0 then Some (gt i) else None in let gty = bcd#get_typ in + let getoptlen a = if a >= 0 then Some a else None in match (t 0) with | "ab" -> XXAllocationBase (gt (a 0)) | "bw" -> XXBlockWrite (gty (a 0), gt (a 1), gt (a 2)) @@ -576,9 +586,18 @@ object (self) | "errno" -> XXSetsErrno | "st" -> XXStartsThread (gt (a 0), List.map gt (List.tl args)) | "t" -> XXTainted (gt (a 0)) - | "tc" -> XXTrustedOsCmdString (gt (a 0), (a 1) = 1, quote_status_mfts#fs (t 1)) + | "tc" -> XXTrustedOsCmdString (gt (a 0)) + | "tfa" -> + XXTrustedOsCmdFmtArgString ( + gt (a 0), quote_status_mfts#fs (t 1), getoptlen (a 1)) + | "tfs" -> + XXTrustedOsCmdFmtString ( + gt (a 0), format_args_kind_mfts#fs (t 1), gt_opt (a 1)) | "ts" -> XXTrustedString (gt (a 0)) | "v" -> XXValidMem (gt (a 0)) + | "wfs" -> + XXWritesStringFromFmtString ( + gt (a 0), gt (a 1), format_args_kind_mfts#fs (t 1), gt_opt (a 2)) | "dis" -> XXDisjunction (self#get_xxpredicate_list (a 0)) | "con" -> XXConditional (self#get_xxpredicate (a 0), self#get_xxpredicate (a 1)) | s -> raise_tag_error name s xxpredicate_mcts#tags diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 5ad0bcbb4..e8558452e 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2365,6 +2365,8 @@ type c_struct_constant_t = type quote_status_t = NO_QUOTES | SINGLE_QUOTES | DOUBLE_QUOTES +type format_args_kind_t = VA_LIST | FMT_ARGS + (** Predicate over external terms to represent function preconditions, postconditions, and side effects.*) @@ -2420,10 +2422,25 @@ type xxpredicate_t = parameters *) | XXTainted of bterm_t (** value of term is externally controlled *) | XXTrustedString of bterm_t (** value of term is trusted *) - | XXTrustedOsCmdString of bterm_t * bool * quote_status_t - (** value of term is safe to pass as an argument to system(.), or is - safe to pass as a format argument with the given quotation status - if is_fmt_string is true. *) + | XXTrustedOsCmdString of bterm_t + (** value of term is safe to pass as an argument to system(.) *) + + | XXTrustedOsCmdFmtString of bterm_t * format_args_kind_t * bterm_t option + (** the string value constructed by the format string bterm is safe to + pass as an argument to system(.). If a length is given the string + must evaluate to a value that has string length less than the given + length*) + + | XXTrustedOsCmdFmtArgString of bterm_t * quote_status_t * int option + (** the string value bterm is safe to pass as a format argument where the + format specifier is enclosed in quotes according to the quote_status. + If a length is given the string length is less than the given length.*) + + | XXWritesStringFromFmtString of + bterm_t * bterm_t * format_args_kind_t * bterm_t option + (** side effect that asserts that a string is constructed from the format + string indicated by the second bterm and written to the first bterm. + An optional length imposes a maximum length on the string being written.*) | XXValidMem of bterm_t (** memory region pointed to be by term has not been freed *) @@ -2610,7 +2627,10 @@ type xpo_predicate_t = | XPOStartsThread of xpr_t * xpr_t list | XPOTainted of xpr_t | XPOTrustedString of xpr_t - | XPOTrustedOsCmdString of xpr_t * bool * quote_status_t + | XPOTrustedOsCmdString of xpr_t + | XPOTrustedOsCmdFmtString of xpr_t * format_args_kind_t * xpr_t option + | XPOTrustedOsCmdFmtArgString of xpr_t * quote_status_t * int option + | XPOWritesStringFromFmtString of xpr_t * xpr_t * format_args_kind_t * xpr_t option | XPOValidMem of xpr_t | XPODisjunction of xpo_predicate_t list | XPOConditional of xpo_predicate_t * xpo_predicate_t @@ -5516,7 +5536,7 @@ class type function_environment_int = method get_initialized_string_value: variable_t -> int -> string - method variables_in_expr: xpr_t -> variable_t list + method variables_in_expr: ?include_addressof:bool -> xpr_t -> variable_t list (** {1 Scope and transactions} *) @@ -5636,6 +5656,7 @@ class type xpodictionary_int = type po_status_t = | Discharged of string | Delegated of xxpredicate_t + | DelegatedLocal of ctxt_iaddress_t * xpo_predicate_t | Requested of doubleword_int * xxpredicate_t | DelegatedGlobal of doubleword_int * xxpredicate_t | Violated of string @@ -5719,19 +5740,6 @@ object (** Returns the object containing all active proof obligations.*) method proofobligations: proofobligations_int - (** Attempts to discharge some open proof obligations and if successful - updates their status. The optional argument [get_elf_string_reference] - allows this function to check if an argument is a constant string in - the binary. A constant string in the binary is considered trusted. - - The reason that it is passed in as an argument is that the elf library - code is not directly accessible from this point. It means that this - function should preferably be called from a location that has access - to the elf library. -*) - method discharge_proofobligations: - ?get_elf_string_reference:(xpr_t -> string option) -> unit -> unit - method convert_preconditions_to_attributes: b_attributes_t @@ -5914,6 +5922,12 @@ object method update_summary: function_summary_int -> unit + method add_precondition: xxpredicate_t -> unit + + method add_sideeffect: xxpredicate_t -> unit + + method add_register_parameter_location: register_t -> btype_t -> int -> unit + (** {2 Function signature}*) @@ -6531,6 +6545,9 @@ class type floc_int = method get_call_args: (fts_parameter_t * xpr_t) list method get_call_arguments: (fts_parameter_t * xpr_t) list + method get_bterm_evaluator: bterm_evaluator_int option + method get_expression_externalizer: expression_externalizer_int option + (** {1 Function summary}*) method evaluate_summary_address_term: bterm_t -> variable_t option diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 1a4248bda..0a89b0d8a 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -48,6 +48,11 @@ let quote_status_mfts: quote_status_t mfts_int = (DOUBLE_QUOTES, "d")] +let format_args_kind_mfts: format_args_kind_t mfts_int = + mk_mfts + "format_args_kind_t" [(VA_LIST, "v"); (FMT_ARGS, "f")] + + let relational_op_mfts: relational_op_t mfts_int = mk_mfts "relational_op_t" @@ -453,6 +458,9 @@ object | XXTainted _ -> "t" | XXTrustedString _ -> "ts" | XXTrustedOsCmdString _ -> "tc" + | XXTrustedOsCmdFmtString _ -> "tfs" + | XXTrustedOsCmdFmtArgString _ -> "tfa" + | XXWritesStringFromFmtString _ -> "wfs" | XXValidMem _ -> "v" | XXDisjunction _ -> "dis" | XXConditional _ -> "con" @@ -461,7 +469,7 @@ object "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; - "pos"; "sa"; "st"; "t"; "tc"; "ts"; "v"; "x" + "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" ] end @@ -508,6 +516,9 @@ object | XPOTainted _ -> "t" | XPOTrustedString _ -> "ts" | XPOTrustedOsCmdString _ -> "tc" + | XPOTrustedOsCmdFmtString _ -> "tfs" + | XPOTrustedOsCmdFmtArgString _ -> "tfa" + | XPOWritesStringFromFmtString _ -> "wfs" | XPOValidMem _ -> "v" | XPODisjunction _ -> "dis" | XPOConditional _ -> "con" @@ -516,7 +527,7 @@ object "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; - "pos"; "sa"; "st"; "t"; "tc"; "ts"; "v"; "x" + "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" ] end diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli index 925bba104..670d7f088 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli @@ -38,6 +38,7 @@ val arithmetic_op_mfts: arithmetic_op_t mfts_int val g_arithmetic_op_mfts: g_arithmetic_op mfts_int val relational_op_mfts: relational_op_t mfts_int val quote_status_mfts: quote_status_t mfts_int +val format_args_kind_mfts: format_args_kind_t mfts_int val arg_io_mfts: arg_io_t mfts_int val formatstring_type_mfts: formatstring_type_t mfts_int diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index 1ee0ea202..5df224d9c 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -65,8 +65,10 @@ object (self) method index_xpo_predicate (xpo: xpo_predicate_t) = let tags = [xpo_predicate_mcts#ts xpo] in let ib b = if b then 1 else 0 in + let ioptlen optlen = match optlen with Some i -> i | _ -> -1 in let ix = self#xd#index_xpr in let it = bcd#index_typ in + let optix optlen = match optlen with Some x -> ix x | _ -> -1 in let key = match xpo with | XPOAllocationBase x -> (tags, [ix x]) | XPOBlockWrite (ty, x1, x2) -> (tags, [it ty; ix x1; ix x2]) @@ -100,8 +102,13 @@ object (self) | XPOStartsThread (x, xl) -> (tags, (ix x) :: (List.map ix xl)) | XPOTainted x -> (tags, [ix x]) | XPOTrustedString x -> (tags, [ix x]) - | XPOTrustedOsCmdString (x, isfmtstring, q) -> - (tags @ [quote_status_mfts#ts q], [ix x; if isfmtstring then 1 else 0]) + | XPOTrustedOsCmdString x -> (tags, [ix x]) + | XPOTrustedOsCmdFmtString (x, kind, optlen) -> + (tags @ [format_args_kind_mfts#ts kind], [ix x; optix optlen]) + | XPOTrustedOsCmdFmtArgString (x, quotes, optlen) -> + (tags @ [quote_status_mfts#ts quotes], [ix x; ioptlen optlen]) + | XPOWritesStringFromFmtString (x1, x2, kind, optlen) -> + (tags @ [format_args_kind_mfts#ts kind], [ix x1; ix x2; optix optlen]) | XPOValidMem x -> (tags, [ix x]) | XPODisjunction pl -> (tags, List.map self#index_xpo_predicate pl) | XPOConditional (p1, p2) -> diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index e00d90bee..3bb4654b2 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -60,7 +60,10 @@ let rec xxp_to_xpo_predicate "unable to convert bterm" (LBLOCK [loc#toPretty; STR " "; (bterm_to_pretty t)]) in random_constant_expr in - + let optbtx opt_t = + match opt_t with + | Some t -> Some (btx t) + | _ -> None in match xxp with | XXAllocationBase t -> XPOAllocationBase (btx t) | XXBlockWrite (ty, t1, t2) -> XPOBlockWrite (ty, btx t1, btx t2) @@ -93,8 +96,13 @@ let rec xxp_to_xpo_predicate | XXStartsThread (t1, t2) -> XPOStartsThread (btx t1, List.map btx t2) | XXTainted t -> XPOTainted (btx t) | XXTrustedString t -> XPOTrustedString (btx t) - | XXTrustedOsCmdString (t, isfmtstring, quotes) -> - XPOTrustedOsCmdString (btx t, isfmtstring, quotes) + | XXTrustedOsCmdString t -> XPOTrustedOsCmdString (btx t) + | XXTrustedOsCmdFmtString (t, fmtargs, optlen) -> + XPOTrustedOsCmdFmtString (btx t, fmtargs, optbtx optlen) + | XXTrustedOsCmdFmtArgString (t, quotes, optlen) -> + XPOTrustedOsCmdFmtArgString (btx t, quotes, optlen) + | XXWritesStringFromFmtString (dest, fmt, fmtargs, optlen) -> + XPOWritesStringFromFmtString (btx dest, btx fmt, fmtargs, optbtx optlen) | XXValidMem t -> XPOValidMem (btx t) | XXDisjunction xl -> XPODisjunction (List.map (xxp_to_xpo_predicate termev loc) xl) @@ -172,15 +180,36 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = | XPOSetsErrno -> STR "sets errno" | XPOStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XPOTainted t -> default "tainted" [t] - | XPOTrustedString t -> default "trusted" [t] - | XPOTrustedOsCmdString (t, isfmtstring, quotes) -> + | XPOTrustedString t -> default "trusted-string" [t] + | XPOTrustedOsCmdString t -> default "trusted-os-cmd-string" [t] + | XPOTrustedOsCmdFmtString (t, kind, optlen) -> LBLOCK [ - STR "trusted-os-cmd-string("; + STR "trusted-os-cmd-fmt-string("; x2p t; STR ", "; - STR (if isfmtstring then "true" else "false"); + STR (format_args_kind_to_string kind); + STR ", "; + (match optlen with Some i -> x2p i | _ -> STR "_"); + STR ")"] + | XPOTrustedOsCmdFmtArgString (t, quotes, optlen) -> + LBLOCK [ + STR "trusted-os-cmd-fmt-arg-string("; + x2p t; STR ", "; STR (quote_status_to_string quotes); + STR ", "; + (match optlen with Some i -> INT i | _ -> STR "_"); + STR ")"] + | XPOWritesStringFromFmtString (t1, t2, kind, optlen) -> + LBLOCK [ + STR "writes-string-from-fmt-string("; + x2p t1; + STR ", "; + x2p t2; + STR ", "; + STR (format_args_kind_to_string kind); + STR ", "; + (match optlen with Some i -> x2p i | _ -> STR "_"); STR ")"] | XPOValidMem t -> default "valid-mem" [t] | XPODisjunction pl -> From f7e7402e06cb3571d6b22d66056bdac0ce4c3593 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 09:58:00 -0700 Subject: [PATCH 08/15] CHB: consolidate proof obligation discharge --- CodeHawk/CHB/bchlib/Makefile | 2 + CodeHawk/CHB/bchlib/bCHBCAttributes.ml | 23 ++- CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml | 4 +- .../CHB/bchlib/bCHCallSemanticsRecorder.ml | 97 +----------- CodeHawk/CHB/bchlib/bCHFloc.ml | 89 ++++++++--- CodeHawk/CHB/bchlib/bCHFloc.mli | 5 + CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 148 ++++-------------- CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml | 28 ++-- CodeHawk/CHB/bchlib/bCHPrecondition.ml | 20 +-- CodeHawk/CHB/bchlib/bCHProofObligations.ml | 20 ++- CodeHawk/CHB/bchlib/bCHSideeffect.ml | 19 +++ 11 files changed, 189 insertions(+), 266 deletions(-) diff --git a/CodeHawk/CHB/bchlib/Makefile b/CodeHawk/CHB/bchlib/Makefile index ac07914da..76abf38ab 100644 --- a/CodeHawk/CHB/bchlib/Makefile +++ b/CodeHawk/CHB/bchlib/Makefile @@ -111,6 +111,7 @@ MLIS := \ bCHCallSemanticsRecorder \ bCHFloc \ bCHCallgraph \ + bCHFunctionPODischarge \ bCHMetricsHandler \ bCHDisassemblySummary \ bCHMetrics \ @@ -204,6 +205,7 @@ SOURCES := \ bCHCallSemanticsRecorder \ bCHFloc \ bCHCallgraph \ + bCHFunctionPODischarge \ bCHMetricsHandler \ bCHDisassemblySummary \ bCHMetrics \ diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml index 964c9f2a5..16e740b58 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml +++ b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml @@ -123,7 +123,15 @@ let convert_b_attributes_to_function_conditions end) in (pre @ xpre, side @ xside, xpost) - | Attr (("format" | "chk_format"), params) -> + (* Generation of the precondition for the format string requires + using chk_format, in addition to the format attribute, because the first + one is attached to the varinfo (which is used here), while the second is + attached to the TFun type (as provided by CIL). + + In effect this requires the attribute annotation: + __attribute__ ((chk_format(printf, 1), format(printf, 1))) + *) + | Attr (("chk_format"), params) -> let pre = (match params with | [ACons ("printf", []); AInt fmtrefindex; AInt _] @@ -145,7 +153,7 @@ let convert_b_attributes_to_function_conditions __FILE__ __LINE__ []; [] end) in - (pre, [] , []) + (pre @ xpre, xside , xpost) | Attr ("chk_pre", params) -> let pre = @@ -214,5 +222,12 @@ let convert_b_attributes_to_function_conditions end) in (pre @ xpre, xside, xpost) - | _ -> - acc) ([], [], []) attrs + | Attr (attrname, _) -> + begin + log_diagnostics_result + ~tag:"convert_b_attributes_to_function_conditions" + ~msg:(name ^ ": with attribute: " ^ attrname ^ " not recognized") + __FILE__ __LINE__ + ["attrname: " ^ attrname]; + acc + end) ([], [], []) attrs diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml b/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml index af0c1f5f3..cff55f8f2 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHBCAttributesUtil.ml @@ -29,6 +29,8 @@ open BCHBCTypes +(* Note that CIL attaches the format attribute to the TFun type, while most + other attributes are attached to the varinfo of the function definition.*) let get_format_archetype (attrs: b_attributes_t) (index: int): BCHLibTypes.formatstring_type_t option = List.fold_left (fun acc attr -> @@ -36,7 +38,7 @@ let get_format_archetype | Some _ -> acc | _ -> match attr with - | Attr (("format" | "chk_format"), params) -> + | Attr ("format", params) -> (match params with | [ACons ("printf", []); AInt fmtrefindex; AInt _] | [ACons ("printf", []); AInt fmtrefindex] -> diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index 1b5f26a9c..062cdd372 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml @@ -44,7 +44,6 @@ open BCHBCTypeUtil open BCHBTerm open BCHDoubleword open BCHExternalPredicate -open BCHGlobalState open BCHLibTypes open BCHStrings open BCHXPOPredicate @@ -136,7 +135,7 @@ object (self) else Open | _ -> Open) - | XPOTrustedString x | XPOTrustedOsCmdString (x, false, _) -> + | XPOTrustedString x | XPOTrustedOsCmdString x -> (match x with | XConst (IntConst n) -> let dw = numerical_mod_to_doubleword n in @@ -174,76 +173,6 @@ object (self) | _ -> Open) | _ -> Open - (* Relies on the expression externalizer, which, at present, has only been - implemented for mips. - An alternative for delegating proof obligations is in the method - discharge_proofobligations in function_info. - Eventually these two methods should be merged or at least unified.*) - method private delegate_precondition (xpo: xpo_predicate_t): po_status_t = - match xpo with - | XPONotNull x -> - let x = simplify_xpr x in - (match self#xprxt#xpr_to_bterm t_voidptr x with - | Some (NumConstant n) when n#gt numerical_zero -> - let dw = numerical_mod_to_doubleword n in - DelegatedGlobal (dw, XXNotNull (NumConstant n)) - | Some t -> Delegated (XXNotNull t) - | _ -> Open) - | XPONullTerminated x -> - let x = simplify_xpr x in - (match self#xprxt#xpr_to_bterm t_voidptr x with - | Some (NumConstant n) when n#gt numerical_zero -> - let dw = numerical_mod_to_doubleword n in - DelegatedGlobal (dw, XXNullTerminated (NumConstant n)) - | Some t -> Delegated (XXNullTerminated t) - | _ -> Open) - | XPOBlockWrite (ty, ptr, size) -> - (match self#xprxt#xpr_to_bterm t_voidptr ptr with - | Some (NumConstant n) when n#gt numerical_zero -> - let dw = numerical_mod_to_doubleword n in - (match self#xprxt#xpr_to_bterm t_int size with - | Some (NumConstant ns) -> - DelegatedGlobal - (dw, XXBlockWrite(ty, NumConstant n, NumConstant ns)) - | _ -> Open) - | Some ptrt -> - (match self#xprxt#xpr_to_bterm t_int size with - | Some sizet -> - Delegated (XXBlockWrite (ty, ptrt, sizet)) - | _ -> Open) - | _ -> Open) - | XPOBuffer (ty, ptr, size) -> - (match self#xprxt#xpr_to_bterm t_voidptr ptr with - | Some (NumConstant n) when n#gt numerical_zero -> - let dw = numerical_mod_to_doubleword n in - (match self#xprxt#xpr_to_bterm t_int size with - | Some (NumConstant ns) -> - DelegatedGlobal - (dw, XXBlockWrite(ty, NumConstant n, NumConstant ns)) - | _ -> Open) - | Some ptrt -> - (match self#xprxt#xpr_to_bterm t_int size with - | Some sizet -> - Delegated (XXBuffer (ty, ptrt, sizet)) - | _ -> Open) - | _ -> Open) - | XPOInitializedRange (ty, ptr, size) -> - (match self#xprxt#xpr_to_bterm t_voidptr ptr with - | Some (NumConstant n) when n#gt numerical_zero -> - let dw = numerical_mod_to_doubleword n in - (match self#xprxt#xpr_to_bterm t_int size with - | Some (NumConstant ns) -> - DelegatedGlobal - (dw, XXBlockWrite(ty, NumConstant n, NumConstant ns)) - | _ -> Open) - | Some ptrt -> - (match self#xprxt#xpr_to_bterm t_int size with - | Some sizet -> - Delegated (XXInitializedRange (ty, ptrt, sizet)) - | _ -> Open) - | _ -> Open) - | _ -> Open - method record_precondition (pre: xxpredicate_t) = let xpo = xxp_to_xpo_predicate self#termev self#loc pre in let status = self#simplify_precondition xpo in @@ -253,23 +182,7 @@ object (self) ~msg:(p2s loc#toPretty) __FILE__ __LINE__ ["pre: " ^ (p2s (xxpredicate_to_pretty pre))] in - match status with - | Discharged _ -> self#add_po xpo status - | _ -> - let status = self#delegate_precondition xpo in - match status with - | Delegated xxp -> - begin - self#add_po xpo status; - self#add_pre xxp - end - | DelegatedGlobal (dw, xxp) -> - begin - self#add_po xpo status; - self#add_gpo dw xxp - end - | _ -> - self#add_po xpo status + self#add_po xpo status method private record_blockreads (pre: xxpredicate_t) = let _ = @@ -313,12 +226,6 @@ object (self) ["po: " ^ (p2s (xpo_predicate_to_pretty xpo))] in self#finfo#proofobligations#add_proofobligation self#loc#ci xpo status - method private add_gpo (dw: doubleword_int) (xxp: xxpredicate_t) = - global_system_state#add_precondition dw self#loc xxp - - method private add_pre (xxp: xxpredicate_t) = - self#finfo#update_summary (self#finfo#get_summary#add_precondition xxp) - method private add_se (xxp: xxpredicate_t) = self#finfo#update_summary (self#finfo#get_summary#add_sideeffect xxp) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 2146f1709..062dd5ab4 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -174,11 +174,50 @@ end class arm_expression_externalizer_t (finfo: function_info_int): expression_externalizer_int = -object +object (self) method finfo = finfo - method xpr_to_bterm (_: btype_t) (_: xpr_t) = None + method xpr_to_bterm (btype: btype_t) (xpr: xpr_t) = + match xpr with + | XConst (IntConst n) -> Some (NumConstant n) + | XVar v when finfo#env#is_initial_register_value v -> + TR.tfold + ~ok:(fun reg -> + let _ = + 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)) + ~error:(fun e -> + begin + log_error_result + ~tag:"xpr_to_bterm" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); String.concat ", " e]; + None + end) + (finfo#env#get_initial_register_value_register v) + | XOp ((Xf "indexsize"), [xx]) -> + let optt = self#xpr_to_bterm t_int xx in + (match optt with + | Some tt -> Some (IndexSize tt) + | _ -> None) + | XOp ((Xf "ntpos"), [xx]) -> + let optt = self#xpr_to_bterm t_int xx in + (match optt with + | Some tt -> Some (ArgNullTerminatorPos tt) + | _ -> None) + + | _ -> + begin + log_diagnostics_result + ~tag:"xpr_to_bterm:not supported" + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr)]; + None + end end @@ -442,7 +481,26 @@ object (self) method has_call_target = self#f#has_call_target self#cia - method get_call_target = self#f#get_call_target self#cia + method get_call_target: call_target_info_int = + self#f#get_call_target self#cia + + method get_bterm_evaluator: bterm_evaluator_int option = + if self#has_call_target then + let arch = system_settings#get_architecture in + let callargs = self#get_call_arguments in + match arch with + | "mips" -> Some (new mips_bterm_evaluator_t self#f callargs) + | "arm" -> Some (new arm_bterm_evaluator_t self#f callargs) + | _ -> None + else + None + + method get_expression_externalizer: expression_externalizer_int option = + let arch = system_settings#get_architecture in + match arch with + | "mips" -> Some (new mips_expression_externalizer_t self#f) + | "arm" -> Some (new arm_expression_externalizer_t self#f) + | _ -> None method update_call_target = if self#has_call_target then @@ -3381,6 +3439,7 @@ object (self) | ([], _) -> errorPostCommands | _ -> [BRANCH [LF.mkCode postCommands; LF.mkCode errorPostCommands]] + (* Only used for x86 *) method private record_precondition_effect (pre:xxpredicate_t) = match pre with | XXFunctionPointer (_,t) -> @@ -3523,6 +3582,7 @@ object (self) [] end + (* Only used for x86 *) method private record_precondition_effects (sem:function_semantics_t) = List.iter self#record_precondition_effect sem.fsem_pre @@ -3659,25 +3719,6 @@ object (self) [OPERATION { op_name = opname; op_args = [] }; ABSTRACT_VARS (v1::abstrRegs); returnassign] - method private get_bterm_xpr - (t: bterm_t) - (parargs: (fts_parameter_t * xpr_t) list): xpr_t option = - match t with - | ArgValue p -> - List.fold_left (fun acc (par, x) -> - match acc with - | Some _ -> acc - | _ -> - if (fts_parameter_compare p par) = 0 then - Some x - else - acc) None parargs - | ArgBufferSize tt -> self#get_bterm_xpr tt parargs - | IndexSize tt -> self#get_bterm_xpr tt parargs - | ByteSize tt -> self#get_bterm_xpr tt parargs - | ArgNullTerminatorPos tt -> self#get_bterm_xpr tt parargs - | _ -> None - method get_mips_call_commands = let parargs = self#get_call_arguments in let ctinfo = self#get_call_target in @@ -3838,6 +3879,10 @@ let get_floc (loc:location_int) = new floc_t (get_function_info loc#f) loc +let get_finfo_floc (finfo: function_info_int) (loc: location_int) = + new floc_t finfo loc + + let get_floc_by_address (faddr: doubleword_int) (iaddr: doubleword_int) = get_floc (make_location {loc_faddr = faddr; loc_iaddr = iaddr}) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.mli b/CodeHawk/CHB/bchlib/bCHFloc.mli index 3114ee9ee..6217979f5 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.mli +++ b/CodeHawk/CHB/bchlib/bCHFloc.mli @@ -49,6 +49,11 @@ open BCHLibTypes val get_floc : location_int -> floc_int +(** [get_finfo_floc finfo floc] returns a [floc] object within function [finfo] + at the location [loc].*) +val get_finfo_floc: function_info_int -> location_int -> floc_int + + (** [get_floc_by_address faddr iaddr] returns a [floc] object for the context-free instruction address [iaddr] in the function with address [faddr] *) val get_floc_by_address: doubleword_int -> doubleword_int -> floc_int diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index bd52fb8f1..8238287dc 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -75,7 +75,6 @@ open BCHUtilities open BCHVariable open BCHVariableNames open BCHXPODictionary -open BCHXPOPredicate module H = Hashtbl module LF = CHOnlineCodeSet.LanguageFactory @@ -1109,7 +1108,8 @@ object (self) else [] - method variables_in_expr (expr: xpr_t): variable_t list = + method variables_in_expr + ?(include_addressof=true) (expr: xpr_t): variable_t list = let s = new VariableCollections.set_t in let rec vs x = match x with @@ -1120,6 +1120,7 @@ object (self) List.iter vs xprs end | XConst _ -> () + | XOp (Xf "addressofvar", _) when not include_addressof -> () | XOp (_, l) -> List.iter vs l | XAttr (_, e) -> vs e in begin @@ -1711,118 +1712,6 @@ object (self) method proofobligations = proofobligations - method discharge_proofobligations - ?(get_elf_string_reference=(fun _ -> None)) () = - let openpos = self#proofobligations#open_proofobligations in - List.iter (fun po -> - let newstatus = - match po#xpo with - | XPOTrustedOsCmdString (x, false, _) -> - (match get_elf_string_reference x with - | Some s -> Discharged ("constant string: " ^ s) - | _ -> Open) - | XPOOutputFormatString (XVar v) - when self#env#is_initial_register_value v -> - TR.tfold - ~ok:(fun reg -> - let _ = - self#update_summary - (self#get_summary#add_register_parameter_location - reg t_charptr 4) in - let ftspar = self#get_summary#get_parameter_for_register reg in - let dst = ArgValue ftspar in - let xpred = XXOutputFormatString dst in - let updatedsummary = self#get_summary#add_precondition xpred in - let _ = self#update_summary updatedsummary in - Delegated xpred) - ~error:(fun e -> - begin - log_error_result - ~tag:"delegate_proofobligation" - __FILE__ __LINE__ - ["v: " ^ (p2s v#toPretty); - String.concat ", " e]; - Open - end) - (self#env#get_initial_register_value_register v) - - | XPOBuffer ( - _ty, - XOp (XMinus, [XVar v; XConst (IntConst off)]), - XConst (IntConst size)) - | XPOBlockWrite ( - _ty, - XOp (XMinus, [XVar v; XConst (IntConst off)]), - XConst (IntConst size)) - when self#env#is_initial_stackpointer_value v -> - let buffer = self#stackframe#get_max_slot_size off#neg#toInt in - (match buffer with - | Some slotsize -> - if size#toInt <= slotsize then - Discharged ( - "buffer size " ^ size#toString - ^ " fits in available space of " - ^ (string_of_int slotsize) - ^ " bytes") - else - Violated ( - "buffer size " - ^ size#toString ^ " is too large; available space is " - ^ (string_of_int slotsize) ^ " bytes") - | _ -> - let _ = - log_diagnostics_result - ~tag:"discharge_proofobligations:open" - ~msg:(p2s po#loc#toPretty) - __FILE__ __LINE__ - ["xpo: " ^ (p2s (xpo_predicate_to_pretty po#xpo)); - "Unable to determine buffer size at offset " - ^ off#toString] in - Open) - | XPOBlockWrite (ty, XVar v, bwlen) when - self#env#is_initial_register_value v -> - TR.tfold - ~ok:(fun reg -> - let paramty = TPtr (ty, []) in - let _ = - self#update_summary - (self#get_summary#add_register_parameter_location - reg paramty 4) in - let ftspar = self#get_summary#get_parameter_for_register reg in - let dst = ArgValue ftspar in - let lenterm = - match bwlen with - | XConst (IntConst size) -> NumConstant size - | _ -> RunTimeValue in - let xpred = XXBlockWrite (ty, dst, lenterm) in - let updatedsummary = self#get_summary#add_precondition xpred in - let updatedsummary = updatedsummary#add_sideeffect xpred in - let _ = self#update_summary updatedsummary in - Delegated xpred) - ~error:(fun e -> - begin - log_error_result - ~tag:"delegate_proofobligation" - __FILE__ __LINE__ - ["v: " ^ (p2s v#toPretty); - String.concat ", " e]; - Open - end) - (self#env#get_initial_register_value_register v) - | _ -> Open in - match newstatus with - | Open -> () - | _ -> - begin - log_diagnostics_result - ~tag:"discharge_proofobligations" - ~msg:(p2s po#loc#toPretty) - __FILE__ __LINE__ - ["xpo: " ^ (p2s (xpo_predicate_to_pretty po#xpo)); - "status: " ^ (p2s (po_status_to_pretty newstatus))]; - po#update_status newstatus - end) openpos - method convert_preconditions_to_attributes = let delegatedpos = self#proofobligations#delegated_proofobligations in List.fold_left (fun acc po -> @@ -2061,6 +1950,37 @@ object (self) method update_summary (fs: function_summary_int) = appsummary <- fs + method add_precondition (pre: xxpredicate_t) = + let _ = + log_diagnostics_result + ~tag:"add_precondition" + ~msg:self#get_name + __FILE__ __LINE__ + ["pre: " ^ (p2s (BCHExternalPredicate.xxpredicate_to_pretty pre))] in + self#update_summary (self#get_summary#add_precondition pre) + + method add_sideeffect (se: xxpredicate_t) = + let _ = + log_diagnostics_result + ~tag:"add_sideeffect" + ~msg:self#get_name + __FILE__ __LINE__ + ["se: " ^ (p2s (BCHExternalPredicate.xxpredicate_to_pretty se))] in + self#update_summary (self#get_summary#add_sideeffect se) + + method add_register_parameter_location + (reg: register_t) (btype: btype_t) (size: int) = + let _ = + log_diagnostics_result + ~tag:"add_register_parameter_location" + ~msg:self#get_name + __FILE__ __LINE__ + ["reg: " ^ (register_to_string reg); + "btype: " ^ (btype_to_string btype); + "size: " ^ (string_of_int size)] in + self#update_summary + (self#get_summary#add_register_parameter_location reg btype size) + method private get_function_semantics = self#get_summary#get_function_semantics diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index 0eb513ae3..20b4ab799 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -46,6 +46,7 @@ open BCHSideeffect open BCHLibTypes open BCHPostcondition +let p2s = CHPrettyUtil.pretty_to_string let id = BCHInterfaceDictionary.interface_dictionary @@ -322,22 +323,29 @@ let bvarinfo_to_function_semantics let (preconditions, sideeffects, _) = convert_b_attributes_to_function_conditions vinfo.bvname fintf vinfo.bvattr in let _ = - chlog#add - "bvarinfo attributes" - (LBLOCK [ - STR vinfo.bvname; - STR ": "; - STR (attributes_to_string vinfo.bvattr)]) in + log_diagnostics_result + ~tag:"bvarinfo_to_function_semantics" + ~msg:vinfo.bvname + __FILE__ __LINE__ + ["pre: " ^ (string_of_int (List.length preconditions)); + "side: " ^ (string_of_int (List.length sideeffects)); + "attrs: " ^ (attributes_to_string vinfo.bvattr)] in let fsem = {default_function_semantics with fsem_pre = preconditions; fsem_sideeffects = sideeffects} in let _ = - ch_diagnostics_log#add - "function semantics" - (LBLOCK [STR vinfo.bvname; STR ": "; - function_semantics_to_pretty fsem]) in + log_diagnostics_result + ~tag:"bvarinfo_to_function_semantics" + ~msg:vinfo.bvname + __FILE__ __LINE__ + ["semantics: " ^ (p2s (function_semantics_to_pretty fsem))] in fsem else + let _ = + log_diagnostics_result + ~tag:"bvarinfo_to_function_semantics:default" + __FILE__ __LINE__ + ["vinfo: " ^ vinfo.bvname] in default_function_semantics diff --git a/CodeHawk/CHB/bchlib/bCHPrecondition.ml b/CodeHawk/CHB/bchlib/bCHPrecondition.ml index 8a285d411..f51f81be1 100644 --- a/CodeHawk/CHB/bchlib/bCHPrecondition.ml +++ b/CodeHawk/CHB/bchlib/bCHPrecondition.ml @@ -226,24 +226,8 @@ let read_xml_precondition_xxpredicate [XXBlockWrite (gty (arg 0), dest, gt (arg 2)); XXNotNull dest] | "deref-write-null" -> [XXBlockWrite (gty (arg 0), gt (arg 1), gt (arg 2))] - | "trusted-os-cmd-string" -> - let s = gt (arg 0) in - let fmtstring = - (pNode#hasNamedAttribute "fmtstring") - && (pNode#getAttribute "fmtstring") = "true" in - if pNode#hasNamedAttribute "quotes" then - let a = pNode#getAttribute "quotes" in - TR.tfold - ~ok:(fun q -> [XXTrustedOsCmdString(s, fmtstring, q)]) - ~error:(fun e -> - raise_xml_error - node - (LBLOCK [ - STR "Problem in parsing trusted-os-cmd-string: "; - STR (String.concat ", " e)])) - (string_to_quote_status a) - else - [XXTrustedOsCmdString(s, fmtstring, NO_QUOTES)] + | "trusted-os-cmd-string" -> [XXTrustedOsCmdString(gt (arg 0))] + | s -> raise_xml_error node diff --git a/CodeHawk/CHB/bchlib/bCHProofObligations.ml b/CodeHawk/CHB/bchlib/bCHProofObligations.ml index 44914c4c0..e253959a0 100644 --- a/CodeHawk/CHB/bchlib/bCHProofObligations.ml +++ b/CodeHawk/CHB/bchlib/bCHProofObligations.ml @@ -53,6 +53,13 @@ let po_status_to_pretty (s: po_status_t): pretty_t = match s with | Discharged s -> LBLOCK [STR "discharged("; STR s; STR ")"] | Delegated x -> LBLOCK [STR "delegated("; xxpredicate_to_pretty x; STR ")"] + | DelegatedLocal (ci, x) -> + LBLOCK [ + STR "delegated-local("; + STR ci; + STR ", "; + xpo_predicate_to_pretty x; + STR ")"] | Requested (dw, x) -> LBLOCK [ STR "requested("; dw#toPretty; STR ", "; xxpredicate_to_pretty x; STR ")"] @@ -67,7 +74,8 @@ let po_status_to_pretty (s: po_status_t): pretty_t = | Open -> STR "open" -let write_xml_po_status (node: xml_element_int) (s: po_status_t) = +let write_xml_po_status + (node: xml_element_int) (xpod: xpodictionary_int) (s: po_status_t) = match s with | Discharged s -> begin @@ -79,6 +87,12 @@ let write_xml_po_status (node: xml_element_int) (s: po_status_t) = node#setAttribute "s" "del"; id#write_xml_xxpredicate node x end + | DelegatedLocal (ci, x) -> + begin + node#setAttribute "s" "local"; + node#setAttribute "iaddr" ci; + xpod#write_xml_xpo_predicate node x + end | Requested (dw, x) -> begin node#setAttribute "s" "req"; @@ -196,9 +210,11 @@ object (self) (List.map (fun po -> let ponode = xmlElement "po" in + let stnode = xmlElement "status" in begin self#xpod#write_xml_xpo_predicate ponode po#xpo; - write_xml_po_status ponode po#status; + write_xml_po_status stnode xpod po#status; + ponode#appendChildren [stnode]; ponode end) polist); anode diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml index 3e72aebb1..20b3a7f2c 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml @@ -126,6 +126,7 @@ let read_xml_sideeffect (thisf: bterm_t) (parameters: fts_parameter_t list): xxpredicate_t = let get_term n = read_xml_bterm n thisf parameters in + let gt = get_term in let get_type n = let t = read_xml_type n in match t with @@ -159,6 +160,24 @@ let read_xml_sideeffect thisf parameters) in XXConditional (condition, aux (node#getTaggedChild "apply")) + | "writes-string-from-fmt-string" -> + let kind = + if pNode#hasNamedAttribute "kind" then + pNode#getAttribute "kind" + else + "fmt_args" in + let kind = + match kind with + | "va_list" -> VA_LIST + | "fmt_args" -> FMT_ARGS + | _ -> FMT_ARGS in + let optlen = + if (List.length argNodes) = 3 then + Some (gt (arg 2)) + else + None in + XXWritesStringFromFmtString (gt (arg 0), gt (arg 1), kind, optlen) + | s -> raise_xml_error node From 6cea60d2d7c3a9ecf8cd5a9ea019da260c63c540 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 10:00:19 -0700 Subject: [PATCH 09/15] CHB:ARM: add reaching definitions for string buffers --- .../CHB/bchlibarm32/bCHFnARMDictionary.ml | 43 +++++++++++++++++-- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 38 +++++++++++++++- 2 files changed, 75 insertions(+), 6 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index b98edc28f..32cd5a757 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -298,7 +298,7 @@ object (self) TR.tfold_default get_rdef (-1) x_r in let get_all_rdefs (xpr: xpr_t): int list = - let vars = floc#env#variables_in_expr xpr in + let vars = floc#env#variables_in_expr ~include_addressof:false xpr in List.fold_left (fun acc v -> let symvar = floc#env#mk_symbolic_variable v in let varinvs = varinv#get_var_reaching_defs symvar in @@ -725,18 +725,53 @@ object (self) else register_of_arm_register AR0 in (floc#f#env#mk_register_variable reg, rtype) in + let _ = + log_diagnostics_result + ~tag:"callinstr_key" + __FILE__ __LINE__ + ["target: " ^ floc#get_call_target#get_name; + "xprs -> rdefs: " ^ (String.concat ", " (List.map x2s xprs))] in let xrdefs = List.fold_left (fun acc x -> let rdefs = get_all_rdefs x in let newixs = List.filter (fun ix -> not (List.mem ix acc)) rdefs in acc @ newixs) [] xprs in + let derefuses = + let sem = floc#get_call_target#get_semantics in + List.fold_left (fun acc p -> + match p with + | XXBlockWrite (_, dest, _) -> + (match floc#evaluate_summary_address_term dest with + | Some memVar -> memVar :: acc + | _ -> acc) + | _ -> acc) [] sem.fsem_pre in + let derefrdefs = + let sem = floc#get_call_target#get_semantics in + List.fold_left (fun acc p -> + match p with + | XXBuffer (_, dest, _) -> + (match floc#evaluate_summary_address_term dest with + | Some memVar -> (get_rdef (XVar memVar)) :: acc + | _ -> acc) + | _ -> acc) [] sem.fsem_pre in + let _ = + log_diagnostics_result + ~tag:"callinstr_key" + __FILE__ __LINE__ + ["target: " ^ floc#get_call_target#get_name; + "deref-uses: " + ^ (String.concat ", " (List.map (fun v -> p2s v#toPretty) derefuses)); + "rdefs: " ^ (String.concat ", " (List.map string_of_int rdefs)); + "xrdefs: " ^ (String.concat ", " (List.map string_of_int xrdefs)); + "deref-rdefs: " + ^ (String.concat ", " (List.map string_of_int derefrdefs))] in let vars_r = [Ok vrd] in let xprs_r = (List.rev (List.map (fun x -> Ok x) xprs)) @ (List.rev xvars) in let cxprs_r = List.rev cxprs_r in let types = [rtype] in - let rdefs = (List.rev rdefs) @ xrdefs in - let uses = [get_def_use vrd] in - let useshigh = [get_def_use_high vrd] in + let rdefs = (List.rev rdefs) @ xrdefs @ derefrdefs in + let uses = [get_def_use vrd] @ (List.map get_def_use derefuses) in + let useshigh = [get_def_use_high vrd] @ (List.map get_def_use derefuses) in let (tagstring, args) = mk_instrx_data_r ~vars_r ~types ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index ebef0d90b..a5be04498 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -712,6 +712,10 @@ let translate_arm_instruction register_of_arm_register AR0 in let returnvar = floc#f#env#mk_register_variable returnreg in let (usecmds, use, usehigh) = + (* This doesn't seem quite right, because the variable may be either + written or read. Here the assumption is made that the variable + is just read (i.e., it is used) rather than written, which would + require a def.*) List.fold_left (fun (acccmds, accuse, accusehigh) (p, x) -> let ptype = get_parameter_type p in let addressedvars = @@ -759,14 +763,44 @@ let translate_arm_instruction floc#l#toPretty; STR " Parameter type not recognized in call translation"]))) ([], [], []) callargs in - let usehigh = usehigh @ (get_use_high_vars (List.map snd callargs)) in + + let (xprdefs, xpuse, xpusehigh) = + let sem = floc#get_call_target#get_semantics in + List.fold_left (fun (accdefs, accuse, accusehigh) p -> + match p with + | XXBlockWrite (_, dest, _) -> + (match floc#evaluate_summary_address_term dest with + | Some memVar -> (memVar :: accdefs, accuse, accusehigh) + | _ -> (accdefs, accuse, accusehigh)) + | 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 + + let _ = + log_diagnostics_result + ~tag:"calltgt_cmds" + __FILE__ __LINE__ + ["call target: " ^ floc#get_call_target#get_name; + "rdefs: " ^ (String.concat ", " + (List.map (fun d -> p2s d#toPretty) xprdefs)); + "use: " ^ (String.concat ", " + (List.map (fun u -> p2s u#toPretty) xpuse)); + "usehigh: " ^ (String.concat ", " + (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 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 let callcmds = floc#get_arm_call_commands in let defcmds = floc#get_vardef_commands - ~defs:[returnvar] + ~defs:(returnvar :: xprdefs) ~clobbers:[vr1; vr2; vr3] ~use ~usehigh From 87efe762a3bee617bc374969e127b13cae12a781 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 10:01:08 -0700 Subject: [PATCH 10/15] CHB: update for proof obligation discharge --- CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml | 3 +-- CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 748c8af21..57195dd98 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -43,7 +43,6 @@ open BCHTypeConstraintStore (* bchlibarm32 *) open BCHARMAssemblyFunctions open BCHARMDictionary -open BCHARMDisassemblyUtils open BCHARMLoopStructure open BCHARMTypes open BCHFnARMDictionary @@ -226,7 +225,7 @@ object (self) mmap#write_xml_references faddr vard grNode; (* self#write_xml_btypes bNode; *) id#write_xml dNode; - finfo#discharge_proofobligations ~get_elf_string_reference (); + BCHFunctionPODischarge.discharge_function_proofobligations finfo; finfo#proofobligations#write_xml poNode; finfo#xpod#write_xml xpodNode; append [cNode; dNode; iiNode; jjNode; sfNode; grNode; xpodNode; poNode] diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml index 55951ee6b..911d54834 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml @@ -160,6 +160,7 @@ object (self) self#write_xml_cfg cNode; self#write_xml_instructions iiNode; finfo#stackframe#write_xml sfNode; + BCHFunctionPODischarge.discharge_function_proofobligations finfo; finfo#proofobligations#write_xml poNode; finfo#xpod#write_xml xpodNode; id#write_xml dNode; From 7756b563088a38b2508171886df1ff6b3a820e59 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 23:32:33 -0700 Subject: [PATCH 11/15] CHB:replace BCAttributes with AttributesFunctionSemantics --- .../bchlib/bCHAttributesFunctionSemantics.ml | 557 ++++++++++++++++++ ...mli => bCHAttributesFunctionSemantics.mli} | 5 +- CodeHawk/CHB/bchlib/bCHBCAttributes.ml | 233 -------- 3 files changed, 559 insertions(+), 236 deletions(-) create mode 100644 CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml rename CodeHawk/CHB/bchlib/{bCHBCAttributes.mli => bCHAttributesFunctionSemantics.mli} (98%) delete mode 100644 CodeHawk/CHB/bchlib/bCHBCAttributes.ml diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml new file mode 100644 index 000000000..437509c6e --- /dev/null +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -0,0 +1,557 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2024-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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHLogger +open CHTraceResult + +(* bchlib *) +open BCHBCTypes +open BCHBCTypePretty +open BCHBCTypeUtil +open BCHFtsParameter +open BCHFunctionInterface +open BCHLibTypes + +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 get_par + (fparameters: fts_parameter_t list) + (index: int): fts_parameter_t traceresult = + try + Ok (List.find (fun p -> + match p.apar_index with Some ix -> ix = index | _ -> false) + fparameters) + with + | Not_found -> + Error [(elocm __LINE__) + ^ "Unable to find parameter with index: " + ^ (string_of_int index); + "parameters: " + ^ (String.concat ", " (List.map (fun p -> p.apar_name) fparameters))] + + +let get_derefty (par: fts_parameter_t): btype_t traceresult = + if is_pointer par.apar_type then + Ok (ptr_deref par.apar_type) + else + Error [(elocm __LINE__) + ^ "Expected a pointer but found " ^ (btype_to_string par.apar_type)] + + +let fparams_to_string (fparams: fts_parameter_t list): string = + "fparams: " ^ (String.concat ", " (List.map fts_parameter_to_string fparams)) + + +let attrparams_to_string (tag: string) (attrparams: b_attrparam_t list): string = + tag ^ ": " ^ (String.concat ", " (List.map b_attrparam_to_string attrparams)) + + +let get_deref_read_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + let* ty = get_derefty par in + Ok (XXBuffer (ty, ArgValue par, RunTimeValue)) + + | ([], [AInt refindex; AInt sizeindex]) -> + let* bufferparam = get_par fparams refindex in + let* sizeparam = get_par fparams sizeindex in + let* ty = get_derefty bufferparam in + Ok (XXBuffer (ty, ArgValue bufferparam, ArgValue sizeparam)) + + | ([AInt size], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let sizeparam = CHNumerical.mkNumerical size in + Ok (XXBuffer (ty, ArgValue bufferparam, NumConstant sizeparam)) + + | ([ACons ("ntp", [])], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let bparam = ArgValue bufferparam in + Ok (XXBuffer (ty, bparam, ArgNullTerminatorPos bparam)) + + | _ -> + Error [(elocm __LINE__) ^ "deref_read params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_deref_write_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + let* ty = get_derefty par in + Ok (XXBlockWrite (ty, ArgValue par, RunTimeValue)) + + | ([], [AInt refindex; AInt sizeindex]) -> + let* bufferparam = get_par fparams refindex in + let* sizeparam = get_par fparams sizeindex in + let* ty = get_derefty bufferparam in + Ok (XXBlockWrite (ty, ArgValue bufferparam, ArgValue sizeparam)) + + | ([AInt size], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let sizeparam = CHNumerical.mkNumerical size in + Ok (XXBlockWrite (ty, ArgValue bufferparam, NumConstant sizeparam)) + + | _ -> + Error [(elocm __LINE__) ^ "deref_write params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_initialized_range_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([ACons ("ntp", [])], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let bparam = ArgValue bufferparam in + Ok (XXInitializedRange(ty, bparam, ArgNullTerminatorPos bparam)) + + | _ -> + Error [(elocm __LINE__) ^ "initialized_range params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_deref_read_write_preconditions + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t list traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + let* ty = get_derefty par in + Ok [XXBuffer (ty, ArgValue par, RunTimeValue); + XXBlockWrite (ty, ArgValue par, RunTimeValue)] + + | ([], [AInt refindex; AInt sizeindex]) -> + let* bufferparam = get_par fparams refindex in + let* sizeparam = get_par fparams sizeindex in + let* ty = get_derefty bufferparam in + Ok [XXBuffer (ty, ArgValue bufferparam, ArgValue sizeparam); + XXBlockWrite (ty, ArgValue bufferparam, ArgValue sizeparam)] + + | ([AInt size], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let sizeparam = CHNumerical.mkNumerical size in + Ok [XXBuffer (ty, ArgValue bufferparam, NumConstant sizeparam); + XXBlockWrite (ty, ArgValue bufferparam, NumConstant sizeparam)] + + | ([ACons ("ntp", [])], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let bparam = ArgValue bufferparam in + Ok [XXBuffer (ty, bparam, ArgNullTerminatorPos bparam); + XXBlockWrite (ty, bparam, RunTimeValue)] + + | _ -> + Error [(elocm __LINE__) ^ "deref_read write_params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_not_null_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXNotNull (ArgValue par)) + + | _ -> + Error [(elocm __LINE__) ^ "not_null params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_null_terminated_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXNullTerminated (ArgValue par)) + + | _ -> + Error [(elocm __LINE__) ^ "null_terminated params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_output_format_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXOutputFormatString (ArgValue par)) + + | _ -> + Error [(elocm __LINE__) ^ "output_format_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_trusted_os_cmd_fmt_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([AStr kind; AInt size], [AInt refindex]) -> + let* par = get_par fparams refindex in + let* kind = BCHExternalPredicate.string_to_format_args_kind kind in + let xsize = NumConstant (CHNumerical.mkNumerical size) in + Ok (XXTrustedOsCmdFmtString (ArgValue par, kind, Some xsize)) + + | _ -> + Error [(elocm __LINE__) ^ "trusted_os_cmd_fmt_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_chk_pre_conditions + (name: string) + (fparams: fts_parameter_t list) + (attrparams: b_attrparam_t list): xxpredicate_t list = + match attrparams with + | (ACons ("deref_read", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_pre_conditions:deref_read" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_read_precondition fparams tagparams argparams) + + | (ACons ("deref_write", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_pre_conditions:deref_write" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_write_precondition fparams tagparams argparams) + + | (ACons ("initialized_range", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:initialized_range" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_initialized_range_precondition fparams tagparams argparams) + + | (ACons ("not_null", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:not_null" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_not_null_precondition fparams tagparams argparams) + + | (ACons ("null_terminated", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:null_terminated" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_null_terminated_precondition fparams tagparams argparams) + + | (ACons ("output_format_string", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:output_format_string" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_output_format_string_precondition fparams tagparams argparams) + + | (ACons ("trusted_os_cmd_fmt_string", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:trusted_os_cmd_fmt_string" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams) + + | (ACons (tag, _)) :: _ -> + begin + log_diagnostics_result + ~tag:"get_chk_pre_conditions:tag not recognized" + ~msg:name + __FILE__ __LINE__ + ["tag: " ^ tag]; + [] + end + + | _ -> + begin + log_diagnostics_result + ~tag:"get_chk_pre_conditions:not recognized" + ~msg:name + __FILE__ __LINE__ + [fparams_to_string fparams; attrparams_to_string "attrparams" attrparams]; + [] + end + + +let get_access_preconditions + (name: string) + (fparams: fts_parameter_t list) + (attrparams: b_attrparam_t list): xxpredicate_t list = + match attrparams with + | (ACons ("read_only", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_access_preconditions:read_only" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_read_precondition fparams tagparams argparams) + + | (ACons ("write_only", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_access_preconditions:write_only" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_write_precondition fparams tagparams argparams) + + | (ACons ("read_write", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> xpre) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_access_preconditions:read_write" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_read_write_preconditions fparams tagparams argparams) + + | (ACons (tag, _)) :: _ -> + begin + log_diagnostics_result + ~tag:"get_access_preconditions:tag not recognized" + ~msg:name + __FILE__ __LINE__ + ["tag: " ^ tag]; + [] + end + + | _ -> + begin + log_diagnostics_result + ~tag:"get_access_preconditions:not yet implemented" + ~msg:name + __FILE__ __LINE__ + [fparams_to_string fparams; attrparams_to_string "params" attrparams]; + [] + end + + +let get_deref_write_sideeffect + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + let* ty = get_derefty par in + Ok (XXBlockWrite (ty, ArgValue par, RunTimeValue)) + + | ([], [AInt refindex; AInt sizeindex]) -> + let* bufferparam = get_par fparams refindex in + let* sizeparam = get_par fparams sizeindex in + let* ty = get_derefty bufferparam in + Ok (XXBlockWrite (ty, ArgValue bufferparam, ArgValue sizeparam)) + + | ([AInt size], [AInt refindex]) -> + let* bufferparam = get_par fparams refindex in + let* ty = get_derefty bufferparam in + let sizeparam = CHNumerical.mkNumerical size in + Ok (XXBlockWrite (ty, ArgValue bufferparam, NumConstant sizeparam)) + + | _ -> + Error [(elocm __LINE__) ^ "deref_write_sideeffect params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_access_sideeffect + (name: string) + (fparams: fts_parameter_t list) + (attrparams: b_attrparam_t list): xxpredicate_t list = + match attrparams with + | (ACons ("read_only", _)) :: _ -> [] + + | (ACons (("write_only" | "read_write"), tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_access_sideeffect:write_only_read_write" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_deref_write_sideeffect fparams tagparams argparams) + + | (ACons (tag, _)) :: _ -> + begin + log_diagnostics_result + ~tag:"get_access_sideeffect:tag not recognized" + ~msg:name + __FILE__ __LINE__ + ["tag: " ^ tag]; + [] + end + + | _ -> + begin + log_diagnostics_result + ~tag:"get_access_sideeffect:not yet implemented" + ~msg:name + __FILE__ __LINE__ + [fparams_to_string fparams; attrparams_to_string "params" attrparams]; + [] + end + + +let convert_b_attributes_to_function_conditions + (fintf: function_interface_t) + (attrs: b_attributes_t): + (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) = + let fparameters = get_fts_parameters fintf in + let name = fintf.fintf_name in + + List.fold_left (fun ((xpre, xside, xpost) as acc) attr -> + match attr with + | Attr (("acccess" | "chk_access"), attrparams) -> + let pre = get_access_preconditions name fparameters attrparams in + let side = get_access_sideeffect name fparameters attrparams in + (pre @ xpre, side @ xside, xpost) + + | Attr ("chk_pre", attrparams) -> + let pre = get_chk_pre_conditions name fparameters attrparams in + (pre @ xpre, xside, xpost) + + | Attr (attrname, _) -> + begin + log_diagnostics_result + ~tag:"convert_b_attributes_to_function_conditions:not yet handled" + ~msg:name + __FILE__ __LINE__ + ["attrname: " ^ attrname]; + acc + end) ([], [], []) attrs diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli similarity index 98% rename from CodeHawk/CHB/bchlib/bCHBCAttributes.mli rename to CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli index c55e58338..624b45b09 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024-2025 Aarno Labs LLC + Copyright (c) 2024-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 @@ -83,7 +83,6 @@ open BCHLibTypes *) val convert_b_attributes_to_function_conditions: - string - -> function_interface_t + function_interface_t -> b_attributes_t -> (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml deleted file mode 100644 index 16e740b58..000000000 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml +++ /dev/null @@ -1,233 +0,0 @@ -(* ============================================================================= - CodeHawk Binary Analyzer - Author: Henny Sipma - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2024-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 - in the Software without restriction, including without limitation the rights - to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - copies of the Software, and to permit persons to whom the Software is - furnished to do so, subject to the following conditions: - - The above copyright notice and this permission notice shall be included in all - copies or substantial portions of the Software. - - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -(* chlib *) -open CHPretty - -(* chutil *) -open CHLogger - -(* bchlib *) -open BCHBasicTypes -open BCHBCTypes -open BCHBCTypePretty -open BCHBCTypeUtil -open BCHFtsParameter -open BCHFunctionInterface -open BCHLibTypes - - - -let convert_b_attributes_to_function_conditions - (name: string) - (fintf: function_interface_t) - (attrs: b_attributes_t): - (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) = - let parameters = get_fts_parameters fintf in - let get_par (n: int) = - try - List.find (fun p -> - match p.apar_index with Some ix -> ix = n | _ -> false) parameters - with - | Not_found -> - raise - (BCH_failure - (LBLOCK [ - STR "No parameter with index "; - INT n; - pretty_print_list (List.map (fun p -> p.apar_name) parameters) - (fun s -> STR s) "[" "," "]"])) in - let get_derefty (par: fts_parameter_t): btype_t = - if is_pointer par.apar_type then - ptr_deref par.apar_type - else - raise - (BCH_failure - (LBLOCK [ - STR "parameter is not a pointer type: "; - fts_parameter_to_pretty par])) in - List.fold_left (fun ((xpre, xside, xpost) as acc) attr -> - match attr with - | Attr (("access" | "chk_access"), params) -> - let (pre, side) = - (match params with - | [ACons ("read_only", []); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - ([XXBuffer (ty, ArgValue par, RunTimeValue)], []) - - | [ACons ("read_only", []); AInt refindex; AInt sizeindex] -> - let rpar = get_par refindex in - let spar = get_par sizeindex in - let ty = get_derefty rpar in - ([XXBuffer (ty, ArgValue rpar, ArgValue spar)], []) - - | [ACons (("write_only" | "read_write"), []); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - ([XXBuffer (ty, ArgValue par, RunTimeValue); - XXBlockWrite (ty, ArgValue par, RunTimeValue)], - [XXBlockWrite (ty, ArgValue par, RunTimeValue)]) - - | [ACons (("write_only" | "read_write"), []); - AInt refindex; AInt sizeindex] -> - let rpar = get_par refindex in - let spar = get_par sizeindex in - let ty = get_derefty rpar in - ([XXBuffer (ty, ArgValue rpar, ArgValue spar); - XXBlockWrite (ty, ArgValue rpar, RunTimeValue)], - [XXBlockWrite (ty, ArgValue rpar, ArgValue spar)]) - - | [ACons ("write_only", [AInt buffersize]); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - let bytesize = CHNumerical.mkNumerical buffersize in - ([XXBuffer (ty, ArgValue par, NumConstant bytesize); - XXBlockWrite (ty, ArgValue par, NumConstant bytesize)], - [XXBlockWrite (ty, ArgValue par, NumConstant bytesize)]) - - | _ -> - begin - log_error_result - ~msg:("attribute conversion for " ^ name ^ ": " - ^ "attribute parameters " - ^ (String.concat - ", " (List.map b_attrparam_to_string params))) - ~tag:"attribute conversion" - __FILE__ __LINE__ []; - ([], []) - end) in - (pre @ xpre, side @ xside, xpost) - - (* Generation of the precondition for the format string requires - using chk_format, in addition to the format attribute, because the first - one is attached to the varinfo (which is used here), while the second is - attached to the TFun type (as provided by CIL). - - In effect this requires the attribute annotation: - __attribute__ ((chk_format(printf, 1), format(printf, 1))) - *) - | Attr (("chk_format"), params) -> - let pre = - (match params with - | [ACons ("printf", []); AInt fmtrefindex; AInt _] - | [ACons ("printf", []); AInt fmtrefindex] -> - let fmtpar = get_par fmtrefindex in - [XXOutputFormatString (ArgValue fmtpar)] - | [ACons ("scanf", []); AInt fmtrefindex; AInt _] - | [ACons ("scanf", []); AInt fmtrefindex] -> - let fmtpar = get_par fmtrefindex in - [XXInputFormatString (ArgValue fmtpar)] - | _ -> - begin - log_diagnostics_result - ~msg:("attribute conversion for " ^ name ^ ": " - ^ "attribute parameters " - ^ (String.concat - ", " (List.map b_attrparam_to_string params))) - ~tag:"attribute conversion" - __FILE__ __LINE__ []; - [] - end) in - (pre @ xpre, xside , xpost) - - | Attr ("chk_pre", params) -> - let pre = - (match params with - | [ACons ("deref_read", []); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - [XXBuffer (ty, ArgValue par, RunTimeValue)] - - | [ACons ("deref_read", []); AInt refindex; AInt sizeindex] -> - let par1 = get_par refindex in - let par2 = get_par sizeindex in - let ty = get_derefty par1 in - [XXBuffer (ty, ArgValue par1, ArgValue par2)] - - | [ACons ("deref_read", [AInt size]); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - let c = CHNumerical.mkNumerical size in - [XXBuffer (ty, ArgValue par, NumConstant c)] - - | [ACons ("deref_read", [ACons ("ntp", [])]); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - [XXBuffer (ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))] - - | [ACons ("deref_write", []); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - [XXBlockWrite (ty, ArgValue par, RunTimeValue)] - - | [ACons ("deref_write", []); AInt refindex; AInt sizeindex] -> - let par1 = get_par refindex in - let par2 = get_par sizeindex in - let ty = get_derefty par1 in - [XXBlockWrite (ty, ArgValue par1, ArgValue par2)] - - | [ACons ("deref_write", [AInt size]); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - let c = CHNumerical.mkNumerical size in - [XXBlockWrite (ty, ArgValue par, NumConstant c)] - - | [ACons ("not_null", []); AInt refindex] -> - let par = get_par refindex in - [XXNotNull (ArgValue par)] - - | [ACons ("null_terminated", []); AInt refindex] -> - let par = get_par refindex in - [XXNullTerminated (ArgValue par)] - - | [ACons ("initialized_range", [ACons ("ntp", [])]); AInt refindex] -> - let par = get_par refindex in - let ty = get_derefty par in - [XXInitializedRange ( - ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))] - - | _ -> - begin - log_error_result - ~tag:"convert_b_attributes_to_function_conditions" - ~msg:(name ^ ":chk_pre") - __FILE__ __LINE__ - [String.concat ", " (List.map b_attrparam_to_string params)]; - [] - end) in - (pre @ xpre, xside, xpost) - - | Attr (attrname, _) -> - begin - log_diagnostics_result - ~tag:"convert_b_attributes_to_function_conditions" - ~msg:(name ^ ": with attribute: " ^ attrname ^ " not recognized") - __FILE__ __LINE__ - ["attrname: " ^ attrname]; - acc - end) ([], [], []) attrs From 733c431489f7db2e80ddc9c7c3a1cdd7687b9391 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 14 May 2026 23:34:06 -0700 Subject: [PATCH 12/15] CHB: move conversion to attributes to separate file --- CodeHawk/CHB/bchlib/Makefile | 6 +- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 19 -- CodeHawk/CHB/bchlib/bCHFunctionInterface.ml | 7 + CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml | 4 +- .../bchlib/bCHFunctionSemanticsAttributes.ml | 272 ++++++++++++++++++ .../bchlib/bCHFunctionSemanticsAttributes.mli | 32 +++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 2 - .../CHB/bchlibarm32/bCHARMAnalysisResults.ml | 4 +- 8 files changed, 320 insertions(+), 26 deletions(-) create mode 100644 CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml create mode 100644 CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.mli diff --git a/CodeHawk/CHB/bchlib/Makefile b/CodeHawk/CHB/bchlib/Makefile index 76abf38ab..3f9e52373 100644 --- a/CodeHawk/CHB/bchlib/Makefile +++ b/CodeHawk/CHB/bchlib/Makefile @@ -82,7 +82,7 @@ MLIS := \ bCHPrecondition \ bCHPostcondition \ bCHSideeffect \ - bCHBCAttributes \ + bCHAttributesFunctionSemantics \ bCHFunctionSemantics \ bCHFunctionSummary \ bCHVariable \ @@ -112,6 +112,7 @@ MLIS := \ bCHFloc \ bCHCallgraph \ bCHFunctionPODischarge \ + bCHFunctionSemanticsAttributes \ bCHMetricsHandler \ bCHDisassemblySummary \ bCHMetrics \ @@ -176,7 +177,7 @@ SOURCES := \ bCHPrecondition \ bCHPostcondition \ bCHSideeffect \ - bCHBCAttributes \ + bCHAttributesFunctionSemantics \ bCHFunctionSemantics \ bCHFunctionSummary \ bCHVariable \ @@ -206,6 +207,7 @@ SOURCES := \ bCHFloc \ bCHCallgraph \ bCHFunctionPODischarge \ + bCHFunctionSemanticsAttributes \ bCHMetricsHandler \ bCHDisassemblySummary \ bCHMetrics \ diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 8238287dc..73e579666 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1712,25 +1712,6 @@ object (self) method proofobligations = proofobligations - method convert_preconditions_to_attributes = - let delegatedpos = self#proofobligations#delegated_proofobligations in - List.fold_left (fun acc po -> - match po#status with - | Delegated xpred -> - (match xpred with - | XXOutputFormatString (ArgValue par) -> - let argindex = par.apar_index in - (match argindex with - | Some argindex -> - let attr = - Attr ("chk_pre", - [ACons ("output_format_string", []); - AInt argindex]) in - attr :: acc - | _ -> acc) - | _ -> acc) - | _ -> acc) [] delegatedpos - method set_instruction_bytes (ia:ctxt_iaddress_t) (b:string) = H.add instrbytes ia b diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index d9814c585..20691fcde 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1249,6 +1249,13 @@ let mips_params (funargs: bfunarg_t list): fts_parameter_t list = params +(* Note: CIL attaches some attributes to the TFun type and some attributes to + the varinfo representing the function definition. In particular, the 'format' + attribute is attached to the TFun type, but any codehawk-specific name (e.g., + chk_format would be attached to the varinfo. + + Given that the current api expects it to be attached to the TFun, only the + format form can be used to indicate that an argument is a format string.*) let bfuntype_to_function_interface (vname: string) (vtype: btype_t): function_interface_t = match vtype with diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index 20b4ab799..a3ac8ddf2 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -35,7 +35,7 @@ open CHLogger open CHXmlDocument (* bchlib *) -open BCHBCAttributes +open BCHAttributesFunctionSemantics open BCHBCTypePretty open BCHBCTypes open BCHBCTypeUtil @@ -321,7 +321,7 @@ let bvarinfo_to_function_semantics (vinfo: bvarinfo_t) (fintf: function_interface_t): function_semantics_t = if (List.length vinfo.bvattr) > 0 then let (preconditions, sideeffects, _) = - convert_b_attributes_to_function_conditions vinfo.bvname fintf vinfo.bvattr in + convert_b_attributes_to_function_conditions fintf vinfo.bvattr in let _ = log_diagnostics_result ~tag:"bvarinfo_to_function_semantics" diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml new file mode 100644 index 000000000..1072a4982 --- /dev/null +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml @@ -0,0 +1,272 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHLogger +open CHTraceResult + +(* bchlib *) +open BCHBCTypePretty +open BCHBCTypes +open BCHBTerm +open BCHLibTypes + +module TR = CHTraceResult + + +let p2s = CHPrettyUtil.pretty_to_string + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + +let bterm_to_numerical_constant (t: bterm_t): int option = + match t with + | NumConstant n -> Some n#toInt + | _ -> None + + +let bterm_par_to_argument_index (p: bterm_t): int traceresult = + match p with + | ArgValue par -> + (match par.apar_index with + | Some index -> Ok index + | _ -> + Error [(elocm __LINE__) + ^ "Unable to convert parameter " + ^ (BCHFtsParameter.fts_parameter_to_string par) + ^ " to an index"]) + | _ -> + Error [(elocm __LINE__) ^ "Unexpected bterm: " ^ (BCHBTerm.bterm_to_string p)] + + +let is_same_bterm_par (t1: bterm_t) (t2: bterm_t): bool = + TR.tfold + ~ok:(fun index1 -> + TR.tfold + ~ok:(fun index2 -> index1 = index2) + ~error:(fun _ -> false) + (bterm_par_to_argument_index t2)) + ~error:(fun _ -> false) + (bterm_par_to_argument_index t1) + + +let chk_pre_attribute (params: b_attrparam_t list): b_attribute_t = + Attr ("chk_pre", params) + + +let convert_buffer + (loc: location_int) + (ty: btype_t) + (pbuffer: bterm_t) + (psize: bterm_t): b_attributes_t = + match psize with + | ArgNullTerminatorPos ntposarg -> + if is_same_bterm_par pbuffer ntposarg then + TR.tfold + ~ok:(fun argindex -> + [chk_pre_attribute + [ACons ("deref_read", [ACons ("ntp", [])]); AInt argindex]]) + ~error:(fun _ -> []) + (bterm_par_to_argument_index pbuffer) + else + begin + log_diagnostics_result + ~tag:"convert_buffer:unexpected ntposarg" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["pbuffer: " ^ (bterm_to_string pbuffer); + "psize: " ^ (bterm_to_string psize)]; + [] + end + | _ -> + begin + log_diagnostics_result + ~tag:"convert_buffer:not yet implemented" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["type: " ^ (btype_to_string ty); + "pbuffer: " ^ (bterm_to_string pbuffer); + "psize: " ^ (bterm_to_string psize)]; + [] + end + + +let convert_initialized_range + (loc: location_int) + (ty: btype_t) + (pbuffer: bterm_t) + (psize: bterm_t): b_attributes_t = + match psize with + | ArgNullTerminatorPos ntposarg -> + if is_same_bterm_par pbuffer ntposarg then + TR.tfold + ~ok:(fun argindex -> + [chk_pre_attribute + [ACons ("initialized_range", [ACons ("ntp", [])]); AInt argindex]]) + ~error:(fun _ -> []) + (bterm_par_to_argument_index pbuffer) + else + begin + log_diagnostics_result + ~tag:"convert_initialized_range:unexpected ntposarg" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["pbuffer: " ^ (bterm_to_string pbuffer); + "psize: " ^ (bterm_to_string psize)]; + [] + end + | _ -> + begin + log_diagnostics_result + ~tag:"convert_initialized_range:not yet implemented" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["type: " ^ (btype_to_string ty); + "pbuffer: " ^ (bterm_to_string pbuffer); + "psize: " ^ (bterm_to_string psize)]; + [] + end + + +let convert_not_null (loc: location_int) (p: bterm_t): b_attributes_t = + TR.tfold + ~ok:(fun argindex -> + [Attr ("chk_pre", [ACons ("not_null", []); AInt argindex])]) + ~error:(fun e -> + begin + log_error_result + ~tag:"convert_not_null" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (bterm_par_to_argument_index p) + + +let convert_null_terminated + (loc: location_int) (p: bterm_t): b_attributes_t = + TR.tfold + ~ok:(fun argindex -> + [Attr ("chk_pre", [ACons ("null_terminated", []); AInt argindex])]) + ~error:(fun e -> + begin + log_error_result + ~tag:"convert_null_terminated" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (bterm_par_to_argument_index p) + + +let convert_output_format_string (loc: location_int) (p: bterm_t): b_attributes_t = + TR.tfold + ~ok:(fun argindex -> + [Attr ("chk_pre", [ACons ("output_format_string", []); AInt argindex])]) + ~error:(fun e -> + begin + log_error_result + ~tag:"convert_output_format_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (bterm_par_to_argument_index p) + + +let convert_trusted_os_cmd_fmt_string + (loc: location_int) + (p: bterm_t) + (kind: format_args_kind_t) + (optlen: bterm_t option): b_attributes_t = + let kindparam = + AStr (BCHExternalPredicate.format_args_kind_to_string kind) in + let lenarg = + match optlen with + | Some t -> + (match bterm_to_numerical_constant t with + | None -> + begin + log_diagnostics_result + ~tag:"convert_trusted_cmd_fmt_string:non_constant length" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["len: " ^ (bterm_to_string t)]; + None + end + | Some numlen -> Some numlen) + | _ -> None in + TR.tfold + ~ok:(fun argindex -> + let tagparams = + match lenarg with Some len -> [kindparam; AInt len] | _ -> [kindparam] in + [chk_pre_attribute + [ACons ("trusted_os_cmd_fmt_string", tagparams); AInt argindex]]) + ~error:(fun e -> + begin + log_error_result + ~tag:"converted_trusted_os_cmd_fmt_string" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (bterm_par_to_argument_index p) + + +let convert_preconditions_to_attributes + (_finfo: function_info_int) + (preconditions: proofobligation_int list): b_attributes_t = + List.fold_left (fun acc po -> + match po#status with + | Delegated xpred -> + (match xpred with + | XXBuffer (ty, pb, ps) -> + (convert_buffer po#loc ty pb ps) @ acc + | XXInitializedRange (ty, pb, ps) -> + (convert_initialized_range po#loc ty pb ps) @ acc + | XXNotNull p -> + (convert_not_null po#loc p) @ acc + | XXNullTerminated p -> + (convert_null_terminated po#loc p) @ acc + | XXOutputFormatString p -> + (convert_output_format_string po#loc p) @ acc + | XXTrustedOsCmdFmtString (p, kind, optlen) -> + (convert_trusted_os_cmd_fmt_string po#loc p kind optlen) @ acc + | _ -> acc) + | _ -> acc) [] preconditions + + +let convert_semantics_to_attributes (finfo: function_info_int): b_attributes_t = + let delegatedpos = finfo#proofobligations#delegated_proofobligations in + let preattrs = convert_preconditions_to_attributes finfo delegatedpos in + preattrs + diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.mli b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.mli new file mode 100644 index 000000000..17215a07e --- /dev/null +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.mli @@ -0,0 +1,32 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* bchlib *) +open BCHBCTypes +open BCHLibTypes + +val convert_semantics_to_attributes: function_info_int -> b_attributes_t diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index e8558452e..de241f64f 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -5740,8 +5740,6 @@ object (** Returns the object containing all active proof obligations.*) method proofobligations: proofobligations_int - method convert_preconditions_to_attributes: b_attributes_t - (** {1 Function invariants} *) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 57195dd98..4f824b879 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -326,7 +326,9 @@ object (self) fname resolvents in let (regtypes, _) = resolvents in let attrs = List.concat (List.map (fun (_, _, a) -> a) regtypes) in - let attrs = (finfo#convert_preconditions_to_attributes) @ attrs in + let attrs = + (BCHFunctionSemanticsAttributes.convert_semantics_to_attributes finfo) + @ attrs in BCHBCFiles.bcfiles#add_fundef ~attrs fname ftype); node#setAttribute "a" faddr; From 8d591de828e91dd4ce4b07aebe9d509217cb1678 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 16 May 2026 11:22:37 -0700 Subject: [PATCH 13/15] CHB: update sprintf summaries --- CodeHawk/CHB/bchsummaries/so_functions/snprintf.xml | 10 ++++++++++ CodeHawk/CHB/bchsummaries/so_functions/sprintf.xml | 10 ++++++++++ CodeHawk/CHB/bchsummaries/so_functions/system.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/vsnprintf.xml | 10 ++++++++++ CodeHawk/CHB/bchsummaries/so_functions/vsprintf.xml | 9 +++++++++ 5 files changed, 40 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CHB/bchsummaries/so_functions/snprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/snprintf.xml index 8cd8981a1..b672bc415 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/snprintf.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/snprintf.xml @@ -102,6 +102,16 @@ + + + + + buffer + format + count + + + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/sprintf.xml index 5e4199362..bb3d1681c 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/sprintf.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/sprintf.xml @@ -68,6 +68,16 @@ + + + + + buffer + format + + + + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/system.xml b/CodeHawk/CHB/bchsummaries/so_functions/system.xml index 44dbe7522..912fd8030 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/system.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/system.xml @@ -36,7 +36,7 @@ 
         
           
-            
+            
             command
           
         
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/vsnprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/vsnprintf.xml
index 5493437bc..bd4a42b12 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/vsnprintf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/vsnprintf.xml
@@ -98,6 +98,16 @@
 	  
 	
       
+      
+        
+          
+            
+            buffer
+            format
+            count
+          
+        
+      
     
    
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/vsprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/vsprintf.xml
index 0076e2aa1..8575e4d65 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/vsprintf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/vsprintf.xml
@@ -82,6 +82,15 @@
 	  
 	
       
+      
+        
+          
+            
+            buffer
+            format
+          
+        
+      
     
    
   

From 049e8f6340e1ebdab394ec73e30d17c53779f3b7 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Sat, 16 May 2026 11:25:37 -0700
Subject: [PATCH 14/15] CHB: add format arguments to trusted-os-cmd-fmt-string
 po

---
 CodeHawk/CH/chutil/cHUtil.ml                  |  11 ++
 CodeHawk/CH/chutil/cHUtil.mli                 |   9 +-
 .../CHB/bchlib/bCHCallSemanticsRecorder.ml    |  14 +-
 CodeHawk/CHB/bchlib/bCHFloc.ml                | 133 +++++++++++++++++-
 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml |  14 +-
 CodeHawk/CHB/bchlib/bCHLibTypes.mli           |  18 ++-
 CodeHawk/CHB/bchlib/bCHXPODictionary.ml       |  31 +++-
 CodeHawk/CHB/bchlib/bCHXPOPredicate.ml        |   6 +-
 .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml  |  21 ++-
 9 files changed, 243 insertions(+), 14 deletions(-)

diff --git a/CodeHawk/CH/chutil/cHUtil.ml b/CodeHawk/CH/chutil/cHUtil.ml
index 3ebcff706..df6f6f220 100644
--- a/CodeHawk/CH/chutil/cHUtil.ml
+++ b/CodeHawk/CH/chutil/cHUtil.ml
@@ -174,6 +174,17 @@ let list_split_p (p:'a -> bool) (l:'a list):('a list * 'a list) =
   loop [] [] l
 
 
+let list_slice (lst: 'a list) (index: int) (count:int): 'a list option  =
+  if index < 0 || count < 0 || (List.length lst) < index + count then
+    None
+  else
+    let rec aux l i n result =
+      if i > 0 then aux (List.tl l) (i-1) n result
+      else if n > 0 then aux (List.tl l) 0 (n-1) ((List.hd l) :: result)
+      else List.rev result in
+    Some (aux lst index count [])
+
+
 let list_suffix (n:int) (l:'a list) =
   let rec aux n l =
     match l with
diff --git a/CodeHawk/CH/chutil/cHUtil.mli b/CodeHawk/CH/chutil/cHUtil.mli
index d475af20d..b2a0fb699 100644
--- a/CodeHawk/CH/chutil/cHUtil.mli
+++ b/CodeHawk/CH/chutil/cHUtil.mli
@@ -60,6 +60,13 @@ val list_split_p: ('a -> bool) -> 'a list -> ('a list * 'a list)
 
 val list_sub: 'a list -> int -> int -> 'a list
 
+(** [list_slice lst index count] returns a list of [count] elements from [st]
+    starting at [index] (counting from zero).
+
+    Returns None if [index] or [count] are negative, or if [lst] does not
+    include sufficient elements to fill the slice. *)
+val list_slice: 'a list -> int -> int -> 'a list option
+
 val list_suffix: int -> 'a list -> 'a list
 
 val list_maxf: 'a list -> ('a -> 'a -> int) -> 'a
@@ -84,7 +91,7 @@ val pair_compare:
   ('a * 'b) -> ('a * 'b) -> ('a -> 'a -> int) -> ('b -> 'b -> int) -> int
 
 
-  (** [triple_compare t1 t2 returns the result of the element-wise comparison
+  (** [triple_compare t1 t2] returns the result of the element-wise comparison
       of triples [t1] and [t2], using [f1], [f2], and [f3] as comparison
       functions for the three elements, respectively.*)
 val triple_compare:
diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
index 062cdd372..1c9269d2c 100644
--- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
+++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
@@ -174,7 +174,19 @@ object (self)
     | _ -> Open
 
   method record_precondition (pre: xxpredicate_t) =
-    let xpo = xxp_to_xpo_predicate self#termev self#loc pre in
+    let xpo =
+      match pre with
+      | XXTrustedOsCmdFmtString (fmt, FMT_ARGS, _optlen) ->
+         (match xxp_to_xpo_predicate self#termev self#loc pre with
+          | XPOTrustedOsCmdFmtString (xfmt, xkind, xoptlen, []) as xpre ->
+             let fmtargs = self#termev#get_annotated_format_arguments fmt in
+             (match fmtargs with
+              | Some fmtargs ->
+                 XPOTrustedOsCmdFmtString (xfmt, xkind, xoptlen, fmtargs)
+              | _ -> xpre)
+          | xpre -> xpre)
+      | _ ->
+         xxp_to_xpo_predicate self#termev self#loc pre in
     let status = self#simplify_precondition xpo in
     let _ =
       log_diagnostics_result
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index 062dd5ab4..7f46de515 100644
--- a/CodeHawk/CHB/bchlib/bCHFloc.ml
+++ b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -276,7 +276,9 @@ class default_bterm_evaluator_t
 object
 
   method finfo = finfo
+  method is_format_string (_t: bterm_t) = false
   method bterm_xpr (_t: bterm_t) = None
+  method get_annotated_format_arguments (_t: bterm_t) = None
   method xpr_local_stack_address (_x: xpr_t) = None
   method bterm_stack_address (_t: bterm_t) = None
   method constant_bterm (_t: bterm_t) = None
@@ -296,6 +298,24 @@ object (self)
 
   method finfo = finfo
 
+  method is_format_string (t: bterm_t): bool =
+    match t with
+    | ArgValue par ->
+       let cpar_o =
+         List.fold_left (fun acc (cpar, _) ->
+             match acc with
+             | Some _ -> acc
+             | _ ->
+                if (fts_parameter_equal cpar par) then Some cpar else None)
+           None callargs in
+       (match cpar_o with
+        | Some cpar ->
+           (match cpar.apar_fmt with
+            | NoFormat -> false
+            | _ -> true)
+        | _ -> false)
+    | _ -> false
+
   method bterm_xpr (t: bterm_t): xpr_t option =
     match t with
     | ArgValue par ->
@@ -317,6 +337,97 @@ object (self)
         | _ -> None)
     | _ -> None
 
+  method private argument_index (t: bterm_t): int option =
+    match t with
+    | ArgValue par ->
+       let cpar_o =
+         List.fold_left (fun acc (cpar, _) ->
+             match acc with
+             | Some _ -> acc
+             | _ ->
+                if (fts_parameter_equal cpar par) then Some cpar else None)
+           None callargs in
+       (match cpar_o with
+        | Some cpar -> cpar.apar_index
+        | _ -> None)
+    | _ -> None
+
+  method get_annotated_format_arguments
+           (t: bterm_t): annotated_format_arg_t list option =
+    match self#argument_index t with
+    | None ->
+       begin
+         log_diagnostics_result
+           ~tag:"get_annotated_format_arguments"
+           ~msg:finfo#get_name
+           __FILE__ __LINE__
+           ["Unable to determine index of the bterm: " ^ (bterm_to_string t)];
+         None
+       end
+    | Some index ->    (* 1-based index in the parameter list *)
+       match self#bterm_xpr t with
+       | None ->
+          begin
+            log_diagnostics_result
+              ~tag:"get_annotated_format_arguments"
+              ~msg:finfo#get_name
+              __FILE__ __LINE__
+              ["Unable to resolve bterm: " ^ (bterm_to_string t)];
+            None
+          end
+       | Some xpr ->
+          match xpr with
+          | XConst (IntConst n) ->
+             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
+               let fmtspec =
+                 CHFormatStringParser.parse_formatstring fmtstring false in
+               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_error_result
+                       ~tag:"get_annotated_format_arguments"
+                       ~msg:finfo#get_name
+                       __FILE__ __LINE__
+                       ["Error in retrieving format arguments from call arguments";
+                        "fmtspec count: " ^ (string_of_int (List.length argspecs));
+                        "argxprs count: " ^ (string_of_int (List.length argxprs))];
+                     None
+                   end)
+             else
+               begin
+                 log_error_result
+                   ~tag:"get_annotated_format_arguments"
+                   ~msg:finfo#get_name
+                   __FILE__ __LINE__
+                   ["No constant format string found in string table"];
+                 None
+               end
+          | _ ->
+             begin
+               log_diagnostics_result
+                 ~tag:"get_annotated_format_arguments"
+                 ~msg:finfo#get_name
+                 __FILE__ __LINE__
+                 ["Unable to retrieve format string from non-constant xpr: "
+                  ^ (x2s xpr)];
+               None
+             end
+
   method xpr_local_stack_address (x: xpr_t): int option =
     match x with
     | XOp (XMinus, [XVar v; XConst (IntConst n)]) when n#geq numerical_zero ->
@@ -381,6 +492,24 @@ object (self)
 
   method finfo = finfo
 
+  method is_format_string (t: bterm_t): bool =
+    match t with
+    | ArgValue par ->
+       let cpar_o =
+         List.fold_left (fun acc (cpar, _) ->
+             match acc with
+             | Some _ -> acc
+             | _ ->
+                if (fts_parameter_equal cpar par) then Some cpar else None)
+           None callargs in
+       (match cpar_o with
+        | Some cpar ->
+           (match cpar.apar_fmt with
+            | NoFormat -> false
+            | _ -> true)
+        | _ -> false)
+    | _ -> false
+
   method bterm_xpr (t: bterm_t): xpr_t option =
     match t with
     | ArgValue par ->
@@ -402,6 +531,8 @@ object (self)
         | _ -> None)
     | _ -> None
 
+  method get_annotated_format_arguments (_t: bterm_t) = None
+
   method xpr_local_stack_address (x: xpr_t): int option =
     match x with
     | XOp (XMinus, [XVar v; XConst (IntConst n)]) when n#geq numerical_zero ->
@@ -3211,7 +3342,7 @@ object (self)
              | _ ->
                 begin
                   log_diagnostics_result
-                    ~tag:"evaluate_fts_address_argument"
+                    ~tag:"evaluate_fts_address_argument:no stackslot found"
                     ~msg:(p2s self#l#toPretty)
                     __FILE__ __LINE__
                     ["parameter: " ^ (fts_parameter_to_string p);
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
index 49258723e..50f3f6e39 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -231,8 +231,12 @@ let trusted_os_cmd_string_delegate_local_instr
                          match optlen with
                          | Some len -> btermev#bterm_xpr len
                          | _ -> None in
+                       let fmtargs =
+                         match btermev#get_annotated_format_arguments src with
+                         | Some fmtargs -> fmtargs
+                         | _ -> [] in
                        let new_xpo =
-                         XPOTrustedOsCmdFmtString (srcptr, fmtkind, xlen) in
+                         XPOTrustedOsCmdFmtString (srcptr, fmtkind, xlen, fmtargs) in
                        let _ =
                          finfo#proofobligations#add_proofobligation
                            floc#l#ci new_xpo Open in
@@ -322,8 +326,7 @@ let trusted_os_cmd_fmt_string_va_list_delegate
      (match xpxt#xpr_to_bterm BCHBCTypeUtil.t_charptr x with
       | Some xfmt ->
          let xpred = XXTrustedOsCmdFmtString (xfmt, FMT_ARGS, xoptlen) in
-         let updatedsummary = finfo#get_summary#add_precondition xpred in
-         let _ = finfo#update_summary updatedsummary in
+         let _ = finfo#add_precondition xpred in
          Delegated (xpred)
       | _ -> Open)
   | _ -> Open
@@ -342,7 +345,8 @@ let discharge_trusted_os_cmd_fmt_string
        (match kind with
         | VA_LIST ->
            trusted_os_cmd_fmt_string_va_list_delegate finfo loc x optlen
-        | _ -> Open)
+        | FMT_ARGS -> status)
+        (* trusted_os_cmd_fmt_string_fmt_args_delegate_local finfo loc x optlen) *)
     | _ -> status in
   match status with
   | Open ->
@@ -963,7 +967,7 @@ let discharge_one
   | XPOTrustedOsCmdString x ->
      discharge_trusted_os_cmd_string finfo po#loc x
 
-  | XPOTrustedOsCmdFmtString (x, kind, optlen) ->
+  | XPOTrustedOsCmdFmtString (x, kind, optlen, _) ->
      discharge_trusted_os_cmd_fmt_string finfo po#loc x kind optlen
 
   | XPOOutputFormatString x ->
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index de241f64f..1b21b353d 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -2592,6 +2592,10 @@ object ('a)
 end
 
 
+type annotated_format_arg_t =
+  CHFormatStringParser.conversion_t * CHFormatStringParser.fieldwidth_t * xpr_t
+
+
 (** Instantiated xxpredicate (or other condition) with expressions in the
     context of a function (proof obligation that can be discharged against
     invariants).*)
@@ -2628,7 +2632,8 @@ type xpo_predicate_t =
   | XPOTainted of xpr_t
   | XPOTrustedString of xpr_t
   | XPOTrustedOsCmdString of xpr_t
-  | XPOTrustedOsCmdFmtString of xpr_t * format_args_kind_t * xpr_t option
+  | XPOTrustedOsCmdFmtString of
+      xpr_t * format_args_kind_t * xpr_t option * annotated_format_arg_t list
   | XPOTrustedOsCmdFmtArgString of xpr_t * quote_status_t * int option
   | XPOWritesStringFromFmtString of xpr_t * xpr_t * format_args_kind_t * xpr_t option
   | XPOValidMem of xpr_t
@@ -6200,6 +6205,7 @@ class type expression_externalizer_int =
 
   end
 
+
 (** Evaluator of terms used in a particular function call.*)
 class type bterm_evaluator_int =
   object
@@ -6207,10 +6213,20 @@ class type bterm_evaluator_int =
     (** Return the function info in which context the term is to be evaluated.*)
     method finfo: function_info_int
 
+    (** [is_format_string t] returns true if t represents a parameter and that
+        parameter is used as a format string. *)
+    method is_format_string: bterm_t -> bool
+
     (** [bterm_xpr t] returns the expression with which [t] was instantiated
         in the call.*)
     method bterm_xpr: bterm_t -> xpr_t option
 
+    (** [get_format_arguments t] returns a list of (converter, xpr) pairs that
+        are the format arguments associated with the format string denoted by
+        [t]. If [t] does not denote a format string, None is returned.*)
+    method get_annotated_format_arguments:
+             bterm_t -> annotated_format_arg_t list option
+
     (** [xpr_local_stack_address x] returns the stack offset (from the initial
         value of the stack pointer at function entry) if [x] is a stack address
         and None otherwise.*)
diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml
index 5df224d9c..478bf4947 100644
--- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml
@@ -26,6 +26,7 @@
    ============================================================================= *)
 
 (* chutil *)
+open CHFormatStringParser
 open CHIndexTable
 open CHXmlDocument
 
@@ -46,12 +47,14 @@ class xpodictionary_t (xd: xprdictionary_int): xpodictionary_int =
 object (self)
 
   val xd = xd
+  val format_arg_table = mk_index_table "format-arg-table"
   val xpo_predicate_table = mk_index_table "xpo-predicate-table"
 
   val mutable tables = []
 
   initializer
     tables <- [
+      format_arg_table;
       xpo_predicate_table
     ]
 
@@ -62,6 +65,29 @@ object (self)
 
   method xd = xd
 
+  method private index_format_arg (c, fw, x) =
+    let conversion_tag =
+      match c with
+      | IntConverter -> "int"
+      | DecimalConverter -> "decimal"
+      | UnsignedOctalConverter -> "unsigned-octal"
+      | UnsignedDecimalConverter -> "unsigned-decimal"
+      | UnsignedHexConverter _ -> "unsigned-hex"
+      | FixedDoubleConverter _ -> "fixed-double"
+      | ExpDoubleConverter _ -> "exp-double"
+      | FlexDoubleConverter _ -> "flex-double"
+      | HexDoubleConverter _ -> "hex-double"
+      | UnsignedCharConverter -> "unsigned-char"
+      | StringConverter -> "string"
+      | PointerConverter -> "pointer"
+      | OutputArgument -> "output-argument" in
+    let fieldwidth_tag =
+      match fw with
+      | FieldwidthConstant n -> string_of_int n
+      | _ -> "other" in
+    let key = ([conversion_tag; fieldwidth_tag], [self#xd#index_xpr x]) in
+    format_arg_table#add key
+
   method index_xpo_predicate (xpo: xpo_predicate_t) =
     let tags = [xpo_predicate_mcts#ts xpo] in
     let ib b = if b then 1 else 0 in
@@ -103,8 +129,9 @@ object (self)
       | XPOTainted x -> (tags, [ix x])
       | XPOTrustedString x -> (tags, [ix x])
       | XPOTrustedOsCmdString x -> (tags, [ix x])
-      | XPOTrustedOsCmdFmtString (x, kind, optlen) ->
-         (tags @ [format_args_kind_mfts#ts kind], [ix x; optix optlen])
+      | XPOTrustedOsCmdFmtString (x, kind, optlen, fmtargs) ->
+         (tags @ [format_args_kind_mfts#ts kind],
+          [ix x; optix optlen] @ (List.map self#index_format_arg fmtargs))
       | XPOTrustedOsCmdFmtArgString (x, quotes, optlen) ->
          (tags @ [quote_status_mfts#ts quotes], [ix x; ioptlen optlen])
       | XPOWritesStringFromFmtString (x1, x2, kind, optlen) ->
diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml
index 3bb4654b2..e102add38 100644
--- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml
+++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml
@@ -98,7 +98,7 @@ let rec xxp_to_xpo_predicate
   | XXTrustedString t -> XPOTrustedString (btx t)
   | XXTrustedOsCmdString t -> XPOTrustedOsCmdString (btx t)
   | XXTrustedOsCmdFmtString (t, fmtargs, optlen) ->
-     XPOTrustedOsCmdFmtString (btx t, fmtargs, optbtx optlen)
+     XPOTrustedOsCmdFmtString (btx t, fmtargs, optbtx optlen, [])
   | XXTrustedOsCmdFmtArgString (t, quotes, optlen) ->
      XPOTrustedOsCmdFmtArgString (btx t, quotes, optlen)
   | XXWritesStringFromFmtString (dest, fmt, fmtargs, optlen) ->
@@ -182,7 +182,7 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) =
   | XPOTainted t -> default "tainted" [t]
   | XPOTrustedString t -> default "trusted-string" [t]
   | XPOTrustedOsCmdString t -> default "trusted-os-cmd-string" [t]
-  | XPOTrustedOsCmdFmtString (t, kind, optlen) ->
+  | XPOTrustedOsCmdFmtString (t, kind, optlen, fmtargs) ->
      LBLOCK [
          STR "trusted-os-cmd-fmt-string(";
          x2p t;
@@ -190,6 +190,8 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) =
          STR (format_args_kind_to_string kind);
          STR ", ";
          (match optlen with Some i -> x2p i | _ -> STR "_");
+         STR ", ";
+         INT (List.length fmtargs);
          STR ")"]
   | XPOTrustedOsCmdFmtArgString (t, quotes, optlen) ->
      LBLOCK [
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
index a5be04498..841106529 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -733,6 +733,17 @@ let translate_arm_instruction
                         let _ = log_dc_error_result __FILE__ __LINE__ e in
                         [])
                       (floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
+
+            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
+                 created for the buffer at this stack address.
+
+                 To be done in a better way, eventually. *)
+              let xx = rewrite_expr floc x in
+              let _ = floc#get_var_at_address ~btype:(ptr_deref ptype) xx in
+              []
             else
               [] in
           if is_register_parameter p then
@@ -771,7 +782,15 @@ let translate_arm_instruction
           | XXBlockWrite (_, dest, _) ->
              (match floc#evaluate_summary_address_term dest with
               | Some memVar -> (memVar :: accdefs, accuse, accusehigh)
-              | _  -> (accdefs, accuse, accusehigh))
+              | _ ->
+                 begin
+                   log_diagnostics_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)
+                 end)
           | XXBuffer (_, dest, _) ->
              (match floc#evaluate_summary_address_term dest with
               | Some memVar -> (accdefs, memVar :: accuse, memVar :: accusehigh)

From 4ae5796f1dc421ec0ea7b91ce687583502bc7dc1 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Mon, 25 May 2026 00:06:22 -0700
Subject: [PATCH 15/15] CHB:PO: delegate BlockWrite without external length
 term

---
 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 72 +++++++++----------
 1 file changed, 33 insertions(+), 39 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
index 50f3f6e39..16e4d1b06 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -499,49 +499,43 @@ let blockwrite_delegate
        Open
      end
   | Some xprxt ->
+     let xlenterm =
+       (* If the destination is external, but the length term cannot be
+          externalized, an external predicate is created with a runtime
+          value argument for its length. The rationale for still
+          delegating this proof obligation is that communicating that
+          this function writes to an external buffer takes priority over
+          having an incomplete predicate, as the writing affects the
+          semantics of the caller. *)
+       match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with
+       | Some bterm -> bterm
+       | _ -> RunTimeValue in
      (match xprxt#xpr_to_bterm ty xpr with
       | Some (NumConstant n) when n#gt CHNumerical.numerical_zero ->
          let dw = BCHDoubleword.numerical_mod_to_doubleword n in
-         (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with
-          | Some (NumConstant ns) ->
-             let xxp = XXBlockWrite (ty, NumConstant n, NumConstant ns) in
-             begin
-               global_system_state#add_precondition dw loc xxp;
-               log_diagnostics_result
-                 ~tag:"blockwrite_delegate:delegate_global"
-                 ~msg:(p2s loc#toPretty)
-                 __FILE__ __LINE__
-                 ["dw: " ^ dw#to_hex_string;
-                  "xxp: " ^ (p2s (xxpredicate_to_pretty xxp))];
-               DelegatedGlobal (dw, xxp)
-             end
-          | _ ->
-             begin
-               log_diagnostics_result
-                 ~tag:"blockwrite_delegate:delegate_global:open"
-                 ~msg:(p2s loc#toPretty)
-                 __FILE__ __LINE__
-                 ["dw: " ^ dw#to_hex_string; "bwlen: " ^ (x2s bwlen)];
-               Open
-             end)
+         let xxp = XXBlockWrite (ty, NumConstant n, xlenterm) in
+         begin
+           global_system_state#add_precondition dw loc xxp;
+           log_diagnostics_result
+             ~tag:"blockwrite_delegate:delegate_global"
+             ~msg:(p2s loc#toPretty)
+             __FILE__ __LINE__
+             ["dw: " ^ dw#to_hex_string;
+              "xxp: " ^ (p2s (xxpredicate_to_pretty xxp))];
+           DelegatedGlobal (dw, xxp)
+         end
       | Some dst ->
-         (match xprxt#xpr_to_bterm BCHBCTypeUtil.t_int bwlen with
-          | Some lenterm ->
-             let xpred = XXBlockWrite (ty, dst, lenterm) in
-             begin
-               finfo#add_precondition xpred;
-               finfo#add_sideeffect xpred;
-               Delegated xpred
-             end
-          | _ ->
-             begin
-               log_diagnostics_result
-                 ~tag:"blockwrite_delegate:dest:open"
-                 ~msg:(p2s loc#toPretty)
-                 __FILE__ __LINE__
-                 ["dst: " ^ (BCHBTerm.bterm_to_string dst); "bwlen: " ^ (x2s bwlen)];
-               Open
-             end)
+         let xpred = XXBlockWrite (ty, dst, xlenterm) in
+         begin
+           finfo#add_precondition xpred;
+           finfo#add_sideeffect xpred;
+           log_diagnostics_result
+             ~tag:"blockwrite_delegate:delegate_api_sideeffect"
+             ~msg:(p2s loc#toPretty)
+             __FILE__ __LINE__
+             ["xpred: " ^ (p2s (xxpredicate_to_pretty xpred))];
+           Delegated xpred
+         end
       | _ ->
          begin
            log_diagnostics_result