CHC:POCHECK: add proof obligation discharge rules

sipma · sipma · commit 36494d8a157a · 2025-11-18T12:20:35.000-08:00
diff --git a/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml b/CodeHawk/CHC/cchanalyze/cCHFunctionTranslator.ml
@@ -60,6 +60,10 @@ open CCHExpTranslator
 module EU = CCHEngineUtil
 module H = Hashtbl
 
+
+let p2s = CHPrettyUtil.pretty_to_string
+
+
 let fenv = CCHFileEnvironment.file_environment
 
 
@@ -94,8 +98,16 @@ object (self)
         let ttyp = fenv#get_type_unrolled vinfo.vtype in
         match ttyp with
         | TPtr ((TInt _ | TFloat _), _) ->
-           let (v,vInit,vm,vmInit) =
+           let (v, vInit, vm, vmInit) =
              env#mk_par_deref_init vinfo NoOffset ttyp NUM_VAR_TYPE in
+           let _ =
+             log_diagnostics_result
+               ~msg:env#get_functionname
+               __FILE__ __LINE__
+               ["v: " ^ (p2s v#toPretty);
+                "vInit: " ^ (p2s vInit#toPretty);
+                "vm: " ^ (p2s vm#toPretty);
+                "vmInit: " ^ (p2s vmInit#toPretty)] in
            (ASSIGN_NUM (v, NUM_VAR vInit))
            :: (ASSIGN_NUM (vm, NUM_VAR vmInit))
            :: acc
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml
@@ -78,8 +78,34 @@ object (self)
      - check_safe_lval
        - check_safe_memlval
          - memlval_implies_safe
+           - memlval_memref_implies_safe
+             -memlval_memref_basevar_implies_safe
    *)
 
+  method private memlval_memref_basevar_implies_safe
+                   (invindex: int) (basevar: variable_t) =
+    let mname = "memlval_memref_basevar_implies_safe" in
+    if poq#env#is_function_return_value basevar then
+      let callee = poq#env#get_callvar_callee basevar in
+      let apilval = Lval (Var (self#vinfo.vname, self#vinfo.vid), NoOffset) in
+      let pred = PUniquePointer apilval in
+      let deps = DEnvC ([invindex], [ApiAssumption pred]) in
+      let msg =
+        "assumption on the environment that the memory region "
+        ^ " pointed at by the return value from "
+        ^ callee.vname
+        ^ " does not overlap with the memory region pointed at by "
+        ^ self#vinfo.vname in
+      let site = Some (__FILE__, __LINE__, mname) in
+      Some (deps, msg, site)
+    else
+       begin
+         poq#set_diagnostic
+           ~site:(Some (__FILE__, __LINE__, mname))
+           ("[memlval:basevar]: " ^ (p2s basevar#toPretty));
+         None
+       end
+
   method private memlval_memref_implies_safe
                    (invindex: int)
                    (memlval: lval)
@@ -98,6 +124,8 @@ object (self)
          ^ vinfo.vname in
        let site = Some (__FILE__, __LINE__, mname) in
        Some (deps, msg, site)
+    | CBaseVar bvar ->
+       self#memlval_memref_basevar_implies_safe invindex bvar
     | _ ->
        begin
          poq#set_diagnostic
@@ -339,23 +367,24 @@ object (self)
 
   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
+    | (Var (_, vid), _) when vid > 0 ->
+       let lvinfo = poq#env#get_varinfo vid in
+       let vinfovalues = poq#get_vinfo_offset_values lvinfo in
        List.fold_left (fun acc (inv, offset) ->
            acc
-           || match offset with
-              | NoOffset ->
-                 begin
-                   match self#memlval_vinv_implies_violation
-                           inv memoffset with
-                   | Some (deps, msg, site) ->
-                      begin
-                        poq#record_violation_result ~site deps msg;
-                        true
-                      end
-                   | _ -> false
-                 end
-              | _ -> false) false vinfovalues
+           || (match offset with
+               | NoOffset ->
+                  begin
+                    match self#memlval_vinv_implies_violation
+                            inv memoffset with
+                    | Some (deps, msg, site) ->
+                       begin
+                         poq#record_violation_result ~site deps msg;
+                         true
+                       end
+                    | _ -> false
+                  end
+               | _ -> false)) false vinfovalues
     | _ -> false
 
   method private check_violation_lval =
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml
@@ -53,12 +53,14 @@ let _fenv = CCHFileEnvironment.file_environment
 class outputparameter_initialized_checker_t
         (poq: po_query_int)
         (vinfo: varinfo)
-        (_offset: offset)
+        (offset: offset)
         (invs: invariant_int list) =
 object (self)
 
   method private vinfo = vinfo
 
+  method private offset = offset
+
   method private get_symbol_name (s: symbol_t) =
     s#getBaseName
     ^ (match s#getAttributes with
@@ -147,9 +149,13 @@ object (self)
                 end
              | _ -> false) false invs
 
+  method check_violation =
+    self#check_invs_violation
+
   (* --------------------------------- safe --------------------------------- *)
   (* check_safe
-     - inv_implies_safe
+     - check_safe_invs
+       - inv_implies_safe
    *)
 
   method private inv_implies_safe (inv: invariant_int) =
@@ -177,7 +183,7 @@ object (self)
          None
        end
 
-  method check_safe =
+  method private check_safe_invs =
     List.fold_left (fun acc inv ->
         acc
         || (match self#inv_implies_safe inv with
@@ -188,8 +194,7 @@ object (self)
                end
             | _ -> false)) false invs
 
-  method check_violation =
-    self#check_invs_violation
+  method check_safe = self#check_safe_invs
 
 end
 
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml
@@ -33,8 +33,10 @@ open XprTypes
 
 (* cchlib *)
 open CCHBasicTypes
+open CCHTypesToPretty
 
 (* cchpre *)
+open CCHMemoryBase
 open CCHPreTypes
 
 (* cchanalyze *)
@@ -67,11 +69,76 @@ object (self)
 
   (* ------------------------------- safe ----------------------------------- *)
   (* check_safe
-     - check_invs_safe
+     - check_safe_invs
        - inv_implies_safe
          - inv_xpr_implies_safe
+     - check_safe_lval
+       - check_safe_memlval
+         - memlval_implies_safe
+           -memlval_memref_implies_safe
    *)
 
+  method private memlval_memref_basevar_implies_safe
+                   (_invindex: int) (basevar: variable_t) =
+    let mname = "memlval_memref_basevar_implies_safe" in
+    begin
+      poq#set_diagnostic
+        ~site:(Some (__FILE__, __LINE__, mname))
+        ("[memref-basevar]: " ^ (p2s basevar#toPretty));
+      None
+    end
+
+  method private memlval_memref_implies_safe
+                   (invindex: int) (memref: memory_reference_int) =
+    let mname = "memlval_memref_implies_safe" in
+    match memref#get_base with
+    | CBaseVar bvar ->
+       self#memlval_memref_basevar_implies_safe invindex bvar
+    | _ ->
+       begin
+         poq#set_diagnostic
+           ~site:(Some (__FILE__, __LINE__, mname))
+           ("[memref-base]: "
+            ^ (p2s (memory_base_to_pretty memref#get_base)));
+         None
+       end
+
+  method private memlval_implies_safe (inv: invariant_int) (offset: offset) =
+    let mname = "memlval_implies_safe" in
+    match inv#expr with
+    | Some (XVar v) when poq#env#is_memory_address v ->
+       let (memref, _) = poq#env#get_memory_address v in
+       self#memlval_memref_implies_safe inv#index memref
+    | Some x ->
+       begin
+         poq#set_diagnostic
+           ~site:(Some (__FILE__, __LINE__, mname)) ("[xpr]: " ^ (x2s x));
+         None
+       end
+    | _ ->
+       begin
+         poq#set_diagnostic
+           ~site:(Some (__FILE__, __LINE__, mname))
+           ("[inv,offset]: "
+            ^ (p2s inv#toPretty)
+            ^ ", "
+            ^ (p2s (offset_to_pretty offset)));
+         None
+       end
+
+  method private check_safe_lval =
+    let vinfovalues = poq#get_vinfo_offset_values self#vinfo in
+    List.fold_left (fun acc (inv, offset) ->
+        acc
+        || (match self#memlval_implies_safe inv offset with
+            | Some (deps, msg, site) ->
+               begin
+                 poq#record_safe_result ~site deps msg;
+                 true
+               end
+            | _ ->
+               false)) false vinfovalues
+
   method private inv_xpr_implies_safe (invindex: int) (xpr: xpr_t) =
     let mname = "inv_xpr_implies_safe" in
     let numv = poq#env#mk_program_var vinfo NoOffset NUM_VAR_TYPE in
@@ -133,7 +200,7 @@ object (self)
          None
        end
 
-  method private check_invs_safe =
+  method private check_safe_invs =
     match invs with
     | [] -> false
     | _ ->
@@ -147,6 +214,9 @@ object (self)
                 end
              | _ -> false) false invs
 
+  method check_safe =
+    self#check_safe_invs || self#check_safe_lval
+
   (* --------------------------- violation ---------------------------------- *)
   (* check_violation
      - inv_implies_violation
@@ -177,9 +247,6 @@ object (self)
          None
        end
 
-  method check_safe =
-    self#check_invs_safe
-
   method check_violation =
     List.fold_left (fun acc inv ->
         acc
diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml
@@ -378,6 +378,7 @@ object (self)
   method get_init_vinfo_mem_invariants
            (vinfo: varinfo) (offset: offset): invariant_int list =
     let numv = self#env#mk_program_var vinfo NoOffset NUM_VAR_TYPE in
+    let ctxtinvs = (invio#get_location_invariant cfgcontext)#get_invariants in
     List.fold_left (fun acc inv ->
         match inv#get_fact with
         | NonRelationalFact (v, _) ->
@@ -394,32 +395,13 @@ object (self)
               | _ -> acc)
            else
              acc
-        | _ -> acc) [] (invio#get_location_invariant cfgcontext)#get_invariants
+        | _ -> acc) [] ctxtinvs
 
   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
-    let invs =
-      List.fold_left (fun acc inv ->
-          match inv#get_fact with
-          | NonRelationalFact (v, _) ->
-             if self#env#is_memory_variable v then
-               let (memref, memoffset) = self#env#get_memory_variable v in
-               (match memref#get_base with
-                | CBaseVar base when self#env#is_initial_parameter_value base ->
-                   let basevar = self#env#get_initial_value_variable base in
-                   if numv#equal basevar
-                      && (offset_compare offset memoffset) = 0 then
-                     inv :: acc
-                   else
-                     acc
-                | _ -> acc)
-             else
-               acc
-          | _ -> acc) [] ctxtinvs in
+    let invs = self#get_init_vinfo_mem_invariants vinfo offset in
     List.iter (fun inv -> po#add_diagnostic_msg ~site (p2s (inv#toPretty))) invs
 
   method set_vinfo_diagnostic_invariants
diff --git a/CodeHawk/CHC/cchlib/cCHVersion.ml b/CodeHawk/CHC/cchlib/cCHVersion.ml
@@ -62,5 +62,5 @@ object (self)
 end
 
 let version = new version_info_t
-  ~version:"0.3.0_20251114"
-  ~date:"2025-11-14"
+  ~version:"0.3.0_20251118"
+  ~date:"2025-11-19"
diff --git a/CodeHawk/CHC/cchpre/cCHProofObligation.ml b/CodeHawk/CHC/cchpre/cCHProofObligation.ml
@@ -660,7 +660,7 @@ let read_xml_explanation (node: xml_element_int) (po: proof_obligation_int)=
       if node#hasNamedAttribute "file" then
         Some (
             cd#get_string (geti "file"),
-            geti "linenr",
+            geti "line",
             cd#get_string (geti "detail"))
       else
         None in
