CHC: add attribute post request for initialized value

Author: sipma

CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli

@@ -219,7 +219,14 @@ object
   method get_variable_type: variable_t -> typ
   method get_local_variable: variable_t -> (varinfo * offset)
   method get_global_variable: variable_t -> (varinfo * offset)
+
+  (** [get_memory_variable v] returns the memory reference associated with the
+      base of variable [v], and the offset from that base.
+
+      @raise [BCH_failure] if [v] is not a memory variable
+   *)
   method get_memory_variable: variable_t -> (memory_reference_int * offset)
+
   method get_memory_address: variable_t -> (memory_reference_int * offset)
   method get_memory_region: symbol_t -> memory_region_int
   method get_vinfo_offset: variable_t -> varinfo -> offset option

CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml

@@ -108,6 +108,30 @@ object (self)
              - memlval_vinv_memref_basevar_implies_safe
    *)
 
+  method private postcondition_implies_safe
+                   (invindex: int)
+                   (callee: varinfo)
+                   (pcs: annotated_xpredicate_t list) =
+    let mname = "postcondition_implies_safe" in
+    match pcs with
+    | [] -> None
+    | _ ->
+       List.fold_left (fun facc (pc, _) ->
+           match facc with
+           | Some _ -> facc
+           | _ ->
+              match pc with
+              | XInitialized (ArgAddressedValue (ReturnValue, ArgNoOffset)) ->
+                 let deps =
+                   DEnvC ([invindex], [PostAssumption (callee.vid, pc)]) in
+                 let msg =
+                   "value addressed by return value from "
+                   ^ callee.vname
+                   ^ " is initialized" in
+                 let site = Some (__FILE__, __LINE__, mname) in
+                 Some (deps, msg, site)
+              | _ -> None) None pcs
+
   method private inv_implies_safe (inv: invariant_int) =
     let mname = "inv_implies_safe" in
     match inv#get_fact with
@@ -125,7 +149,56 @@ object (self)
             let site = Some (__FILE__, __LINE__, mname) in
             Some (deps, msg, site)
        end
-    | _ -> None
+    | _ ->
+       match inv#expr with
+       | Some (XVar v) when poq#env#is_initial_value v ->
+          let var = poq#env#get_initial_value_variable v in
+          if poq#env#is_memory_variable var then
+            let (memref, offset) = poq#env#get_memory_variable var in
+            if is_zero_memory_offset offset then
+              if memref#has_external_base then
+                let basevar = memref#get_external_basevar in
+                if poq#env#is_function_return_value basevar then
+                  let callee = poq#env#get_callvar_callee basevar in
+                  let (pcs, epcs) = poq#get_postconditions basevar in
+                  let r =
+                    match epcs with
+                    | [] ->
+                       self#postcondition_implies_safe inv#index callee pcs
+                    | _ -> None in
+                  match r with
+                  | None ->
+                     let pcr =
+                       XInitialized
+                         (ArgAddressedValue (ReturnValue, ArgNoOffset)) in
+                     begin
+                       poq#mk_postcondition_request pcr callee;
+                       poq#set_diagnostic
+                         ("Unable to determine if memory pointed at by the return "
+                          ^ "value from "
+                          ^ callee.vname
+                          ^ " is initialized.");
+                       None
+                     end
+                  | Some _ -> r
+                else
+                   begin
+                     poq#set_diagnostic_arg
+                       1 ("memvar:base: " ^ (p2s memref#toPretty));
+                 None
+               end
+            else
+               None
+          else
+            begin
+              poq#set_diagnostic_arg
+                1 ("initial-value: " ^ (p2s v#toPretty));
+              None
+            end
+          else
+            None
+       | _ ->
+          None
 
   method private check_safe_functionpointer (vinfo: varinfo) =
     let vinfovalues = poq#get_vinfo_offset_values vinfo in

CodeHawk/CHC/cchlib/cCHCAttributes.ml

@@ -158,6 +158,9 @@ let convert_attribute_to_function_conditions
   | Attr ("returns_nonnull", []) ->
      ([], [XNotNull ReturnValue], [])
 
+  | Attr ("chkc_returns_addressed_initialized", []) ->
+     ([], [XInitialized (ArgAddressedValue (ReturnValue, ArgNoOffset))], [])
+
   | Attr ("chkc_returns_null_terminated_string", []) ->
      ([], [XNullTerminated ReturnValue], [])
 

CodeHawk/CHC/cchlib/cCHFileContract.ml

@@ -637,7 +637,16 @@ object (self)
                    (vinfo: varinfo) (attr: attribute) =
     let (xpre, xpost, xside) =
       convert_attribute_to_function_conditions vinfo.vname attr in
+    let logx kind x =
+      log_diagnostics_result
+        ~tag:("add_function_attribute_conditions:" ^ kind)
+        ~msg:vinfo.vname
+        __FILE__ __LINE__
+        [p2s (xpredicate_to_pretty x)] in
     begin
+      List.iter (logx "pre") xpre;
+      List.iter (logx "post") xpost;
+      List.iter (logx "side") xside;
       List.iter (self#add_precondition vinfo.vname) xpre;
       List.iter (self#add_postcondition vinfo.vname) xpost;
       List.iter (self#add_sideeffect vinfo.vname) xside

CodeHawk/CHC/cchlib/cCHTypesUtil.ml

@@ -217,6 +217,13 @@ let rec is_constant_string (e:exp) =
   | _ -> false
 
 
+let is_zero_memory_offset (offset: offset): bool =
+  match offset with
+  | NoOffset -> true
+  | Index (Const (CInt (i64, _, _)), NoOffset) -> i64 = Int64.zero
+  | _ -> false
+
+
 let rec type_of_exp (fdecls:cfundeclarations_int) (x:exp) : typ =
   try
     let ty =

CodeHawk/CHC/cchlib/cCHTypesUtil.mli

@@ -148,6 +148,8 @@ val is_field_offset: offset -> bool
 
 val is_constant_offset: offset -> bool
 
+val is_zero_memory_offset: offset -> bool
+
 val is_field_lval_exp: exp -> bool
 
 val exp_has_repeated_field: exp -> bool

CodeHawk/CHC/cchlib/cCHVersion.ml

@@ -62,5 +62,5 @@ object (self)
 end
 
 let version = new version_info_t
-  ~version:"0.3.0_20260223"
-  ~date:"2026-02-23"
+  ~version:"0.3.0_20260302"
+  ~date:"2026-03-02"