Merge branch 'master' into outputparameters

Author: sipma

CodeHawk/CH/chutil/cHUtil.ml

@@ -261,6 +261,37 @@ let list_compare_r (l1: 'a list) (l2: 'b list) (f: 'a -> 'b -> int): int =
       (fun e1 e2 a -> if a = 0 then (f e1 e2) else a) l1 l2 0
 
 
+let pair_compare
+      (p1: ('a * 'b))
+      (p2: ('a * 'b))
+      (f1: 'a -> 'a -> int)
+      (f2: 'b -> 'b -> int): int =
+  let l0 = f1 (fst p1) (fst p2) in
+  if l0 = 0 then
+    f2 (snd p1) (snd p2)
+  else
+    l0
+
+
+let triple_compare
+      (p1: ('a * 'b * 'c))
+      (p2: ('a * 'b * 'c))
+      (f1: 'a -> 'a -> int)
+      (f2: 'b -> 'b -> int)
+      (f3: 'c -> 'c -> int) =
+  let (x1, y1, z1) = p1 in
+  let (x2, y2, z2) = p2 in
+  let l0 = f1 x1 x2 in
+  if l0 = 0 then
+    let l1 = f2 y1 y2 in
+    if l1 = 0 then
+      f3 z1 z2
+    else
+      l1
+  else
+    l0
+
+
   (* Compares to optional values, with the Some value smaller than None,
      two None values are considered equal, and otherwise the provided
      function decides *)

CodeHawk/CH/chutil/cHUtil.mli

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 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
@@ -76,6 +76,26 @@ val list_compare: 'a list -> 'a list -> ('a -> 'a -> int) -> int
     and [lst2] starting from the last element.*)
 val list_compare_r: 'a list -> 'a list -> ('a -> 'a -> int) -> int
 
+
+(** [pair_compare p1 p2 f1 f2] returns the result of the element-wise comparison
+    of pairs [p1] and [p2] using [f1] and [f2] as comparison function for the
+    first and second element of the pair respectively.*)
+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
+      of triples [t1] and [t2], using [f1], [f2], and [f3] as comparison
+      functions for the three elements, respectively.*)
+val triple_compare:
+    ('a * 'b * 'c)
+  -> ('a * 'b * 'c)
+  -> ('a -> 'a -> int)
+  -> ('b -> 'b -> int)
+  -> ('c -> 'c -> int)
+  -> int
+
+
 val list_union_f: 'a list -> 'a list -> ('a -> 'a -> bool) -> 'a list
 
 val list_difference: 'a list -> 'a list -> ('a -> 'a -> bool) -> 'a list

CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml

@@ -87,6 +87,9 @@ open BCHTrace
 module TR = CHTraceResult
 
 
+let p2s = CHPrettyUtil.pretty_to_string
+
+
 let analyze_all = ref false
 let maxrelationalvarcomplexity = ref 150000.0
 let maxrelationalloopcomplexity = ref 2000
@@ -568,14 +571,12 @@ let analyze_arm starttime =
   let failedfunctions = ref [] in
   let functionfailure (failuretype: string) (faddr: doubleword_int) (p: pretty_t) =
     begin
-      ch_error_log#add
-        "function failure"
-        (LBLOCK [
-             STR failuretype;
-             STR ". ";
-             faddr#toPretty;
-             STR ": ";
-             p]);
+      log_error_result
+        ~tag:"analyze_arm:functionfailure"
+        ~msg:faddr#to_hex_string
+        __FILE__ __LINE__
+        ["failure-type: " ^ failuretype;
+         "error: " ^ (p2s p)];
       if system_settings#fail_on_function_failure then
         raise
           (BCH_failure

CodeHawk/CHB/bchanalyze/bCHTrace.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2025 Aarno Labs LLC
+   Copyright (c) 2021-2026 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -159,7 +159,7 @@ let rec _trace_fwd faddr op =
         let call_args = callee#get_call_args in
         List.iter (fun (p,e) ->
 	    match p.apar_location with
-	    | [StackParameter (par, _)] ->
+	    | [StackParameter (par, _, _)] ->
 	       let argIndices = get_xarg_indices finfo e in
 	       if List.mem op argIndices then
 	         begin

CodeHawk/CHB/bchcil/bCHParseCilFile.ml

@@ -87,6 +87,11 @@ let parse_cil_file ?(computeCFG=true) ?(removeUnused=true) (filename: string) =
            NL];
        exit 1
      end
+  | CHCommon.CHFailure p ->
+     begin
+       pr_debug [STR "Error when parsing "; STR filename; STR ": "; p; NL];
+       exit 1
+     end
   | e ->
      begin
        pr_debug [STR "Error when parsing (other exception): "; STR filename; NL];

CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml

@@ -142,6 +142,9 @@ let speclist =
     ("-collectdata", Arg.Unit (fun () -> system_settings#set_collect_data),
      "analyze all functions, create ssa variables (if enabled), and "
      ^ " create stacklayouts and proof obligations");
+    ("-construct_signatures",
+     Arg.Unit (fun () -> system_settings#set_construct_signatures),
+     "create function signatures based on parameter inference");
     ("-no_varinvs", Arg.Unit (fun () -> system_settings#set_no_varinvs),
      "do not generate variable invariants");
     ("-stream", Arg.Unit (fun () -> cmd := "stream"),
@@ -888,6 +891,7 @@ let main () =
       let _ =
         if (List.length system_info#ifiles > 0) then
           pr_timing [STR "c header files parsed"] in
+      let _ = BCHBCTypeXml.register_ch_named_struct_types () in
       (* function annotations in userdata should be loaded after the header
          files are parsed, so types in the function annotations can be resolved.*)
       let _ = system_info#initialize_function_annotations in

CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml

@@ -80,14 +80,14 @@ let speclist = [
 
 let ccNode =
   xml_string
-    "copyright-notice" "Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304"
+    "copyright-notice" "Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304"
 
 let usage_msg = "mktemplate name"
 let read_args () = Arg.parse speclist (fun s -> name := s) usage_msg
 
 let post_shortcuts = [
   "notzero-zero"; "nonzero-zero"; "one-zero"; "zero-negone";
-  "notnull"; "notnull-null";
+  "notnull"; "notnull-null"; "nonnegative-negone";
   "nonnegative-negative"; "positive-nonpositive"; "positive-zero"]
 
 

CodeHawk/CHB/bchlib/Makefile

@@ -100,13 +100,13 @@ MLIS := \
 	bCHSystemInfo \
 	bCHXPODictionary \
 	bCHCallTargetInfo \
+	bCHXPOPredicate \
 	bCHProofObligations \
 	bCHFunctionStackframe \
 	bCHFunctionInfo \
 	bCHMakeCallTargetInfo \
 	bCHGlobalState \
 	bCHMemoryRecorder \
-	bCHXPOPredicate \
 	bCHCallSemanticsRecorder \
 	bCHFloc \
 	bCHCallgraph \
@@ -144,10 +144,6 @@ SOURCES := \
 	bCHInvDictionary \
 	bCHVarInvDictionary \
 	bCHTypeDefinitions \
-	bCHTypeConstraintDictionary \
-	bCHTypeConstraintUtil \
-	bCHTypeConstraintGraph \
-	bCHTypeConstraintStore \
 	bCHJavaSignatures \
 	bCHVariableNames \
 	bCHCodegraph \
@@ -164,8 +160,12 @@ SOURCES := \
 	bCHFtsParameter \
 	bCHARMFunctionInterface \
 	bCHMIPSFunctionInterface \
-	bCHFunctionInterface \
 	bCHBTerm \
+	bCHTypeConstraintDictionary \
+	bCHTypeConstraintUtil \
+	bCHTypeConstraintGraph \
+	bCHTypeConstraintStore \
+	bCHFunctionInterface \
 	bCHFunctionStub \
 	bCHCallTarget \
 	bCHCStructConstant \
@@ -192,13 +192,13 @@ SOURCES := \
 	bCHSystemInfo \
 	bCHXPODictionary \
 	bCHCallTargetInfo \
+	bCHXPOPredicate \
 	bCHProofObligations \
 	bCHFunctionStackframe \
 	bCHFunctionInfo \
 	bCHMakeCallTargetInfo \
 	bCHGlobalState \
 	bCHMemoryRecorder \
-	bCHXPOPredicate \
 	bCHCallSemanticsRecorder \
 	bCHFloc \
 	bCHCallgraph \
@@ -232,7 +232,7 @@ clean:
 	rm -f *.cmxa
 	rm -f *.ml~
 	rm -f *.mli~
-	rm -f Makefile~ 
+	rm -f Makefile~
 	rm -f bchlib.cmxa
 	rm -rf doc
 

CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml

@@ -677,13 +677,13 @@ let get_arm_format_spec_parameters
     List.fold_left
       (fun aas p ->
         match p.apar_location with
-        | [RegisterParameter (ARMRegister r, _)] ->
+        | [RegisterParameter (ARMRegister r, _, _)] ->
            update_core_reg aas r
-        | [RegisterParameter (ARMDoubleRegister (r1, r2), _)] ->
+        | [RegisterParameter (ARMDoubleRegister (r1, r2), _, _)] ->
            update_core_double_reg aas r1 r2
-        | [RegisterParameter (ARMExtensionRegister r, _)] ->
+        | [RegisterParameter (ARMExtensionRegister r, _, _)] ->
            update_extension_reg aas r
-        | [StackParameter (offset, pld)] ->
+        | [StackParameter (offset, pld, _)] ->
            update_stack_offset aas offset pld.pld_size
         | _ ->
            raise

CodeHawk/CHB/bchlib/bCHBCAttributes.ml

@@ -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
@@ -88,17 +88,27 @@ let convert_b_attributes_to_function_conditions
             | [ACons (("write_only" | "read_write"), []); AInt refindex] ->
                let par = get_par refindex in
                let ty = get_derefty par in
-               ([XXBuffer (ty, ArgValue par, RunTimeValue)],
+               ([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)],
+               ([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
@@ -111,5 +121,72 @@ let convert_b_attributes_to_function_conditions
                  ([], [])
                end) in
          (pre @ xpre, side @ xside, xpost)
+      | Attr ("chk_pre", params) ->
+         let pre =
+           (match params with
+            | [ACons ("deref_read", []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBuffer (ty, ArgValue par, RunTimeValue)]
+
+            | [ACons ("deref_read", []); AInt refindex; AInt sizeindex] ->
+               let par1 = get_par refindex in
+               let par2 = get_par sizeindex in
+               let ty = get_derefty par1 in
+               [XXBuffer (ty, ArgValue par1, ArgValue par2)]
+
+            | [ACons ("deref_read", [AInt size]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               let c = CHNumerical.mkNumerical size in
+               [XXBuffer (ty, ArgValue par, NumConstant c)]
+
+            | [ACons ("deref_read", [ACons ("ntp", [])]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBuffer (ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))]
+
+            | [ACons ("deref_write", []); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXBlockWrite (ty, ArgValue par, RunTimeValue)]
+
+            | [ACons ("deref_write", []); AInt refindex; AInt sizeindex] ->
+               let par1 = get_par refindex in
+               let par2 = get_par sizeindex in
+               let ty = get_derefty par1 in
+               [XXBlockWrite (ty, ArgValue par1, ArgValue par2)]
+
+            | [ACons ("deref_write", [AInt size]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               let c = CHNumerical.mkNumerical size in
+               [XXBlockWrite (ty, ArgValue par, NumConstant c)]
+
+            | [ACons ("not_null", []); AInt refindex] ->
+               let par = get_par refindex in
+               [XXNotNull (ArgValue par)]
+
+            | [ACons ("null_terminated", []); AInt refindex] ->
+               let par = get_par refindex in
+               [XXNullTerminated (ArgValue par)]
+
+            | [ACons ("initialized_range", [ACons ("ntp", [])]); AInt refindex] ->
+               let par = get_par refindex in
+               let ty = get_derefty par in
+               [XXInitializedRange (
+                    ty, ArgValue par, ArgNullTerminatorPos (ArgValue par))]
+
+            | _ ->
+               begin
+                 log_error_result
+                   ~tag:"convert_b_attributes_to_function_conditions"
+                   ~msg:(name ^ ":chk_pre")
+                   __FILE__ __LINE__
+                   [String.concat ", " (List.map b_attrparam_to_string params)];
+                 []
+               end) in
+         (pre @ xpre, xside, xpost)
+
       | _ ->
          acc) ([], [], []) attrs