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/Makefile b/CodeHawk/CHB/bchlib/Makefile
index ac07914da..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 \
@@ -111,6 +111,8 @@ MLIS := \
bCHCallSemanticsRecorder \
bCHFloc \
bCHCallgraph \
+ bCHFunctionPODischarge \
+ bCHFunctionSemanticsAttributes \
bCHMetricsHandler \
bCHDisassemblySummary \
bCHMetrics \
@@ -175,7 +177,7 @@ SOURCES := \
bCHPrecondition \
bCHPostcondition \
bCHSideeffect \
- bCHBCAttributes \
+ bCHAttributesFunctionSemantics \
bCHFunctionSemantics \
bCHFunctionSummary \
bCHVariable \
@@ -204,6 +206,8 @@ SOURCES := \
bCHCallSemanticsRecorder \
bCHFloc \
bCHCallgraph \
+ bCHFunctionPODischarge \
+ bCHFunctionSemanticsAttributes \
bCHMetricsHandler \
bCHDisassemblySummary \
bCHMetrics \
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 964c9f2a5..000000000
--- a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml
+++ /dev/null
@@ -1,218 +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)
-
- | Attr (("format" | "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, [] , [])
-
- | 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)
-
- | _ ->
- acc) ([], [], []) 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 cd4431c34..1c9269d2c 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,6 +135,15 @@ object (self)
else
Open
| _ -> Open)
+ | XPOTrustedString x | XPOTrustedOsCmdString x ->
+ (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,73 +173,20 @@ object (self)
| _ -> Open)
| _ -> Open
- 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 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
@@ -239,23 +194,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 _ =
@@ -299,12 +238,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/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml
index c5abf9f33..b89044b9d 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,42 @@ 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 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
@@ -151,6 +188,29 @@ 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
+ | (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
@@ -198,6 +258,11 @@ 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]
+ | 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) ->
@@ -347,6 +412,36 @@ 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 -> default "trusted-os-cmd-string" [t]
+ | XXTrustedOsCmdFmtString (t, kind, optlen) ->
+ LBLOCK [
+ STR "trusted-os-cmd-fmt-string(";
+ btp t;
+ STR ", ";
+ 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 ->
pretty_print_list pl xxpredicate_to_pretty "[" " || " "]"
@@ -391,6 +486,14 @@ 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 -> 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 8b03af2f2..1168e5400 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,14 @@ 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 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/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index 2146f1709..7f46de515 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
@@ -237,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
@@ -257,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 ->
@@ -278,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 ->
@@ -342,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 ->
@@ -363,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 ->
@@ -442,7 +612,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
@@ -3153,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);
@@ -3381,6 +3570,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 +3713,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 +3850,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 +4010,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 b9cff4c11..73e579666 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,88 +1712,6 @@ object (self)
method proofobligations = proofobligations
- method discharge_proofobligations =
- let openpos = self#proofobligations#open_proofobligations in
- List.iter (fun po ->
- let newstatus =
- match po#xpo with
- | 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 set_instruction_bytes (ia:ctxt_iaddress_t) (b:string) =
H.add instrbytes ia b
@@ -2012,6 +1931,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/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/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
new file mode 100644
index 000000000..16e4d1b06
--- /dev/null
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -0,0 +1,1042 @@
+(* =============================================================================
+ 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 fmtargs =
+ match btermev#get_annotated_format_arguments src with
+ | Some fmtargs -> fmtargs
+ | _ -> [] in
+ let new_xpo =
+ XPOTrustedOsCmdFmtString (srcptr, fmtkind, xlen, fmtargs) 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 _ = finfo#add_precondition xpred 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
+ | FMT_ARGS -> status)
+ (* trusted_os_cmd_fmt_string_fmt_args_delegate_local finfo loc x optlen) *)
+ | _ -> 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 ->
+ 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
+ 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 ->
+ 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
+ ~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
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
index 25bb060ff..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
@@ -46,6 +46,7 @@ open BCHSideeffect
open BCHLibTypes
open BCHPostcondition
+let p2s = CHPrettyUtil.pretty_to_string
let id = BCHInterfaceDictionary.interface_dictionary
@@ -320,24 +321,31 @@ 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 _ =
- 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
@@ -361,6 +369,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/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/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml
index 6b1edf68b..95b85b6db 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
@@ -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
@@ -521,6 +523,15 @@ 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 -> (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) ->
@@ -541,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))
@@ -573,7 +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))
+ | "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 ea449c288..1b21b353d 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -2363,6 +2363,11 @@ type c_struct_constant_t =
| FieldCallTarget of call_target_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.*)
type xxpredicate_t =
@@ -2408,6 +2413,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 +2421,30 @@ 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
+ (** 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 *)
+
| XXDisjunction of xxpredicate_t list
| XXConditional of xxpredicate_t * xxpredicate_t
@@ -2564,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).*)
@@ -2598,6 +2630,12 @@ type xpo_predicate_t =
| XPOSetsErrno
| XPOStartsThread of xpr_t * xpr_t list
| XPOTainted of xpr_t
+ | XPOTrustedString of xpr_t
+ | XPOTrustedOsCmdString of xpr_t
+ | 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
| XPODisjunction of xpo_predicate_t list
| XPOConditional of xpo_predicate_t * xpo_predicate_t
@@ -3247,6 +3285,7 @@ type type_arg_mode_t =
| ArgDeallocate
| ArgFunctionPointer
| ArgScalarValue
+ | ArgOutputFormatString
type type_operation_kind_t =
@@ -5502,7 +5541,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} *)
@@ -5622,6 +5661,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
@@ -5705,10 +5745,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.*)
- method discharge_proofobligations: unit
-
(** {1 Function invariants} *)
@@ -5889,6 +5925,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}*)
@@ -6163,6 +6205,7 @@ class type expression_externalizer_int =
end
+
(** Evaluator of terms used in a particular function call.*)
class type bterm_evaluator_int =
object
@@ -6170,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.*)
@@ -6506,6 +6559,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/bCHPrecondition.ml b/CodeHawk/CHB/bchlib/bCHPrecondition.ml
index 489eecc3f..f51f81be1 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,9 @@ 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" -> [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
diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
index ca1415508..0a89b0d8a 100644
--- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
+++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
@@ -40,6 +40,19 @@ 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 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"
@@ -443,6 +456,11 @@ object
| XXSetsErrno -> "errno"
| XXStartsThread _ -> "st"
| XXTainted _ -> "t"
+ | XXTrustedString _ -> "ts"
+ | XXTrustedOsCmdString _ -> "tc"
+ | XXTrustedOsCmdFmtString _ -> "tfs"
+ | XXTrustedOsCmdFmtArgString _ -> "tfa"
+ | XXWritesStringFromFmtString _ -> "wfs"
| XXValidMem _ -> "v"
| XXDisjunction _ -> "dis"
| XXConditional _ -> "con"
@@ -451,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"; "v"; "x"
+ "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x"
]
end
@@ -496,6 +514,11 @@ object
| XPOSetsErrno -> "errno"
| XPOStartsThread _ -> "st"
| XPOTainted _ -> "t"
+ | XPOTrustedString _ -> "ts"
+ | XPOTrustedOsCmdString _ -> "tc"
+ | XPOTrustedOsCmdFmtString _ -> "tfs"
+ | XPOTrustedOsCmdFmtArgString _ -> "tfa"
+ | XPOWritesStringFromFmtString _ -> "wfs"
| XPOValidMem _ -> "v"
| XPODisjunction _ -> "dis"
| XPOConditional _ -> "con"
@@ -504,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"; "v"; "x"
+ "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x"
]
end
@@ -531,8 +554,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/bCHSumTypeSerializer.mli b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli
index a98e54b24..670d7f088 100644
--- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli
+++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli
@@ -37,6 +37,8 @@ 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 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/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 ->
diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml
index 4fd53751e..478bf4947 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
@@ -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,11 +65,36 @@ 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
+ 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])
@@ -99,6 +127,15 @@ 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 -> (tags, [ix x])
+ | 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) ->
+ (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 a8a3a3a5e..e102add38 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)
@@ -92,6 +95,14 @@ 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 -> 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)
@@ -169,6 +180,39 @@ 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-string" [t]
+ | XPOTrustedOsCmdString t -> default "trusted-os-cmd-string" [t]
+ | XPOTrustedOsCmdFmtString (t, kind, optlen, fmtargs) ->
+ LBLOCK [
+ STR "trusted-os-cmd-fmt-string(";
+ x2p t;
+ STR ", ";
+ 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 [
+ 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 ->
pretty_print_list pl xpo_predicate_to_pretty "[" " || " "]"
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
index 07099e5db..4f824b879 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
@@ -225,7 +225,7 @@ object (self)
mmap#write_xml_references faddr vard grNode;
(* self#write_xml_btypes bNode; *)
id#write_xml dNode;
- finfo#discharge_proofobligations;
+ BCHFunctionPODischarge.discharge_function_proofobligations finfo;
finfo#proofobligations#write_xml poNode;
finfo#xpod#write_xml xpodNode;
append [cNode; dNode; iiNode; jjNode; sfNode; grNode; xpodNode; poNode]
@@ -310,6 +310,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
@@ -320,13 +326,11 @@ object (self)
fname resolvents in
let (regtypes, _) = resolvents in
let attrs = List.concat (List.map (fun (_, _, a) -> a) regtypes) in
+ let attrs =
+ (BCHFunctionSemanticsAttributes.convert_semantics_to_attributes finfo)
+ @ 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
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
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..841106529 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 =
@@ -729,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
@@ -759,14 +774,52 @@ 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)
+ | _ ->
+ 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)
+ | _ -> (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
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;
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 @@
+
+
+
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 @@
+
+
+
+
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/system.xml b/CodeHawk/CHB/bchsummaries/so_functions/system.xml
index bfbbfdd3a..912fd8030 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/system.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/system.xml
@@ -32,7 +32,16 @@
-
+
+
+
+
+
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 @@
+
+
+
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 @@
+
+
+