CHC: add diagnostics for memory variables

Author: sipma

CodeHawk/CHC/cchanalyze/cCHCallTranslator.ml

@@ -1261,6 +1261,13 @@ object (self)
                    (fname:string) (args:exp list) (_fnargs:xpr_t list) =
     let (pcs, _epcs) =
       get_postconditions env#get_functionname (Some fname) context in
+    let _ =
+      log_diagnostics_result
+        ~tag:"sym:get_postconditions"
+        ~msg:env#get_functionname
+        __FILE__ __LINE__
+        ["pcs: " ^
+           (String.concat ", " (List.map annotated_xpredicate_to_string pcs))] in
     List.concat
       (List.map (fun (pc, _) ->
            match pc with
@@ -1334,6 +1341,13 @@ object (self)
                    (fnargs:xpr_t list) =
     let vinfo = fdecls#get_varinfo_by_vid fvid in
     let sideeffects = get_sideeffects env#get_functionname (Some fname) context in
+    let _ =
+      log_diagnostics_result
+        ~tag:"get_sideeffect:sym"
+        ~msg:env#get_functionname
+        __FILE__ __LINE__
+        ["side effects: " ^
+           (String.concat ", " (List.map annotated_xpredicate_to_string sideeffects))] in
     let (sitevars,xsitevars) = env#get_site_call_vars context in
     let fnzargs = List.map (fun _ -> None) fnargs in
     let zsevar =
@@ -1508,9 +1522,25 @@ object (self)
                      | CastE (_, Lval (Var (_vname,vid), offset)) ->
                         let vinfo = env#get_varinfo vid in
                         Some (env#mk_program_var vinfo offset SYM_VAR_TYPE)
-                     | _ -> None
+                     | _ ->
+                        begin
+                          log_diagnostics_result
+                            ~tag:"get_sideeffect:sym:initialized-range"
+                            ~msg:env#get_functionname
+                            __FILE__ __LINE__
+                            ["no base variable found for " ^ (p2s (s_term_to_pretty base))];
+                          None
+                        end
                    end
-                | _ -> None in
+                | _ ->
+                   begin
+                     log_diagnostics_result
+                       ~tag:"get_sideeffect:sym:initialized-range"
+                       ~msg:env#get_functionname
+                       __FILE__ __LINE__
+                       ["base term not recognized: " ^ (p2s (s_term_to_pretty base))];
+                     None
+                   end in
               let lenvalue =
                 match len with
                 | ArgValue (ParFormal n, ArgNoOffset) ->

CodeHawk/CHC/cchanalyze/cCHExtractInvariantFacts.ml

@@ -63,6 +63,9 @@ open CCHNumericalConstraints
 module H = Hashtbl
 
 
+let p2s = CHPrettyUtil.pretty_to_string
+
+
 exception TimeOut of float
 
 
@@ -530,7 +533,7 @@ let extract_valuesets
 
 
 let extract_symbols
-      (_env:c_environment_int)
+      (env:c_environment_int)
       (invio:invariant_io_int)
       (invariants:(string, (string,atlas_t) H.t) H.t) =
   try
@@ -539,6 +542,15 @@ let extract_symbols
           let inv = H.find v symbolic_sets_domain in
           let context = get_context k in
           let facts = extract_symbol_facts symbolic_sets_domain inv in
+          let _ =
+            log_diagnostics_result
+              ~tag:"extract_symbols"
+              ~msg:env#get_functionname
+              __FILE__ __LINE__
+              ["facts: " ^
+                 (String.concat ", "
+                    (List.map (fun f ->
+                         (p2s (invariant_fact_to_pretty f))) facts))] in
           List.iter (fun f -> invio#add_fact context f) facts) invariants
   with
   | CCHFailure p ->

CodeHawk/CHC/cchanalyze/cCHOperationsProvider.ml

@@ -59,6 +59,8 @@ open CCHCommand
 module H = Hashtbl
 
 let x2p = xpr_formatter#pr_expr
+let p2s = CHPrettyUtil.pretty_to_string
+let x2s x = p2s (x2p x)
 
 
 module ProgramContextCollections = CHCollections.Make
@@ -190,14 +192,27 @@ object (self)
                 [make_c_cmd SKIP]
            | _ ->
               match exp_translator#translate_exp context e with
-              | XVar symvar -> [make_c_cmd (ASSIGN_SYM (v, SYM_VAR symvar))]
-              | XConst _ -> [make_c_cmd SKIP]
+              | XVar symvar ->
+                 let _ =
+                   log_diagnostics_result
+                     ~tag:"make_context_operation:sym:symvar"
+                     ~msg:env#get_functionname
+                     __FILE__ __LINE__
+                     ["e: " ^ (p2s (exp_to_pretty e));
+                      "symvar: " ^ (p2s symvar#toPretty)] in
+                 [make_c_cmd (ASSIGN_SYM (v, SYM_VAR symvar))]
+              | XConst _ ->
+                 [make_c_cmd SKIP]
               | xpr ->
                  begin
-                   chlog#add "no symbolic check value assigned"
-                             (LBLOCK [STR env#get_functionname; STR ": ";
-                                       exp_to_pretty e; STR " --> ";
-                                       x2p xpr]);
+                   log_diagnostics_result
+                     ~tag:"make_context_operation:sym"
+                     ~msg:env#get_functionname
+                     __FILE__ __LINE__
+                     ["no symbolic check value assigned for: " ^
+                        "e: " ^ (p2s (exp_to_pretty e));
+                      "translated to: " ^
+                        "xpr: " ^ (x2s xpr)];
                    [make_c_cmd SKIP]
                  end
          end

CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml

@@ -32,6 +32,7 @@ open CHNumerical
 open CHPretty
 
 (* chutil *)
+open CHLogger
 open CHPrettyUtil
 
 (* xprlib *)
@@ -124,6 +125,17 @@ object (self)
 
   method private get_initialization_length (vinfo: varinfo) =
     let vinfovalues = poq#get_vinfo_offset_values vinfo in
+    let _ =
+      log_diagnostics_result
+        ~tag:"get_initialization_length"
+        ~msg:poq#env#get_functionname
+        __FILE__ __LINE__
+        ["vinfo: " ^ vinfo.vname;
+         "vinfo-values: " ^
+           (String.concat ", "
+              (List.map (fun (inv, offset) ->
+                   "(" ^ (p2s inv#toPretty) ^ ", " ^ (p2s (offset_to_pretty offset)))
+                 vinfovalues))] in
     List.fold_left (fun acc (inv,offset) ->
         match acc with
         | Some _ -> acc

CodeHawk/CHC/cchpre/cCHInvariantFact.ml

@@ -621,7 +621,13 @@ object (self)
             else
               inv :: entry in
        H.replace table vindex newentry
-    | _ -> ()
+    | _ ->
+       let _ =
+         log_diagnostics_result
+           ~tag:"integrate_fact:ignored"
+           __FILE__ __LINE__
+           [p2s inv#toPretty] in
+       ()
 
   method write_xml (node:xml_element_int) =
     let invs = List.sort Stdlib.compare (H.fold (fun k _ a -> k::a) facts []) in

CodeHawk/CHC/cchpre/cCHMemoryBase.ml

@@ -28,12 +28,16 @@
    ============================================================================= *)
 
 (* chlib *)
+open CHLanguage
 open CHPretty
 
 (* cchpre *)
 open CCHPreTypes
 
 
+let p2s = CHPrettyUtil.pretty_to_string
+
+
 let memory_base_to_string (b:memory_base_t) =
   match b with
   | CNull i -> "NULL(" ^ (string_of_int i) ^ ")"
@@ -44,6 +48,8 @@ let memory_base_to_string (b:memory_base_t) =
      ^ v#getName#getBaseName
      ^ "_"
      ^ (string_of_int v#getName#getSeqNumber)
+     ^ "_"
+     ^ (p2s (variable_type_to_pretty v#getType))
   | CGlobalAddress v -> "addrof_globalvar_" ^ v#getName#getBaseName
   | CBaseVar (v, nullattr) ->
      "addr_in_"