CHC:POCHECK: add diagnoatic messages

sipma · sipma · commit 953c96f2da14 · 2025-11-12T12:42:16.000-08:00
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml
@@ -153,6 +153,8 @@ object (self)
   (* ----------------------------- safe ------------------------------------- *)
   (* check_safe
      - inv_implies_safe
+       - inv_xpr_implies_safe
+       - inv_bounded_xpr_implies_safe
      - check_safe_command_line_argument
      - check_safe_lval
        - check_safe_memlval
@@ -162,6 +164,29 @@ object (self)
              - memlval_vinv_memref_basevar_implies_safe
    *)
 
+  method private inv_xpr_implies_safe (invindex: int) (x: xpr_t) =
+    let deps = DLocal [invindex] in
+    let msg =
+      "variable "
+      ^ (p2s (lval_to_pretty lval))
+      ^ " has the value "
+      ^ (x2s x) in
+    let site = Some (__FILE__, __LINE__, "inv_xpr_implies_safe") in
+    Some (deps, msg, site)
+
+  method private inv_bounded_xpr_implies_safe
+                   (invindex: int) (lb: xpr_t) (ub: xpr_t) =
+    let deps = DLocal [invindex] in
+    let msg =
+      "variable "
+      ^ (p2s (lval_to_pretty lval))
+      ^ " is bounded by LB: "
+      ^ (x2s lb)
+      ^ " and UB: "
+      ^ (x2s ub) in
+    let site = Some (__FILE__, __LINE__, "inv_bounded_xpr_implies_safe") in
+    Some (deps, msg, site)
+
   method private inv_implies_safe (inv: invariant_int) =
     let mname = "inv_implies_safe" in
     match inv#get_fact with
@@ -177,9 +202,16 @@ object (self)
               (String.concat
                  "_xx_" (List.map self#get_symbol_name localAssigns)) in
             let site = Some (__FILE__, __LINE__, mname) in
-            Some (deps,msg, site)
+            Some (deps, msg, site)
        end
-    | _ -> None
+    | _ ->
+       match inv#expr with
+       | Some x -> self#inv_xpr_implies_safe inv#index x
+       | _ ->
+          match (inv#lower_bound_xpr, inv#upper_bound_xpr) with
+          | (Some lb, Some ub) ->
+             self#inv_bounded_xpr_implies_safe inv#index lb ub
+          | _ -> None
 
   method private check_safe_functionpointer (vinfo: varinfo) =
     let vinfovalues = poq#get_vinfo_offset_values vinfo in
@@ -231,6 +263,37 @@ object (self)
                false
              end) false vinfovalues
 
+  method private memlval_vinv_memref_stackvar_implies_safe
+                   (invindex: int) (vinfo: varinfo) =
+    let mname = "memlval_vinv_memref_stackvar_implies_safe" in
+    let vinfovalues = poq#get_vinfo_offset_values vinfo in
+    List.fold_left (fun acc (vinv, voffset) ->
+        match acc with
+        | Some _ -> acc
+        | _ ->
+           match vinv#get_fact, voffset with
+           | NonRelationalFact (_, FInitializedSet l), NoOffset ->
+              (match l with
+               | [] -> None
+               | _ ->
+                  let deps = DLocal [invindex; vinv#index] in
+                  let msg =
+                    "local assignment(s) to "
+                    ^ vinfo.vname
+                    ^ ": "
+                    ^ (String.concat
+                         "_xx_" (List.map self#get_symbol_name l)) in
+                  let site = Some (__FILE__, __LINE__, mname) in
+                  Some (deps, msg, site))
+           | _ ->
+              begin
+                poq#set_diagnostic
+                  ~site:(Some (__FILE__, __LINE__, mname))
+                  ("[" ^ vinfo.vname ^ "]: " ^ (p2s vinv#toPretty));
+                None
+              end
+      ) None vinfovalues
+
   method private memlval_vinv_memref_basevar_implies_safe
                    (invindex: int) (v: variable_t) (memoffset: offset) =
     let mname = "memlval_vinv_memref_basevar_implies_safe" in
@@ -366,8 +429,13 @@ object (self)
                 1
                 ("stack variable: "
                  ^ vinfo.vname
+                 ^ " with offset "
                  ^ (p2s (offset_to_pretty voffset))) in
-            None
+            (match (voffset, memoffset) with
+             | (NoOffset, NoOffset) ->
+                self#memlval_vinv_memref_stackvar_implies_safe invindex vinfo
+             | _ -> None)
+
          | CBaseVar v ->
             (try
                self#memlval_vinv_memref_basevar_implies_safe invindex v memoffset
@@ -458,7 +526,7 @@ object (self)
        let _ =
          poq#set_diagnostic
            ~site:(Some (__FILE__, __LINE__, mname))
-           ("[offset]: " ^ (p2s (offset_to_pretty memoffset))) in
+           ("[mem-offset]: " ^ (p2s (offset_to_pretty memoffset))) in
        List.fold_left (fun acc (inv, offset) ->
            acc ||
              match offset with
@@ -566,7 +634,7 @@ object (self)
   (* ----------------------- delegation ------------------------------------- *)
   (* check_delegation
      - check_delegation_lval
-       - memlval_implies_delegation
+       - check_delegation_memlval
          - memlval_vinv_implies_delegation
            - memlval_var_implies_delegation
 
@@ -587,11 +655,11 @@ object (self)
       | Lval apilval ->
          let pred = PInitialized apilval in
          let deps = DEnvC ([invindex], [ApiAssumption pred]) in
-         let site = Some (__FILE__, __LINE__, mname) in
          let msg =
            "condition "
            ^ (p2s (po_predicate_to_pretty pred))
            ^ " delegated to the api" in
+         let site = Some (__FILE__, __LINE__, mname) in
          Some (deps, msg, site)
       | _ -> None
     else
@@ -677,11 +745,11 @@ object (self)
               let memlval =  (Mem (Lval lval),memoffset) in
               let pred = PInitialized memlval in
               let deps = DEnvC ([inv#index], [ApiAssumption  pred]) in
-              let site = Some (__FILE__, __LINE__, mname) in
               let msg =
                 "condition "
                 ^ (p2s (po_predicate_to_pretty pred))
                 ^ " delegated to the api (vinv)" in
+              let site = Some (__FILE__, __LINE__, mname) in
               Some (deps, msg, site)
             else
               self#memlval_var_implies_delegation inv#index lval memoffset
@@ -694,7 +762,7 @@ object (self)
        end
     | _ -> None
 
-  method private memlval_implies_delegation (memlval: lval) (memoffset: offset) =
+  method private check_delegation_memlval (memlval: lval) (memoffset: offset) =
     match memlval with
     | (Var (_vname, vid), NoOffset) when vid > 0 ->
        let vinfo  = poq#env#get_varinfo vid in
@@ -719,7 +787,7 @@ object (self)
   method private check_delegation_lval =
     match lval with
     | (Mem (Lval memlval), memoffset) ->
-       self#memlval_implies_delegation memlval memoffset
+       self#check_delegation_memlval memlval memoffset
     | (Mem
          (BinOp
             (_,
@@ -746,7 +814,12 @@ end
 
 
 let check_initialized (poq:po_query_int) (lval:lval) =
-  let invs = poq#get_invariants 1 in
+  let f_priority (inv: invariant_int) =
+    match inv#get_fact with
+    | NonRelationalFact (_, FInitializedSet _) -> true
+    | _ -> false in
+  let invs =
+    CCHInvariantFact.prioritize_invariants f_priority (poq#get_invariants 1) in
   let _ = poq#set_diagnostic_invariants 1 in
   let checker = new initialized_checker_t poq lval invs in
   checker#check_safe || checker#check_violation || checker#check_delegation
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml
@@ -69,11 +69,21 @@ object (self)
        | [] -> ""
        | l  -> "(" ^ (String.concat "" l) ^ ")")
 
+  (* --------------------------- safe --------------------------------------- *)
+  (* check_safe
+     - check_safe_invs
+       - inv_implies_safe
+         - xpr_implies_safe
+   *)
+
   method private xpr_implies_safe (invindex: int) (x: xpr_t) =
+    let mname = "xpr_implies_safe" in
     if poq#is_api_expression x then
       let _ =
         poq#set_diagnostic_arg
-          2 ("api expression: " ^ (e2s (poq#get_api_expression x))) in
+          ~site:(Some (__FILE__, __LINE__, mname))
+          2
+          ("api expression: " ^ (e2s (poq#get_api_expression x))) in
       match poq#get_api_expression x with
       | Lval (Mem (Lval (Var vpar, NoOffset)), NoOffset)
            when not ((fst vpar) = vinfo.vname) ->
@@ -84,12 +94,14 @@ object (self)
             ^ vinfo.vname
             ^ ", but from a different parameter: "
             ^ (fst vpar)) in
-         Some (deps, msg)
+         let site = Some (__FILE__, __LINE__, mname) in
+         Some (deps, msg, site)
       | _ -> None
     else
       None
 
   method private inv_implies_safe (inv: invariant_int) =
+    let mname = "inv_implies_safe" in
     match inv#expr with
     | Some x -> self#xpr_implies_safe inv#index x
     | _ ->
@@ -105,28 +117,43 @@ object (self)
                 "local assignment(s): "
                 ^ (String.concat
                      "_xx_" (List.map self#get_symbol_name localAssigns)) in
-              Some (deps, msg))
+              let site = Some (__FILE__, __LINE__, mname) in
+              Some (deps, msg, site))
        | _ -> None
 
-  method private check_invs_safe =
+  method private check_safe_invs =
     match invs with
     | [] -> false
     | _ ->
        List.fold_left (fun acc inv ->
            acc ||
              match self#inv_implies_safe inv with
-             | Some (deps, msg) ->
+             | Some (deps, msg, site) ->
                 begin
-                  poq#record_safe_result deps msg;
+                  poq#record_safe_result ~site deps msg;
                   true
                 end
              | _ -> false) false invs
 
+  (* --------------------------- violation ---------------------------------- *)
+  (* check_violation
+     - check_violation_invs
+       - inv_implies_violation
+         - xpr_implies_violation
+
+     - check_violation_lval
+       - check_violation_memlval
+         - memlval_vinv_implies_violation
+   *)
+
   method private xpr_implies_violation (invindex: int) (x: xpr_t) =
+    let mname = "xpr_implies_violation" in
     if poq#is_api_expression x then
       let _ =
         poq#set_diagnostic_arg
-          2 ("api expression: " ^ (e2s (poq#get_api_expression x))) in
+          ~site:(Some (__FILE__, __LINE__, mname))
+          2
+          ("api expression: " ^ (e2s (poq#get_api_expression x))) in
       match poq#get_api_expression x with
       | Lval (Mem (Lval (Var vpar, NoOffset)), NoOffset)
            when (fst vpar) = vinfo.vname ->
@@ -135,8 +162,8 @@ object (self)
            ("value of " ^ (p2s (lval_to_pretty lval))
             ^ " is obtained from dereferencing parameter "
             ^ (fst vpar)) in
-         Some (deps, msg)
-
+         let site = Some (__FILE__, __LINE__, mname) in
+         Some (deps, msg, site)
       | _ -> None
     else
       None
@@ -146,8 +173,9 @@ object (self)
     | Some x -> self#xpr_implies_violation inv#index x
     | _ -> None
 
-  method private vinv_implies_deref_offset_violation
+  method private memlval_vinv_implies_violation
                    (inv: invariant_int) (memoffset: offset) =
+    let mname = "memlval_vinv_implies_violation" in
     match inv#expr with
     | Some x when poq#is_api_expression x ->
        begin
@@ -161,15 +189,16 @@ object (self)
                 ^ (p2s (lval_to_pretty memlval))
                 ^ " with offset "
                 ^ (p2s (offset_to_pretty memoffset)) in
-              Some (deps, msg)
+              let site = Some (__FILE__, __LINE__, mname) in
+              Some (deps, msg, site)
             else
               None
          | _ ->
             None
        end
     | _ -> None
 
-  method private check_lval_deref_violation (memlval: lval) (memoffset: offset) =
+  method private check_violation_memlval (memlval: lval) (memoffset: offset) =
     match memlval with
     | (Var (vname, vid), NoOffset) when vid > 0 && vinfo.vname = vname ->
        let vinfovalues = poq#get_vinfo_offset_values vinfo in
@@ -178,50 +207,54 @@ object (self)
            || match offset with
               | NoOffset ->
                  begin
-                   match self#vinv_implies_deref_offset_violation
+                   match self#memlval_vinv_implies_violation
                            inv memoffset with
-                   | Some (deps, msg) ->
+                   | Some (deps, msg, site) ->
                       begin
-                        poq#record_violation_result deps msg;
+                        poq#record_violation_result ~site deps msg;
                         true
                       end
                    | _ -> false
                  end
               | _ -> false) false vinfovalues
     | _ -> false
 
-  method private check_lval_violation =
+  method private check_violation_lval =
     match lval with
     | (Mem (Lval memlval), memoffset) ->
-       self#check_lval_deref_violation memlval memoffset
+       self#check_violation_memlval memlval memoffset
     | _ -> false
 
-  method private check_invs_violation =
+  method private check_violation_invs =
     match invs with
     | [] -> false
     | _ ->
        List.fold_left (fun acc inv ->
            acc ||
              match self#inv_implies_violation inv with
-             | Some (deps, msg) ->
+             | Some (deps, msg, site) ->
                 begin
-                  poq#record_violation_result deps msg;
+                  poq#record_violation_result ~site deps msg;
                   true
                 end
              | _ -> false) false invs
 
   method check_safe =
-    self#check_invs_safe
+    self#check_safe_invs
 
   method check_violation =
-    self#check_invs_violation || self#check_lval_violation
+    self#check_violation_invs || self#check_violation_lval
 
 end
 
 
 let check_locally_initialized (poq:po_query_int) (vinfo: varinfo) (lval:lval) =
   let invs = poq#get_invariants 2 in
   let _ = poq#set_diagnostic_invariants 2 in
-  let _ = poq#set_init_vinfo_mem_diagnostic_invariants vinfo (snd lval) in
+  let _ =
+    poq#set_init_vinfo_mem_diagnostic_invariants
+      ~site:(Some (__FILE__, __LINE__, "check_locally_initialized"))
+      vinfo
+      (snd lval) in
   let checker = new locally_initialized_checker_t poq vinfo lval invs in
   checker#check_safe || checker#check_violation
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml
@@ -398,7 +398,8 @@ object (self)
 
   method set_init_vinfo_mem_diagnostic_invariants
            ?(site: (string * int * string) option = None)
-           (vinfo: varinfo) (offset: offset) =
+           (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
     let invs =
diff --git a/CodeHawk/CHC/cchcmdline/cCHVersion.ml b/CodeHawk/CHC/cchcmdline/cCHVersion.ml
@@ -63,4 +63,4 @@ end
 
 let version = new version_info_t
   ~version:"0.3.0"
-  ~date:"2025-10-28"
+  ~date:"2025-11-12"
