From e4d7b2a9d980449a6bd8f9f1f1d41d53d26be787 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 2 Mar 2026 12:12:30 -0800 Subject: [PATCH] CHC: add attribute post request for initialized value --- CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli | 7 ++ .../CHC/cchanalyze/cCHPOCheckInitialized.ml | 75 ++++++++++++++++++- CodeHawk/CHC/cchlib/cCHCAttributes.ml | 3 + CodeHawk/CHC/cchlib/cCHFileContract.ml | 9 +++ CodeHawk/CHC/cchlib/cCHTypesUtil.ml | 7 ++ CodeHawk/CHC/cchlib/cCHTypesUtil.mli | 2 + CodeHawk/CHC/cchlib/cCHVersion.ml | 4 +- 7 files changed, 104 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli b/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli index ba88b1cd..8930ec49 100644 --- a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli +++ b/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 diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml index 4c4bd6bf..dd967b5e 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml +++ b/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 diff --git a/CodeHawk/CHC/cchlib/cCHCAttributes.ml b/CodeHawk/CHC/cchlib/cCHCAttributes.ml index 5aaf554a..88178b81 100644 --- a/CodeHawk/CHC/cchlib/cCHCAttributes.ml +++ b/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], []) diff --git a/CodeHawk/CHC/cchlib/cCHFileContract.ml b/CodeHawk/CHC/cchlib/cCHFileContract.ml index 76b16e55..297d0b11 100644 --- a/CodeHawk/CHC/cchlib/cCHFileContract.ml +++ b/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 diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml index 25ea0b22..aed8df81 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml +++ b/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 = diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli index 62b3b314..aba34ce0 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli +++ b/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 diff --git a/CodeHawk/CHC/cchlib/cCHVersion.ml b/CodeHawk/CHC/cchlib/cCHVersion.ml index 324c3060..9c9dfbdb 100644 --- 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_20260223" - ~date:"2026-02-23" + ~version:"0.3.0_20260302" + ~date:"2026-03-02"