Skip to content

Commit f6cb7b6

Browse files
sipmasipma
committed
CHC: add output parameter predicates
1 parent f12f9af commit f6cb7b6

File tree

4 files changed

+59
-6
lines changed

4 files changed

+59
-6
lines changed

‎CodeHawk/CHC/cchpre/cCHPOPredicate.ml‎

Lines changed: 33 additions & 2 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-2023 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
@@ -60,6 +60,7 @@ let po_predicate_tag p =
6060
| PIndexLowerBound _ -> "index-lower-bound"
6161
| PIndexUpperBound _ -> "index-upper-bound"
6262
| PInitialized _ -> "initialized"
63+
| PLocallyInitialized _ -> "locally-initialized"
6364
| PInitializedRange _ -> "initialized-range"
6465
| PInScope _ -> "in-scope"
6566
| PIntOverflow _ -> "int-overflow"
@@ -92,12 +93,16 @@ let po_predicate_tag p =
9293
| PValidMem _ -> "valid-mem"
9394
| PPreservedAllMemory -> "preserved-all-memory"
9495
| PPreservedAllMemoryX _ -> "preserved-all-memory-x"
96+
| POutputParameterInitialized _ -> "outputparameter-initialized"
97+
| POutputParameterUnaltered _ -> "outputparameter-unaltered"
9598
| _ -> "misc"
9699

97100

98101
class po_predicate_walker_t =
99102
object (self)
100103

104+
method walk_varinfo (_index: int) (_v: varinfo) = ()
105+
101106
method walk_exp (_index:int) (_e:exp) = ()
102107

103108
method walk_type (_index:int) (_t:typ) = ()
@@ -119,6 +124,7 @@ object (self)
119124
let we = self#walk_exp in
120125
let wt = self#walk_type in
121126
let wl = self#walk_lval in
127+
let wv = self#walk_varinfo in
122128
match p with
123129
| PNotNull e | PNull e | PValidMem e | PInScope e
124130
| PControlledResource (_, e)
@@ -138,6 +144,11 @@ object (self)
138144
we 2 e2
139145
end
140146
| PInitialized l -> wl 1 l
147+
| PLocallyInitialized (v, l) ->
148+
begin
149+
wv 1 v;
150+
wl 2 l;
151+
end
141152
| PStackAddressEscape (None,e) -> we 2 e
142153
| PStackAddressEscape (Some l,e) ->
143154
begin
@@ -235,6 +246,8 @@ object (self)
235246
| PPreservedAllMemory -> ()
236247
| PPreservedAllMemoryX l -> List.iteri (fun i e -> we (i+1) e) l
237248
| PContractObligation _ -> ()
249+
| POutputParameterInitialized v -> wv 1 v
250+
| POutputParameterUnaltered v -> wv 1 v
238251

239252
end
240253

@@ -364,7 +377,14 @@ let po_predicate_to_full_pretty p =
364377
| PIndexUpperBound (e1, e2) ->
365378
LBLOCK [exp_to_pretty e1; STR " < "; exp_to_pretty e2]
366379
| PInitialized lval ->
367-
LBLOCK [STR "initialized("; lval_to_pretty lval; STR ")"]
380+
LBLOCK [STR "initialized("; lval_to_pretty lval; STR ")"]
381+
| PLocallyInitialized (vinfo, lval) ->
382+
LBLOCK [
383+
STR "locally-initialized(";
384+
STR vinfo.vname;
385+
STR ",";
386+
lval_to_pretty lval;
387+
STR ")"]
368388
| PInitializedRange (base, len) ->
369389
LBLOCK [
370390
STR "initialized-range(";
@@ -615,6 +635,10 @@ let po_predicate_to_full_pretty p =
615635
STR "preserved-all-memory-x";
616636
pretty_print_list l exp_to_pretty "(" "," ")"]
617637
| PContractObligation s -> LBLOCK [STR "contract-obligation:"; STR s]
638+
| POutputParameterInitialized vinfo ->
639+
LBLOCK [STR "outputparameter-initialized("; STR vinfo.vname; STR ")"]
640+
| POutputParameterUnaltered vinfo ->
641+
LBLOCK [STR "outputparameter-unaltered("; STR vinfo.vname; STR ")"]
618642

619643

620644
let pr_expr op e1 e2 t = exp_to_pretty (BinOp (op, e1, e2,t ))
@@ -659,6 +683,9 @@ let po_predicate_to_pretty ?(full=false) (p:po_predicate_t) =
659683
| PIndexUpperBound (e1, e2) ->
660684
LBLOCK [STR "index-upperbound("; pe e1; STR ","; pe e2; STR ")"]
661685
| PInitialized lval -> LBLOCK [STR "initialized("; pl lval; STR ")"]
686+
| PLocallyInitialized (vinfo, lval) ->
687+
LBLOCK [
688+
STR "locally-initialized("; STR vinfo.vname; STR ","; pl lval; STR ")"]
662689
| PInitializedRange (base, len) ->
663690
LBLOCK [STR "initialized-range("; pe base; STR ", "; pe len; STR ")"]
664691
| PCast (fromt, tot, e) ->
@@ -837,6 +864,10 @@ let po_predicate_to_pretty ?(full=false) (p:po_predicate_t) =
837864
STR "preserved-all-memory-x";
838865
pretty_print_list l exp_to_pretty "(" "," ")"]
839866
| PContractObligation s -> LBLOCK [STR "contract-obligation:"; STR s]
867+
| POutputParameterInitialized vinfo ->
868+
LBLOCK [STR "outputparameter-initialized("; STR vinfo.vname; STR ")"]
869+
| POutputParameterUnaltered vinfo ->
870+
LBLOCK [STR "outputparameter-unaltered("; STR vinfo.vname; STR ")"]
840871

841872

842873
let get_global_vars_in_exp (env:cfundeclarations_int) (e:exp) =

‎CodeHawk/CHC/cchpre/cCHPreSumTypeSerializer.ml‎

Lines changed: 7 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-2023 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
@@ -179,12 +179,16 @@ object
179179
| PRevBuffer _ -> "rb"
180180
| PNewMemory _ -> "nm"
181181
| PDistinctRegion _ -> "dr"
182+
| PLocallyInitialized _ -> "li"
183+
| POutputParameterInitialized _ -> "opi"
184+
| POutputParameterUnaltered _ -> "opu"
182185

183186
method! tags = [
184187
"ab"; "b"; "c"; "cb"; "cbt"; "cf"; "cob"; "cr"; "cssl"; "cssu"; "csul";
185188
"csuu"; "ctt"; "cus"; "cuu"; "dr"; "ds"; "fc"; "ft"; "ga"; "ha"; "ilb";
186-
"i"; "io"; "ir"; "is"; "iu"; "iub"; "lb"; "nm"; "nn"; "nneg"; "no";
187-
"nt"; "null"; "pc"; "plb"; "pm"; "prm"; "prmx"; "pub"; "pubd"; "pv";
189+
"i"; "io"; "ir"; "is"; "iu"; "iub"; "li"; "lb"; "nm"; "nn"; "nneg"; "no";
190+
"nt"; "null"; "opi"; "opu";
191+
"pc"; "plb"; "pm"; "prm"; "prmx"; "pub"; "pubd"; "pv";
188192
"rb"; "sae"; "tao"; "ub"; "uio"; "uiu"; "up"; "va"; "vc"; "vm"; "w";
189193
"z"]
190194

‎CodeHawk/CHC/cchpre/cCHPreTypes.mli‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -860,6 +860,15 @@ type po_predicate_t =
860860
| PDistinctRegion of exp * int
861861
(** memref index is distinct from the region pointed to by exp *)
862862

863+
| PLocallyInitialized of varinfo * lval
864+
(** lval is initialized locally or distinct from the region pointed to by varinfo *)
865+
866+
| POutputParameterInitialized of varinfo
867+
(** the memory region pointed to by varinfo is fully initialized *)
868+
869+
| POutputParameterUnaltered of varinfo
870+
(** the memory region pointed to by varinfo is unaltered *)
871+
863872

864873
type violation_severity_t =
865874
| UndefinedBehavior

‎CodeHawk/CHC/cchpre/cCHPredicateDictionary.ml‎

Lines changed: 10 additions & 1 deletion
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 Henny B. Sipma
9-
Copyright (c) 2021-2024 Aarno Labs LLC
9+
Copyright (c) 2021-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
@@ -46,9 +46,11 @@ open CCHPreTypes
4646
module H = Hashtbl
4747

4848

49+
let cdecls = CCHDeclarations.cdeclarations
4950
let cd = CCHDictionary.cdictionary
5051
let id = CCHInterfaceDictionary.interface_dictionary
5152

53+
5254
let raise_tag_error (name:string) (tag:string) (accepted:string list) =
5355
let msg =
5456
LBLOCK [
@@ -95,6 +97,8 @@ object (self)
9597
| PIndexLowerBound e -> (tags,[cd#index_exp e])
9698
| PIndexUpperBound (e1,e2) -> (tags,[cd#index_exp e1; cd#index_exp e2])
9799
| PInitialized v -> (tags,[cd#index_lval v])
100+
| PLocallyInitialized (vinfo, v) ->
101+
(tags, [cdecls#index_varinfo vinfo; cd#index_lval v])
98102
| PInitializedRange (e1, e2) -> (tags,[cd#index_exp e1; cd#index_exp e2])
99103
| PCast (tfrom, tto, e)
100104
| PPointerCast(tfrom, tto, e)
@@ -143,6 +147,8 @@ object (self)
143147
| PBuffer (e1, e2) -> (tags, [cd#index_exp e1; cd#index_exp e2])
144148
| PRevBuffer (e1, e2) -> (tags, [cd#index_exp e1; cd#index_exp e2])
145149
| PDistinctRegion (e, i) -> (tags, [cd#index_exp e; i])
150+
| POutputParameterInitialized vinfo -> (tags, [cdecls#index_varinfo vinfo])
151+
| POutputParameterUnaltered vinfo -> (tags, [cdecls#index_varinfo vinfo])
146152
in
147153
po_predicate_table#add key
148154

@@ -167,6 +173,7 @@ object (self)
167173
| "ilb" -> PIndexLowerBound (cd#get_exp (a 0))
168174
| "iub" -> PIndexUpperBound (cd#get_exp (a 0), cd#get_exp (a 1))
169175
| "i" -> PInitialized (cd#get_lval (a 0))
176+
| "li" -> PLocallyInitialized (cdecls#get_varinfo (a 0), cd#get_lval (a 1))
170177
| "ir" -> PInitializedRange (cd#get_exp (a 0), cd#get_exp (a 1))
171178
| "c" -> PCast (cd#get_typ (a 0), cd#get_typ (a 1), cd#get_exp (a 2))
172179
| "fc" ->
@@ -258,6 +265,8 @@ object (self)
258265
| "rb" -> PRevBuffer (cd#get_exp (a 0), cd#get_exp (a 1))
259266
| "nm" -> PNewMemory (cd#get_exp (a 0))
260267
| "dr" -> PDistinctRegion (cd#get_exp (a 0), a 1)
268+
| "opi" -> POutputParameterInitialized (cdecls#get_varinfo (a 0))
269+
| "opu" -> POutputParameterUnaltered (cdecls#get_varinfo (a 0))
261270
| s -> raise_tag_error name s po_predicate_mcts#tags
262271

263272

0 commit comments

Comments
 (0)