CHC: add locations to diagnostic messages

Author: sipma

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,47 +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: unit
+    method set_all_diagnostic_invariants:
+             ?site:(string * int * string) option -> unit -> unit
 
-    method set_init_vinfo_mem_diagnostic_invariants: varinfo -> offset -> 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
 

CodeHawk/CHC/cchanalyze/cCHPOQuery.ml

@@ -285,51 +285,68 @@ object (self)
       None
 
   method private record_proof_result
+                   ?(site: (string * int * string) option = None)
                    (status:po_status_t)
                    (deps:dependencies_t)
                    (expl:string) =
     begin
       po#set_status status;
       po#set_dependencies deps;
-      po#set_explanation expl;
+      po#set_explanation ~site expl;
       po#set_resolution_timestamp (current_time_to_string ())
     end
 
-  method set_diagnostic (msg: string) = po#add_diagnostic_msg msg
+  method set_diagnostic
+           ?(site: (string * int * string) option = None)
+           (msg: string) =
+    po#add_diagnostic_msg ~site msg
 
-  method set_key_diagnostic (key: string) (msg: string) =
-    po#add_diagnostic_key_msg key msg
+  method set_key_diagnostic
+           ?(site: (string * int * string) option = None)
+           (key: string)
+           (msg: string) =
+    po#add_diagnostic_key_msg ~site key msg
 
-  method set_ref_diagnostic (fname: string) =
+  method set_ref_diagnostic
+           ?(site: (string * int * string) option = None) (fname: string) =
     match self#get_summary fname with
     | Some s ->
        begin
          match s.fs_domainref with
          | Some (ref, desc) ->
-            po#add_diagnostic_key_msg ("DomainRef:" ^ ref ^ ":" ^ fname) desc
+            po#add_diagnostic_key_msg ~site ("DomainRef:" ^ ref ^ ":" ^ fname) desc
          | _ -> ()
        end
     | _ -> ()
 
-  method set_diagnostic_arg (index: int) (txt: string) =
+  method set_diagnostic_arg
+           ?(site: (string * int * string) option = None)
+           (index: int)
+           (txt: string) =
     let txt = "[" ^ (string_of_int) index ^ "]:" ^ txt in
-    po#add_diagnostic_arg_msg index txt
+    po#add_diagnostic_arg_msg ~site index txt
 
-  method set_exp_diagnostic ?(lb=false) ?(ub=false) (e:exp) (s:string) =
+  method set_exp_diagnostic
+           ?(site: (string * int * string) option = None)
+           ?(lb=false)
+           ?(ub=false)
+           (e:exp)
+           (s:string) =
     match e with
     | Const (CInt _) -> ()
     | _ ->
        let prefix =
          if lb then "lb-exp" else if ub then "ub-exp" else "exp" in
-       self#set_diagnostic ("[" ^ prefix ^  ":" ^ (e2s e) ^ "]: " ^ s)
+       self#set_diagnostic ~site ("[" ^ prefix ^  ":" ^ (e2s e) ^ "]: " ^ s)
 
   method set_diagnostic_invariants (index:int) =
     let invs = List.map (fun inv -> inv#index) (self#get_invariants index) in
     match invs with
     | [] -> ()
     | _ -> po#set_diagnostic_invariants index invs
 
-  method set_diagnostic_call_invariants =
+  method set_diagnostic_call_invariants
+           ?(site: (string * int * string) option = None) () =
     let callinvs = self#get_call_invariants in
     let entrysym = env#get_p_entry_sym in
     List.iter (fun inv ->
@@ -338,22 +355,25 @@ object (self)
            begin
              match l with
              | [s] when s#equal entrysym ->
-                self#set_diagnostic ("[" ^ v#getName#getBaseName ^ ":calls]:none")
+                self#set_diagnostic
+                  ~site ("[" ^ v#getName#getBaseName ^ ":calls]:none")
               | _ ->
                  let lst =
                    List.fold_left (fun acc s ->
                        if s#equal entrysym then
                          acc
                        else
                          acc ^ "; " ^ s#getBaseName) "" l in
-                 self#set_diagnostic ("[" ^ v#getName#getBaseName ^ ":calls]" ^ lst)
+                 self#set_diagnostic
+                   ~site("[" ^ v#getName#getBaseName ^ ":calls]" ^ lst)
             end
         | _ -> ()) callinvs
 
-  method set_all_diagnostic_invariants =
+  method set_all_diagnostic_invariants
+           ?(site: (string * int * string) option = None) () =
     let locinv = invio#get_location_invariant cfgcontext in
     let invs = locinv#get_invariants in
-    List.iter (fun inv -> po#add_diagnostic_msg (p2s (inv#toPretty))) invs
+    List.iter (fun inv -> po#add_diagnostic_msg ~site (p2s (inv#toPretty))) invs
 
   method get_init_vinfo_mem_invariants
            (vinfo: varinfo) (offset: offset): invariant_int list =
@@ -377,6 +397,7 @@ object (self)
         | _ -> acc) [] (invio#get_location_invariant cfgcontext)#get_invariants
 
   method set_init_vinfo_mem_diagnostic_invariants
+           ?(site: (string * int * string) option = None)
            (vinfo: varinfo) (offset: offset) =
     let numv = self#env#mk_program_var vinfo NoOffset NUM_VAR_TYPE in
     let ctxtinvs = (invio#get_location_invariant cfgcontext)#get_invariants in
@@ -398,12 +419,14 @@ object (self)
              else
                acc
           | _ -> acc) [] ctxtinvs in
-    List.iter (fun inv -> po#add_diagnostic_msg (p2s (inv#toPretty))) invs
+    List.iter (fun inv -> po#add_diagnostic_msg ~site (p2s (inv#toPretty))) invs
 
-  method set_vinfo_diagnostic_invariants (vinfo:varinfo) =
+  method set_vinfo_diagnostic_invariants
+           ?(site: (string * int * string) option = None) (vinfo:varinfo) =
     let vinfovalues = self#get_vinfo_offset_values vinfo in
     List.iter (fun (inv, offset) ->
         po#add_diagnostic_msg
+          ~site
           ("["
            ^ vinfo.vname
            ^ "]: "
@@ -416,7 +439,10 @@ object (self)
   method private record_unevaluated (x:xpr_t) =
     fApi#add_unevaluated po#get_predicate (xd#index_xpr x)
 
-  method record_safe_result (deps:dependencies_t) (expl:string) =
+  method record_safe_result
+           ?(site: (string * int * string) option = None)
+           (deps: dependencies_t)
+           (expl: string) =
     let _ = match deps with
       | DEnvC (_, assumptions) ->
          let (ppos, spos) = self#get_ppos_spos in
@@ -434,12 +460,16 @@ object (self)
                   (fApi#add_api_assumption ~isglobal:true ~ppos ~spos pred)
            ) assumptions
       | _ -> () in
-    self#record_proof_result Green deps expl
+    self#record_proof_result ~site Green deps expl
 
-  method record_violation_result (deps:dependencies_t) (expl:string) =
-    self#record_proof_result Red deps expl
+  method record_violation_result
+           ?(site: (string * int * string) option = None)
+           (deps:dependencies_t)
+           (expl:string) =
+    self#record_proof_result ~site Red deps expl
 
   method delegate_to_api
+           ?(site: (string * int * string) option = None)
            ?(isfile=false)
            ?(isglobal=false)
            (pred:po_predicate_t)
@@ -454,12 +484,13 @@ object (self)
          ^ (p2s (po_predicate_to_pretty apred))
          ^ " delegated to api" in
        begin
-         self#record_proof_result Green deps expl;
+         self#record_proof_result ~site Green deps expl;
          true
        end
     | _ ->
        begin
          self#set_diagnostic
+           ~site
            ("condition " ^ (p2s (po_predicate_to_pretty pred)) ^ " not delegated");
          false
        end