Performance

CodeHawk/CH/chutil/cHLogger.ml

@@ -241,6 +241,19 @@ let log_error_result
     (LBLOCK [STR msg; STR (String.concat "; " error)])
 
 
+let log_error_result_default
+      ?(msg="")
+      ?(tag="")
+      (filename: string)
+      (linenumber: int)
+      (error: string list)
+      (defaultvalue: 'a): 'a =
+  begin
+    log_error_result ~msg ~tag filename linenumber error;
+    defaultvalue
+  end
+
+
 let log_result
       ?(msg="")
       ?(tag="")

CodeHawk/CH/chutil/cHLogger.mli

@@ -122,6 +122,10 @@ val log_error_result:
   ?msg:string -> ?tag:string -> string -> int -> string list -> unit
 
 
+val log_error_result_default:
+  ?msg:string -> ?tag:string -> string -> int -> string list -> 'c -> 'c
+
+
 (** [log_result msg tag filename linenumber error] writes an entry to
     [chlog] with a tag that combines [tag], [filename], and [linenumber].
     The entry is the concatenation of [msg] and the list of error messages

CodeHawk/CH/chutil/cHTiming.ml

@@ -124,11 +124,14 @@ end
 
 let progress_timer = new progress_timer_t
 
+let timing_enabled = ref true
+let disable_timing () = timing_enabled := false
 
 let pr_timing (l: pretty_t list) =
-  let pp = new pretty_printer_t stderr in
-  let timing = [STR "["; STR progress_timer#time_elapsed_str; STR "] "] in
-  pp#print (LBLOCK (timing @ l @ [NL]))
+  if !timing_enabled then
+    let pp = new pretty_printer_t stderr in
+    let timing = [STR "["; STR progress_timer#time_elapsed_str; STR "] "] in
+    pp#print (LBLOCK (timing @ l @ [NL]))
 
 
 let pr_interval_timing (l: pretty_t list) (interval: float) =

CodeHawk/CH/chutil/cHTiming.mli

@@ -44,6 +44,8 @@ end
 
 val mk_task_timer: unit -> timing_int
 
+val disable_timing: unit -> unit
+
 val pr_timing: pretty_t list -> unit
 
 val pr_interval_timing: pretty_t list -> float -> unit

CodeHawk/CH/chutil/cHTraceResult.ml

@@ -161,6 +161,23 @@ let tfold_list_fail
          | Ok v -> Ok (ok accv v)) initacc rl
 
 
+let tbind_iter_list (f: 'a -> unit traceresult) (args: 'a list): unit traceresult =
+  List.fold_left (fun acc_r a ->
+      match acc_r with
+      | Error _ -> acc_r
+      | _ -> f a) (Ok ()) args
+
+
+let tbind_map_list (f: 'a -> 'b traceresult) (args: 'a list): 'b list traceresult =
+  List.fold_left (fun acc_r a ->
+      match acc_r with
+      | Error _ -> acc_r
+      | Ok vl ->
+         match f a with
+         | Error e -> Error e
+         | Ok v -> Ok (vl @ [v])) (Ok []) args
+
+
 let to_bool (f: 'a -> bool) (r: 'a traceresult) =
   match r with
   | Ok v -> f v

CodeHawk/CH/chutil/cHTraceResult.mli

@@ -140,6 +140,12 @@ val tfold_list_fail:
   ('c -> 'a -> 'c) -> 'c traceresult -> ('a traceresult) list -> 'c traceresult
 
 
+val tbind_iter_list: ('a -> unit traceresult) -> 'a list -> unit traceresult
+
+
+val tbind_map_list: ('a -> 'b traceresult) -> 'a list -> 'b list traceresult
+
+
 (** [to_bool f r] is [f v] if [r] is [Ok v] and [false] otherwise.*)
 val to_bool: ('a -> bool) -> 'a traceresult -> bool
 

CodeHawk/CHC/cchanalyze/Makefile

@@ -61,6 +61,7 @@ MLIS := \
 	cCHPOCheckIndexLowerBound \
 	cCHPOCheckIndexUpperBound \
 	cCHPOCheckInitialized \
+	cCHPOCheckLocallyInitialized \
 	cCHPOCheckInitializedRange \
 	cCHPOCheckIntUtil \
 	cCHPOCheckIntOverflow \
@@ -72,6 +73,8 @@ MLIS := \
 	cCHPOCheckNotNull \
 	cCHPOCheckNotZero \
 	cCHPOCheckNonNegative \
+	cCHPOCheckOutputParameterInitialized \
+	cCHPOCheckOutputParameterUnaltered \
 	cCHPOCheckPreservedAllMemory \
 	cCHPOCheckStackAddressEscape \
 	cCHPOCheckWidthOverflow \
@@ -126,6 +129,7 @@ SOURCES := \
 	cCHPOCheckIndexLowerBound \
 	cCHPOCheckIndexUpperBound \
 	cCHPOCheckInitialized \
+	cCHPOCheckLocallyInitialized \
 	cCHPOCheckInitializedRange \
 	cCHPOCheckIntUtil \
 	cCHPOCheckIntOverflow \
@@ -138,6 +142,8 @@ SOURCES := \
 	cCHPOCheckNotZero \
 	cCHPOCheckNonNegative \
 	cCHPOCheckWidthOverflow \
+	cCHPOCheckOutputParameterInitialized \
+	cCHPOCheckOutputParameterUnaltered \
 	cCHPOCheckNullTerminated \
 	cCHPOCheckPointerCast \
 	cCHPOCheckPreservedAllMemory \

CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli

@@ -440,26 +440,45 @@ class type po_query_int =
     (** [record_safe_result deps expl] adds the assumptions in [deps] to the
         function api or global environment with PO as a dependent, sets the
         status of PO to safe (Green), and records the dependencies and
-        explanation [expl] in PO.*)
-    method record_safe_result: dependencies_t -> string -> unit
+        explanation [expl] in PO. Optionally a [site] can be added that
+        records the location in the ocaml code that provided the decision
+     *)
+    method record_safe_result:
+             ?site:(string * int * string) option
+             -> dependencies_t
+             -> string
+             -> unit
 
     (** [record_violation_result deps expl] sets the status of PO to violated
         (Red), and records the dependencies [deps] and explanation [expl]
-        in PO.*)
-    method record_violation_result: dependencies_t -> string -> unit
+        in PO. Optionally a [site] can be added that records the location in
+        the ocaml code that provided the decision
+     *)
+    method record_violation_result:
+             ?site:(string * int * string) option
+             -> dependencies_t
+             -> string
+             -> unit
 
     (** [delegate_to_api isfile isglobal ppred invindices] checks if the local
         predicate [ppred] can be converted to an external (api) predicate. If so,
         it converts [ppred] to an api predicate and creates a dependency on this
         api assumption, justified by the invariants indicated by [invindices].
         It sets the status to safe (Green) and adds an explanation stating that the
         PO has been delegated to the api. In this case [true] is returned.
+        Optionally a [site] can be added that records the location in the ocaml
+        code that provided the decision.
 
         If [ppred] cannot be converted to an api predicate a diagnostic is set
         to this effect, and [false] is returned.
      *)
     method delegate_to_api:
-             ?isfile:bool -> ?isglobal:bool -> po_predicate_t -> int list -> bool
+             ?site:(string * int * string) option
+             -> ?isfile:bool
+             -> ?isglobal:bool
+             -> po_predicate_t
+             -> int list
+             -> bool
 
     (** {1 Make requests} *)
 
@@ -479,43 +498,75 @@ class type po_query_int =
     (** {1 Set diagnostics} *)
 
     (** [set_diagnostic msg] adds message [msg] to the list of general diagnostics
-        of PO.*)
-    method set_diagnostic: string -> unit
+        of PO. Optionally a [site] can be added that records the location of the
+        generation of the diagnostic message.*)
+    method set_diagnostic: ?site: (string * int * string) option -> string -> unit
 
     (** [set_key_diagnostic key msg] adds message [msg] as a key diagnostic to
-        PO with key [key].
+        PO with key [key] Optionally a [site] can be added that records the
+        location of the generation of the diagnostic message..
 
         A key diagnostic is a diagnostic that refers to a particular as yet
         unsolved challenge in the analysis such as the analysis of
         null-termination that prevents the proof obligation to be discharged.
      *)
-    method set_key_diagnostic: string -> string -> unit
+    method set_key_diagnostic:
+             ?site:(string * int * string) option -> string -> string -> unit
 
     (** [set_ref_diagnostic fname] adds a key diagnostic to PO for a challenge
-        in the analysis associated with the function summary for [fname].*)
-    method set_ref_diagnostic: string -> unit
+        in the analysis associated with the function summary for [fname].
+        Optionally a [site] can be added that records the location of the
+        generation of the diagnoatic message.
+     *)
+    method set_ref_diagnostic:
+             ?site:(string * int * string) option -> string -> unit
 
     (** [set_diagnostic_arg argindex msg] adds a diagnostic message [msg] to
-        PO associated with the PO argument with (1-based) index [argindex].*)
-    method set_diagnostic_arg: int -> string -> unit
+        PO associated with the PO argument with (1-based) index [argindex].
+        Optionally a [site] can be added that records the location of the
+        generation of the diagnostic message.
+     *)
+    method set_diagnostic_arg:
+             ?site:(string * int * string) option -> int -> string -> unit
 
     (** [set_exp_diagnostic lb ub exp msg] adds a diagnostic msg [msg] to PO for
         the expression [exp] prefixed by lb-exp if [lb], ub-exp if [ub] or exp
-        if neither of these is true.*)
-    method set_exp_diagnostic: ?lb:bool -> ?ub:bool -> exp -> string -> unit
+        if neither of these is true. Optionally a [site] can be added that records
+        the location of the generation of the diagnostic message.
+     *)
+    method set_exp_diagnostic:
+             ?site:(string * int * string) option
+             -> ?lb:bool
+             -> ?ub:bool
+             -> exp
+             -> string
+             -> unit
 
     (** [set_diagnostic_invariants argindex] adds the invariants associated with
         the argument with (1-based) index [argindex] to the diagnostic invariant
         table for [argindex].*)
     method set_diagnostic_invariants: int -> unit
 
     (** Adds a message to PO that contains all calls that separate this PO from
-        an entry symbol.*)
-    method set_diagnostic_call_invariants: unit
+        an entry symbol. Optionally a [site] can be added that records the
+        location of the generation of the diagnostic message.
+     *)
+    method set_diagnostic_call_invariants:
+             ?site:(string * int * string) option -> unit -> unit
 
     (** [set_vinfo_diagnostic vinfo] adds a diagnostic message to PO that lists
-        all values that variable [vinfo] may have in this PO.*)
-    method set_vinfo_diagnostic_invariants: varinfo -> unit
+        all values that variable [vinfo] may have in this PO. Optionally a [site]
+        can be added that records the location of the generation of the diagnostic
+        message.
+     *)
+    method set_vinfo_diagnostic_invariants:
+             ?site:(string * int * string) option -> varinfo -> unit
+
+    method set_all_diagnostic_invariants:
+             ?site:(string * int * string) option -> unit -> unit
+
+    method set_init_vinfo_mem_diagnostic_invariants:
+             ?site:(string * int * string) option -> varinfo -> offset -> unit
 
     method add_local_spo: location -> program_context_int -> po_predicate_t -> unit
 
@@ -666,6 +717,8 @@ class type po_query_int =
         returns None.*)
     method get_gv_upperbound: string -> int option
 
+    method get_init_vinfo_mem_invariants: varinfo -> offset -> invariant_int list
+
 
     (** {2 Function summary} *)
 

CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2023 Henny B. Sipma
-   Copyright (c) 2024      Aarno Labs LLC
+   Copyright (c) 2024-2025 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
@@ -56,6 +56,8 @@ open CCHUtilities
 open CCHAnalysisTypes
 open CCHCommand
 
+let p2s = CHPrettyUtil.pretty_to_string
+
 
 class num_assignment_translator_t
   (env:c_environment_int)
@@ -82,25 +84,22 @@ object (self)
 	  if chifVar#isTmp then
             let memoryvars = env#get_memory_variables in
             let _ =
-              chlog#add
-                "abstract memory variables"
-                (LBLOCK [
-                     pretty_print_list
-                       memoryvars (fun v -> v#toPretty) "" ", " ""]) in
+              log_diagnostics_result
+                ~tag:"abstract memory variables"
+                ~msg:env#get_functionname
+                __FILE__ __LINE__
+                (List.map (fun v -> (p2s v#toPretty)) memoryvars) in
             CCMD (ABSTRACT_VARS memoryvars)
 	  else if env#has_constant_offset chifVar then
 	    make_c_cmd (ASSIGN_NUM (chifVar, numExp))
           else
             let memoryvars = env#get_memory_variables_with_base chifVar in
             let _ =
-              chlog#add
-                "abstract memory variables with base"
-                (LBLOCK [
-                     STR "base: ";
-                     chifVar#toPretty;
-                     STR "; ";
-                     pretty_print_list
-                       memoryvars (fun v -> v#toPretty) "[" ", " "]"]) in
+              log_diagnostics_result
+                ~tag:"abstract memory variables"
+                ~msg:env#get_functionname
+                __FILE__ __LINE__
+                (List.map (fun v -> (p2s v#toPretty)) memoryvars) in
             CCMD (ABSTRACT_VARS memoryvars) in
         [rhsCode; assign]
       with
@@ -235,19 +234,30 @@ end
 class sym_pointersets_assignment_translator_t
         (env:c_environment_int)
         (exp_translator:exp_translator_int):assignment_translator_int =
-object
+object (self)
 
   val fdecls = env#get_fdecls
 
+  method private dmsg (ctxt: program_context_int) (loc: location): string =
+    env#get_functionname ^ ":"
+    ^ (ctxt#to_string)
+    ^ " (line: " ^ (string_of_int loc.line) ^ ")"
+
   method translate
-           (context:program_context_int) (_loc:location) (lhs:lval) (rhs:exp) =
+           (context:program_context_int) (loc:location) (lhs:lval) (rhs:exp) =
     try
       let chifVar = exp_translator#translate_lhs context lhs in
       let rhsExpr = exp_translator#translate_exp context rhs in
       let assign =
         if chifVar#isTmp then
           if is_pointer_type (type_of_lval fdecls lhs) then
             let ptrvars = env#get_pointer_variables SYM_VAR_TYPE in
+            let _ =
+              log_diagnostics_result
+                ~tag:"abstract pointer variables"
+                ~msg:env#get_functionname
+                __FILE__ __LINE__
+                (List.map (fun v -> p2s v#toPretty) ptrvars) in
             make_c_cmd (ABSTRACT_VARS ptrvars)
           else
             make_c_cmd SKIP
@@ -262,6 +272,14 @@ object
           | _ -> make_c_cmd (ASSIGN_SYM (chifVar, SYM (new symbol_t "unknown")))
         else
           make_c_cmd SKIP in
+      let _ =
+        log_diagnostics_result
+          ~msg:(self#dmsg context loc)
+          ~tag:"sym_pointersets:translate assignment"
+          __FILE__ __LINE__
+          ["lhs: " ^ (p2s (lval_to_pretty lhs));
+           "rhs: " ^ (p2s (exp_to_pretty rhs));
+           "result: " ^ (p2s (c_cmd_to_pretty assign))] in
       [assign]
     with
     | CCHFailure p ->