Skip to content

Commit 07b782c

Browse files
sipmasipma
committed
CHC: attribute conversion to pre/post conditions
1 parent 3149231 commit 07b782c

File tree

2 files changed

+572
-0
lines changed

2 files changed

+572
-0
lines changed

‎CodeHawk/CHC/cchlib/cCHCAttributes.ml‎

Lines changed: 195 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,195 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2024 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* chutil *)
29+
open CHTimingLog
30+
31+
(* cchlib *)
32+
open CCHBasicTypes
33+
open CCHLibTypes
34+
open CCHTypesToPretty
35+
36+
37+
let convert_attribute_to_function_conditions
38+
(name: string)
39+
(attr: attribute):(xpredicate_t list * xpredicate_t list * xpredicate_t list) =
40+
41+
let arg (i: int) = ArgValue (ParFormal i, ArgNoOffset) in
42+
43+
match attr with
44+
| Attr (("access" | "chkc_access"), attrparams) ->
45+
let (pre, side) =
46+
(match attrparams with
47+
| [ACons ("read_only", []); AInt refindex] ->
48+
([XBuffer (arg refindex, RuntimeValue)], [])
49+
50+
| [ACons ("read_only", []); AInt refindex; AInt sizeindex] ->
51+
([XBuffer (arg refindex, arg sizeindex)], [])
52+
53+
| [ACons (("write_only" | "read_write"), []); AInt refindex] ->
54+
([XBuffer (arg refindex, RuntimeValue)],
55+
[XBlockWrite (arg refindex, RuntimeValue)])
56+
57+
| [ACons (("write_only" | "read_write"), []);
58+
AInt refindex; AInt sizeindex] ->
59+
([XBuffer (arg refindex, arg sizeindex)],
60+
[XBlockWrite (arg refindex, arg sizeindex)])
61+
62+
| _ ->
63+
begin
64+
log_info
65+
"attribute conversion for %s: attribute parameters %s not recognized"
66+
name
67+
(String.concat ", " (List.map attrparam_to_string attrparams));
68+
([], [])
69+
end) in
70+
71+
(pre, [], side)
72+
73+
| Attr ("aconst", []) ->
74+
([], [XFunctional], [XFunctional])
75+
76+
| Attr ("format", attrparams) ->
77+
let pre =
78+
(match attrparams with
79+
| [ACons ("printf", []); AInt stringindex; AInt _firsttocheck] ->
80+
[XOutputFormatString (arg stringindex)]
81+
| [ACons ("scanf", []); AInt stringindex; AInt _firsttocheck] ->
82+
[XInputFormatString (arg stringindex)]
83+
| _ ->
84+
begin
85+
log_info
86+
"attribute conversion for %s: attribute parameters %s not recognized"
87+
name
88+
(String.concat ", " (List.map attrparam_to_string attrparams));
89+
[]
90+
end) in
91+
(pre, [], [])
92+
93+
| Attr ("malloc", attrparams) ->
94+
let post =
95+
(match attrparams with
96+
| []
97+
| [ACons ("free", [])]
98+
| [ACons ("free", []); AInt 1]->
99+
[XNewMemory ReturnValue;
100+
XHeapAddress ReturnValue;
101+
XAllocationBase ReturnValue]
102+
| _ ->
103+
begin
104+
log_info
105+
"attribute conversion for %s: attribute parameters %s not recognized"
106+
name
107+
(String.concat ", " (List.map attrparam_to_string attrparams));
108+
[]
109+
end) in
110+
([], post, [])
111+
112+
| Attr ("nonnull", attrparams) ->
113+
let pre =
114+
List.fold_left (fun acc attrparam ->
115+
match attrparam with
116+
| AInt i -> (XNotNull (arg i)) :: acc
117+
| _ ->
118+
begin
119+
log_info
120+
("attribute conversion for %s: parameter %s not recognized "
121+
^^ "(excluded)")
122+
name
123+
(attrparam_to_string attrparam);
124+
acc
125+
end) [] attrparams in
126+
(pre, [], [])
127+
128+
| Attr ("noreturn", []) ->
129+
([], [XFalse], [])
130+
131+
| Attr ("null_terminated_string_arg", attrparams) ->
132+
let pre =
133+
List.fold_left (fun acc attrparam ->
134+
match attrparam with
135+
| AInt i -> (XNullTerminated (arg i)) :: acc
136+
| _ ->
137+
begin
138+
log_info
139+
("attribute conversion for %s: parameter %s not recognized "
140+
^^ "(excluded)")
141+
name
142+
(attrparam_to_string attrparam);
143+
acc
144+
end) [] attrparams in
145+
(pre, [], [])
146+
147+
| Attr ("pure", []) ->
148+
([], [], [XPreservesAllMemory; XPreservesNullTermination])
149+
150+
| Attr ("returns_nonnull", []) ->
151+
([], [XNotNull ReturnValue], [])
152+
153+
| Attr ("chkc_returns_null_terminated_string", []) ->
154+
([], [XNullTerminated ReturnValue], [])
155+
156+
| Attr ("chkc_preserves_all_memory", []) ->
157+
([], [], [XPreservesAllMemory])
158+
159+
| Attr ("chkc_preserves_memory", attrparams) ->
160+
let se =
161+
List.fold_left (fun acc attrparam ->
162+
match attrparam with
163+
| AInt i -> (XPreservesMemory (arg i)) :: acc
164+
| _ ->
165+
begin
166+
log_info
167+
("attribute conversion for %s: parameter %s not recognized "
168+
^^ "(excluded)")
169+
name
170+
(attrparam_to_string attrparam);
171+
acc
172+
end) [] attrparams in
173+
([], [], se)
174+
175+
| _ -> ([], [], [])
176+
177+
178+
let attribute_update_globalvar_contract
179+
(gvarc: globalvar_contract_int) (attr: attribute) =
180+
match attr with
181+
| Attr ("chkc_le", [AInt i]) -> gvarc#set_upper_bound i
182+
| Attr ("chkc_lt", [AInt i]) -> gvarc#set_upper_bound (i-1)
183+
| Attr ("chkc_ge", [AInt i]) -> gvarc#set_lower_bound i
184+
| Attr ("chkc_gt", [AInt i]) -> gvarc#set_lower_bound (i+1)
185+
| Attr ("chkc_value", [AInt i]) -> gvarc#set_value i
186+
| Attr ("chkc_static", []) -> gvarc#set_static
187+
| Attr ("chkc_const", []) -> gvarc#set_const
188+
| Attr ("chkc_not_null", []) -> gvarc#set_not_null
189+
| Attr (s, attrparams) ->
190+
log_info
191+
"global variable attribute %s for %s with %d parameters not recognized"
192+
s
193+
gvarc#get_name
194+
(List.length attrparams)
195+

0 commit comments

Comments
 (0)