Skip to content

Commit b7151cf

Browse files
waskyosipma
waskyo
authored and
sipma
committed
CHC: Add command-line argument handling to a number of checkers
The logic was already in both cCHPOCheckNotNull.ml and in cCHPOQuery.ml, although cCHPOCheckNotNull.ml was using its own function instead of the one in the POQuery object. This adds calls to the util function in the POQuery object and nukes the private function in CheckNotNull. With these changes, a simple hello world program no longer gets a ton of open POs: ``` int main(int argc, char **argv) { if (argc != 2) { printf("ERROR: usage: %s <name>\n", argv[0]); return 1; } printf("Hello world %s\n", argv[1]); -------------------------------------------------------------------------------- | initialized-range((*(argv + 1):((char *) *)), len:cnapp(ntp((*(argv + 1):((char *) *))))| -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | valid-mem((*(argv + 1):((char *) *))) | | [augv[call]:$fn-entry$(-1):calls]:none | -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | null-terminated((*(argv + 1):((char *) *))) | | no invariants found for *(((lval (argv) +i 1):((char*)*)) | -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | upper-bound(char,(*(argv + 1):((char *) *))) | | no invariants for *(((lval (argv) +i 1):((char*)*)) | -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | lower-bound(char,(*(argv + 1):((char *) *))) | | no invariants found for *(((lval (argv) +i 1):((char*)*)) | -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | ptr-upper-bound((*(argv + 1):((char *) *)), cnapp(ntp((*(argv + 1):((char *) *))), op:pluspi, typ: char)| -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- | in-scope((*(argv + 1):((char *) *))) | | no invariants found for *(((lval (argv) +i 1):((char*)*)) | -------------------------------------------------------------------------------- ``` There's still one open pre-condition that I haven't figured out how to close: -------------------------------------------------------------------------------- | Preconditions: | | ptr-upper-bound-deref(argv, 1, op:indexpi, typ: (char *)) | --------------------------------------------------------------------------------
1 parent 78663b7 commit b7151cf

File tree

8 files changed

+120
-39
lines changed

8 files changed

+120
-39
lines changed

‎CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -230,6 +230,21 @@ object (self)
230230
r
231231

232232
method check_safe =
233+
let safemsg = fun index arg_count -> ("command-line argument"
234+
^ (string_of_int index)
235+
^ " is guaranteed to be in scope"
236+
^ " for argument count "
237+
^ (string_of_int arg_count)) in
238+
let vmsg = fun index arg_count -> ("command-line argument "
239+
^ (string_of_int index)
240+
^ " is not included in argument count of "
241+
^ (string_of_int arg_count)) in
242+
let dmsg = fun index -> ("no invariant found for argument count; "
243+
^ "unable to validate scope of "
244+
^ "command-line argument "
245+
^ (string_of_int index)) in
246+
247+
poq#check_command_line_argument e safemsg vmsg dmsg ||
233248
match invs with
234249
| [] ->
235250
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -320,6 +320,20 @@ object (self)
320320
| _ -> None
321321

322322
method check_safe =
323+
let safemsg = fun index arg_count -> ("command-line argument"
324+
^ (string_of_int index)
325+
^ " is guaranteed initialized for argument count "
326+
^ (string_of_int arg_count)) in
327+
let vmsg = fun index arg_count -> ("command-line argument "
328+
^ (string_of_int index)
329+
^ " is not included in argument count of "
330+
^ (string_of_int arg_count)) in
331+
let dmsg = fun index -> ("no invariant found for argument count; "
332+
^ "unable to validate initialization of "
333+
^ "command-line argument "
334+
^ (string_of_int index)) in
335+
336+
poq#check_command_line_argument e1 safemsg vmsg dmsg ||
323337
match self#unsigned_length_conflict with
324338
| Some _ -> false
325339
| _ ->

‎CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -198,6 +198,21 @@ object (self)
198198
| _ -> None
199199

200200
method check_safe =
201+
let safemsg = fun index arg_count -> ("command-line argument"
202+
^ (string_of_int index)
203+
^ " is guaranteed to be valid to access"
204+
^ " for argument count "
205+
^ (string_of_int arg_count)) in
206+
let vmsg = fun index arg_count -> ("command-line argument "
207+
^ (string_of_int index)
208+
^ " is not included in argument count of "
209+
^ (string_of_int arg_count)) in
210+
let dmsg = fun index -> ("no invariant found for argument count; "
211+
^ "unable to validate access of "
212+
^ "command-line argument "
213+
^ (string_of_int index)) in
214+
215+
poq#check_command_line_argument e safemsg vmsg dmsg ||
201216
match invs with
202217
| [] ->
203218
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml‎

Lines changed: 15 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -76,43 +76,6 @@ object (self)
7676

7777
(* ----------------------------- safe ------------------------------------- *)
7878

79-
method private command_line_argument =
80-
if poq#is_command_line_argument e then
81-
let index = poq#get_command_line_argument_index e in
82-
match poq#get_command_line_argument_count with
83-
| Some (inv, i) ->
84-
if index < i then
85-
begin
86-
poq#record_safe_result
87-
(DLocal [inv])
88-
("command-line argument "
89-
^ (string_of_int index)
90-
^ " is guaranteed not null for argument count "
91-
^ (string_of_int i));
92-
true
93-
end
94-
else
95-
begin
96-
poq#record_violation_result
97-
(DLocal [inv])
98-
("command-line argument "
99-
^ (string_of_int index)
100-
^ " is not included in argument count of "
101-
^ (string_of_int i));
102-
true
103-
end
104-
| _ ->
105-
begin
106-
poq#set_diagnostic
107-
("no invariant found for argument count; "
108-
^ "unable to validate access of "
109-
^ "command-line argument "
110-
^ (string_of_int index));
111-
false
112-
end
113-
else
114-
false
115-
11679
method private global_expression_safe (invindex: int) (x: xpr_t) =
11780
let pred = PNotNull (poq#get_global_expression x) in
11881
match poq#check_implied_by_assumptions pred with
@@ -314,7 +277,21 @@ object (self)
314277
r
315278

316279
method check_safe =
317-
self#command_line_argument
280+
let safemsg = fun index arg_count -> ("command-line argument"
281+
^ (string_of_int index)
282+
^ " is guaranteed not null"
283+
^ " for argument count "
284+
^ (string_of_int arg_count)) in
285+
let vmsg = fun index arg_count -> ("command-line argument "
286+
^ (string_of_int index)
287+
^ " is not included in argument count of "
288+
^ (string_of_int arg_count)) in
289+
let dmsg = fun index -> ("no invariant found for argument count; "
290+
^ "unable to validate not-null of "
291+
^ "command-line argument "
292+
^ (string_of_int index)) in
293+
294+
poq#check_command_line_argument e safemsg vmsg dmsg
318295
|| (List.fold_left (fun acc inv ->
319296
acc ||
320297
match self#inv_implies_safe inv with

‎CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,21 @@ object (self)
166166
| _ -> None
167167

168168
method check_safe =
169+
let safemsg = fun index arg_count -> ("command-line argument"
170+
^ (string_of_int index)
171+
^ " is guaranteed to be null-termianted"
172+
^ " for argument count "
173+
^ (string_of_int arg_count)) in
174+
let vmsg = fun index arg_count -> ("command-line argument "
175+
^ (string_of_int index)
176+
^ " is not included in argument count of "
177+
^ (string_of_int arg_count)) in
178+
let dmsg = fun index -> ("no invariant found for argument count; "
179+
^ "unable to validate null-termination of "
180+
^ "command-line argument "
181+
^ (string_of_int index)) in
182+
183+
poq#check_command_line_argument e safemsg vmsg dmsg ||
169184
match invs with
170185
| [] ->
171186
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -455,6 +455,21 @@ object (self)
455455
| _ -> false) acc1 invs2) false invs1
456456

457457
method check_safe =
458+
let safemsg = fun index arg_count -> ("command-line argument"
459+
^ (string_of_int index)
460+
^ " is guaranteed to be valid to access"
461+
^ " for argument count "
462+
^ (string_of_int arg_count)) in
463+
let vmsg = fun index arg_count -> ("command-line argument "
464+
^ (string_of_int index)
465+
^ " is not included in argument count of "
466+
^ (string_of_int arg_count)) in
467+
let dmsg = fun index -> ("no invariant found for argument count; "
468+
^ "unable to validate access of "
469+
^ "command-line argument "
470+
^ (string_of_int index)) in
471+
472+
poq#check_command_line_argument e1 safemsg vmsg dmsg ||
458473
match self#null_terminated_string_implies_pluspi_safe with
459474
| Some (deps,msg) ->
460475
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,21 @@ object (self)
181181
| Some l -> self#xprlist_implies_safe inv#index l
182182

183183
method check_safe =
184+
let safemsg = fun index arg_count -> ("command-line argument"
185+
^ (string_of_int index)
186+
^ " is guaranteed to be valid to access"
187+
^ " for argument count "
188+
^ (string_of_int arg_count)) in
189+
let vmsg = fun index arg_count -> ("command-line argument "
190+
^ (string_of_int index)
191+
^ " is not included in argument count of "
192+
^ (string_of_int arg_count)) in
193+
let dmsg = fun index -> ("no invariant found for argument count; "
194+
^ "unable to validate access of "
195+
^ "command-line argument "
196+
^ (string_of_int index)) in
197+
198+
poq#check_command_line_argument e safemsg vmsg dmsg ||
184199
match invs with
185200
| [] ->
186201
begin

‎CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml‎

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -447,7 +447,22 @@ object (self)
447447
r
448448

449449
method check_safe =
450-
self#global_free
450+
let safemsg = fun index arg_count -> ("command-line argument"
451+
^ (string_of_int index)
452+
^ " is guaranteed to have valid memory"
453+
^ " for argument count "
454+
^ (string_of_int arg_count)) in
455+
let vmsg = fun index arg_count -> ("command-line argument "
456+
^ (string_of_int index)
457+
^ " is not included in argument count of "
458+
^ (string_of_int arg_count)) in
459+
let dmsg = fun index -> ("no invariant found for argument count; "
460+
^ "unable to validate memory validity of "
461+
^ "command-line argument "
462+
^ (string_of_int index)) in
463+
464+
poq#check_command_line_argument e safemsg vmsg dmsg
465+
|| self#global_free
451466
|| (match invs with
452467
| [] -> false
453468
| _ ->

0 commit comments

Comments
 (0)