Skip to content

Commit 48ca571

Browse files
sipmasipma
committed
CHC: add checker implementations for proof-obligation predicates
1 parent 90dc841 commit 48ca571

10 files changed

+435
-41
lines changed

‎CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -517,6 +517,10 @@ class type po_query_int =
517517
all values that variable [vinfo] may have in this PO.*)
518518
method set_vinfo_diagnostic_invariants: varinfo -> unit
519519

520+
method set_all_diagnostic_invariants: unit
521+
522+
method set_init_vinfo_mem_diagnostic_invariants: varinfo -> offset -> unit
523+
520524
method add_local_spo: location -> program_context_int -> po_predicate_t -> unit
521525

522526
(** {1 Checks} *)
@@ -666,6 +670,8 @@ class type po_query_int =
666670
returns None.*)
667671
method get_gv_upperbound: string -> int option
668672

673+
method get_init_vinfo_mem_invariants: varinfo -> offset -> invariant_int list
674+
669675

670676
(** {2 Function summary} *)
671677

‎CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,15 @@ let make_invariant_generation_spec t =
160160
STR " not recognized"]))
161161

162162

163+
let analysis_is_active (fname: string): bool =
164+
match proof_scaffolding#get_analysis_info fname with
165+
| UndefinedBehaviorInfo -> true
166+
| OutputParameterInfo vinfos ->
167+
let proof_obligations = proof_scaffolding#get_proof_obligations fname in
168+
CCHCreateOutputParameterPOs.output_parameter_analysis_is_active
169+
fname vinfos proof_obligations
170+
171+
163172
let process_function gspecs fname =
164173
let cfilename = system_settings#get_cfilename in
165174
try
@@ -181,7 +190,7 @@ let process_function gspecs fname =
181190
(List.length proofObligations)
182191
(List.length openpos)
183192
__FILE__ __LINE__ in
184-
if (List.length openpos) > 0 then
193+
if (List.length openpos) > 0 && (analysis_is_active fname) then
185194
let _ =
186195
pr_timing [
187196
STR cfilename; STR ": ===analyze function=== "; STR fname;
@@ -304,7 +313,9 @@ let process_function gspecs fname =
304313
save_api fname;
305314
end
306315
else
307-
()
316+
pr_timing [
317+
STR cfilename; STR ":"; STR fname;
318+
STR ": Skip analysis; analysis is not active"]
308319
with
309320
| CCHFailure p ->
310321
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
77
Copyright (c) 2005-2019 Kestrel Technology LLC
88
Copyright (c) 2020-2024 Henny B. Sipma
9-
Copyright (c) 2024 Aarno Labs LLC
9+
Copyright (c) 2024-2025 Aarno Labs LLC
1010
1111
Permission is hereby granted, free of charge, to any person obtaining a copy
1212
of this software and associated documentation files (the "Software"), to deal
@@ -532,7 +532,7 @@ object (self)
532532
let msg =
533533
"condition "
534534
^ (p2s (po_predicate_to_pretty pred))
535-
^ " delegated to the api" in
535+
^ " delegated to the api (xpr)" in
536536
Some (deps,msg)
537537
| _ -> None
538538
else
@@ -617,7 +617,7 @@ object (self)
617617
let msg =
618618
"condition "
619619
^ (p2s (po_predicate_to_pretty pred))
620-
^ " delegated to the api" in
620+
^ " delegated to the api (vinv)" in
621621
Some (deps,msg)
622622
else
623623
self#var_memoffset_deref_delegation inv#index lval memoffset

‎CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml‎

Lines changed: 166 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,18 @@
2525
SOFTWARE.
2626
============================================================================= *)
2727

28+
(* chlib *)
29+
open CHLanguage
30+
31+
(* chutil *)
32+
33+
(* xprlib *)
34+
open XprTypes
35+
2836
(* cchlib *)
2937
open CCHBasicTypes
38+
open CCHTypesToPretty
39+
open CCHTypesUtil
3040

3141
(* cchpre *)
3242
open CCHPreTypes
@@ -38,7 +48,7 @@ open CCHAnalysisTypes
3848
let x2p = XprToPretty.xpr_formatter#pr_expr
3949
let p2s = CHPrettyUtil.pretty_to_string
4050
let _x2s x = p2s (x2p x)
41-
let _e2s e = p2s (CCHTypesToPretty.exp_to_pretty e)
51+
let e2s e = p2s (CCHTypesToPretty.exp_to_pretty e)
4252

4353

4454
let _fenv = CCHFileEnvironment.file_environment
@@ -47,23 +57,171 @@ let _fenv = CCHFileEnvironment.file_environment
4757
class locally_initialized_checker_t
4858
(poq: po_query_int)
4959
(vinfo: varinfo)
50-
(_lval: lval)
51-
(_invs: invariant_int list) =
60+
(lval: lval)
61+
(invs: invariant_int list) =
5262
object (self)
5363

5464
method private vinfo = vinfo
5565

66+
method private get_symbol_name (s: symbol_t) =
67+
s#getBaseName
68+
^ (match s#getAttributes with
69+
| [] -> ""
70+
| l -> "(" ^ (String.concat "" l) ^ ")")
71+
72+
method private xpr_implies_safe (invindex: int) (x: xpr_t) =
73+
if poq#is_api_expression x then
74+
let _ =
75+
poq#set_diagnostic_arg
76+
2 ("api expression: " ^ (e2s (poq#get_api_expression x))) in
77+
match poq#get_api_expression x with
78+
| Lval (Mem (Lval (Var vpar, NoOffset)), NoOffset)
79+
when not ((fst vpar) = vinfo.vname) ->
80+
let deps = DLocal ([invindex]) in
81+
let msg =
82+
("value of " ^ (p2s (lval_to_pretty lval))
83+
^ " is not obtained from dereferencing parameter "
84+
^ vinfo.vname
85+
^ ", but from a different parameter: "
86+
^ (fst vpar)) in
87+
Some (deps, msg)
88+
| _ -> None
89+
else
90+
None
91+
92+
method private inv_implies_safe (inv: invariant_int) =
93+
match inv#expr with
94+
| Some x -> self#xpr_implies_safe inv#index x
95+
| _ ->
96+
match inv#get_fact with
97+
| NonRelationalFact (_, FInitializedSet l) ->
98+
let localAssigns =
99+
List.filter (fun s -> not (s#getBaseName = "parameter")) l in
100+
(match localAssigns with
101+
| [] -> None
102+
| _ ->
103+
let deps = DLocal [inv#index] in
104+
let msg =
105+
"local assignment(s): "
106+
^ (String.concat
107+
"_xx_" (List.map self#get_symbol_name localAssigns)) in
108+
Some (deps, msg))
109+
| _ -> None
110+
111+
method private check_invs_safe =
112+
match invs with
113+
| [] -> false
114+
| _ ->
115+
List.fold_left (fun acc inv ->
116+
acc ||
117+
match self#inv_implies_safe inv with
118+
| Some (deps, msg) ->
119+
begin
120+
poq#record_safe_result deps msg;
121+
true
122+
end
123+
| _ -> false) false invs
124+
125+
method private xpr_implies_violation (invindex: int) (x: xpr_t) =
126+
if poq#is_api_expression x then
127+
let _ =
128+
poq#set_diagnostic_arg
129+
2 ("api expression: " ^ (e2s (poq#get_api_expression x))) in
130+
match poq#get_api_expression x with
131+
| Lval (Mem (Lval (Var vpar, NoOffset)), NoOffset)
132+
when (fst vpar) = vinfo.vname ->
133+
let deps = DLocal ([invindex]) in
134+
let msg =
135+
("value of " ^ (p2s (lval_to_pretty lval))
136+
^ " is obtained from dereferencing parameter "
137+
^ (fst vpar)) in
138+
Some (deps, msg)
139+
140+
| _ -> None
141+
else
142+
None
143+
144+
method private inv_implies_violation (inv: invariant_int) =
145+
match inv#expr with
146+
| Some x -> self#xpr_implies_violation inv#index x
147+
| _ -> None
148+
149+
method private vinv_implies_deref_offset_violation
150+
(inv: invariant_int) (memoffset: offset) =
151+
match inv#expr with
152+
| Some x when poq#is_api_expression x ->
153+
begin
154+
match poq#get_api_expression x with
155+
| Lval lval ->
156+
if is_constant_offset memoffset then
157+
let memlval = (Mem (Lval lval), memoffset) in
158+
let deps = DLocal ([inv#index]) in
159+
let msg =
160+
"initialized from parameter "
161+
^ (p2s (lval_to_pretty memlval))
162+
^ " with offset "
163+
^ (p2s (offset_to_pretty memoffset)) in
164+
Some (deps, msg)
165+
else
166+
None
167+
| _ ->
168+
None
169+
end
170+
| _ -> None
171+
172+
method private check_lval_deref_violation (memlval: lval) (memoffset: offset) =
173+
match memlval with
174+
| (Var (vname, vid), NoOffset) when vid > 0 && vinfo.vname = vname ->
175+
let vinfovalues = poq#get_vinfo_offset_values vinfo in
176+
List.fold_left (fun acc (inv, offset) ->
177+
acc
178+
|| match offset with
179+
| NoOffset ->
180+
begin
181+
match self#vinv_implies_deref_offset_violation
182+
inv memoffset with
183+
| Some (deps, msg) ->
184+
begin
185+
poq#record_violation_result deps msg;
186+
true
187+
end
188+
| _ -> false
189+
end
190+
| _ -> false) false vinfovalues
191+
| _ -> false
192+
193+
method private check_lval_violation =
194+
match lval with
195+
| (Mem (Lval memlval), memoffset) ->
196+
self#check_lval_deref_violation memlval memoffset
197+
| _ -> false
198+
199+
method private check_invs_violation =
200+
match invs with
201+
| [] -> false
202+
| _ ->
203+
List.fold_left (fun acc inv ->
204+
acc ||
205+
match self#inv_implies_violation inv with
206+
| Some (deps, msg) ->
207+
begin
208+
poq#record_violation_result deps msg;
209+
true
210+
end
211+
| _ -> false) false invs
212+
56213
method check_safe =
57-
let _ = poq#set_vinfo_diagnostic_invariants self#vinfo in
58-
false
214+
self#check_invs_safe
59215

60-
method check_violation = false
216+
method check_violation =
217+
self#check_invs_violation || self#check_lval_violation
61218

62219
end
63220

64221

65222
let check_locally_initialized (poq:po_query_int) (vinfo: varinfo) (lval:lval) =
66-
let invs = poq#get_invariants 1 in
67-
let _ = poq#set_diagnostic_invariants 1 in
223+
let invs = poq#get_invariants 2 in
224+
let _ = poq#set_diagnostic_invariants 2 in
225+
let _ = poq#set_init_vinfo_mem_diagnostic_invariants vinfo (snd lval) in
68226
let checker = new locally_initialized_checker_t poq vinfo lval invs in
69227
checker#check_safe || checker#check_violation

0 commit comments

Comments
 (0)