From 282df6887d8da255707059e42f4340e0dabc50c5 Mon Sep 17 00:00:00 2001 From: Ricardo Baratto Date: Tue, 29 Apr 2025 16:35:45 -0400 Subject: [PATCH 1/3] CHC: Close POs that refer to argv[0] We already had some logic to deal with this but not for all pointer cases. I copy/pasted that logic over to the cases where the current version of CHC complains for a simple hello world program that passes argv[0] to printf. There's still an open issue where there's a precondition for 'initialized(*argv)' that I have not addressed --- CodeHawk/CHC/cchpre/cCHCheckValid.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CodeHawk/CHC/cchpre/cCHCheckValid.ml b/CodeHawk/CHC/cchpre/cCHCheckValid.ml index 9b8df1ed..f24cbdb9 100644 --- a/CodeHawk/CHC/cchpre/cCHCheckValid.ml +++ b/CodeHawk/CHC/cchpre/cCHCheckValid.ml @@ -1510,6 +1510,11 @@ let check_ppo_validity | _ -> () end + | PPtrUpperBound (_, _, e, _) when is_program_name e -> + make + ("validity of pointer to program name is guaranteed by the " + ^ "operating system") + | PPtrUpperBound (_, _, e, _) when is_null_pointer e -> make ("not-null of first argument is checked separately") @@ -2062,6 +2067,11 @@ let check_ppo_validity | PInitialized (Mem e, NoOffset) when is_constant_string e -> make ("constant string is guaranteed to have at least one character") + | PInitializedRange (e, _) when is_program_name e -> + make + ("validity of pointer to program name is guaranteed by the " + ^ "operating system") + | PInitializedRange (e, _) when is_null_pointer e -> make "null pointer does have any range, so this is trivially valid" @@ -2150,6 +2160,11 @@ let check_ppo_validity | PNullTerminated (Const (CWStr _)) | PNullTerminated (CastE (_, Const (CWStr _))) -> make "wide string literal" + | PNullTerminated e when is_program_name e -> + make + ("validity of pointer to program name is guaranteed by the " + ^ "operating system") + | PNullTerminated e when is_null_pointer e -> make "null pointer is not subject to null-termination" From 3d0495a9057659b3d143c5d0575c7c5736bcf8ee Mon Sep 17 00:00:00 2001 From: Ricardo Baratto Date: Wed, 30 Apr 2025 09:28:31 -0400 Subject: [PATCH 2/3] CHC: Address precondition on 'initialized(*argv)' for a simple hello world program I couldn't figure out how to do it within the cCHCheckValid.ml match logic so I added the logic to the actual initialized checker. It now has a specific path that figures out if what we're looking at is argv[0] and marks it safe, closes the PO, and does not mark it for delegation. Probably not the cleanest solution, but it will do for now. --- .../CHC/cchanalyze/cCHPOCheckInitialized.ml | 31 ++++++++++++++++--- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml index d1cae456..8666e2b1 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitialized.ml @@ -71,19 +71,37 @@ class initialized_checker_t (poq:po_query_int) (lval:lval) (invs:invariant_int list) = object (self) + method private check_program_name = + if poq#is_command_line_argument (Lval lval) then + let index = poq#get_command_line_argument_index (Lval lval) in + if index == 0 then + begin + (* first index into argv is always safe, it is the program name *) + poq#record_safe_result + (DLocal []) + ("command-line argument " + ^ (string_of_int index) + ^ " is guaranteed initialized by the operating system"); + true + end + else + false + else + false + method private check_command_line_argument = if poq#is_command_line_argument (Lval lval) then let index = poq#get_command_line_argument_index (Lval lval) in match poq#get_command_line_argument_count with - | Some (inv,i) -> - if index < i then + | Some (inv, arg_count) -> + if index < arg_count then begin poq#record_safe_result (DLocal [inv]) ("command-line argument " ^ (string_of_int index) ^ " is guaranteed initialized for argument count " - ^ (string_of_int i)); + ^ (string_of_int arg_count)); true end else @@ -93,7 +111,7 @@ object (self) ("command-line argument " ^ (string_of_int index) ^ " is not included in argument count of " - ^ (string_of_int i)); + ^ (string_of_int arg_count)); true end | _ -> @@ -654,7 +672,10 @@ object (self) | _ -> false method check_delegation = - self#check_invs_delegation || self#check_lval_delegation + if self#check_program_name then + false + else + self#check_invs_delegation || self#check_lval_delegation end From 685ec83d69d01f76c3da520455ea82904e00a232 Mon Sep 17 00:00:00 2001 From: Ricardo Baratto Date: Wed, 30 Apr 2025 09:56:56 -0400 Subject: [PATCH 3/3] 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 \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 *)) | -------------------------------------------------------------------------------- --- CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml | 15 ++++++ .../cchanalyze/cCHPOCheckInitializedRange.ml | 14 +++++ .../CHC/cchanalyze/cCHPOCheckLowerBound.ml | 15 ++++++ CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml | 53 ++++++------------- .../cchanalyze/cCHPOCheckNullTerminated.ml | 15 ++++++ .../CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml | 15 ++++++ .../CHC/cchanalyze/cCHPOCheckUpperBound.ml | 15 ++++++ CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml | 17 +++++- 8 files changed, 120 insertions(+), 39 deletions(-) diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml index 91255d40..727c4a3b 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInScope.ml @@ -230,6 +230,21 @@ object (self) r method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to be in scope" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate scope of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml index ecf3a21b..fb5608cf 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckInitializedRange.ml @@ -320,6 +320,20 @@ object (self) | _ -> None method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed initialized for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate initialization of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e1 safemsg vmsg dmsg || match self#unsigned_length_conflict with | Some _ -> false | _ -> diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml index 3138b576..344a15ad 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckLowerBound.ml @@ -198,6 +198,21 @@ object (self) | _ -> None method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to be valid to access" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate access of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml index 231ded83..7e7c63bf 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckNotNull.ml @@ -76,43 +76,6 @@ object (self) (* ----------------------------- safe ------------------------------------- *) - method private command_line_argument = - if poq#is_command_line_argument e then - let index = poq#get_command_line_argument_index e in - match poq#get_command_line_argument_count with - | Some (inv, i) -> - if index < i then - begin - poq#record_safe_result - (DLocal [inv]) - ("command-line argument " - ^ (string_of_int index) - ^ " is guaranteed not null for argument count " - ^ (string_of_int i)); - true - end - else - begin - poq#record_violation_result - (DLocal [inv]) - ("command-line argument " - ^ (string_of_int index) - ^ " is not included in argument count of " - ^ (string_of_int i)); - true - end - | _ -> - begin - poq#set_diagnostic - ("no invariant found for argument count; " - ^ "unable to validate access of " - ^ "command-line argument " - ^ (string_of_int index)); - false - end - else - false - method private global_expression_safe (invindex: int) (x: xpr_t) = let pred = PNotNull (poq#get_global_expression x) in match poq#check_implied_by_assumptions pred with @@ -314,7 +277,21 @@ object (self) r method check_safe = - self#command_line_argument + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed not null" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate not-null of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg || (List.fold_left (fun acc inv -> acc || match self#inv_implies_safe inv with diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml index de723a01..982c520a 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckNullTerminated.ml @@ -166,6 +166,21 @@ object (self) | _ -> None method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to be null-termianted" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate null-termination of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml index 18b88ff4..a8363eb9 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckPtrUpperBound.ml @@ -455,6 +455,21 @@ object (self) | _ -> false) acc1 invs2) false invs1 method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to be valid to access" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate access of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e1 safemsg vmsg dmsg || match self#null_terminated_string_implies_pluspi_safe with | Some (deps,msg) -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml index 5f17495b..f754f58f 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckUpperBound.ml @@ -181,6 +181,21 @@ object (self) | Some l -> self#xprlist_implies_safe inv#index l method check_safe = + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to be valid to access" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate access of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg || match invs with | [] -> begin diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml index fb9da592..aedc0ce6 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckValidMem.ml @@ -447,7 +447,22 @@ object (self) r method check_safe = - self#global_free + let safemsg = fun index arg_count -> ("command-line argument" + ^ (string_of_int index) + ^ " is guaranteed to have valid memory" + ^ " for argument count " + ^ (string_of_int arg_count)) in + let vmsg = fun index arg_count -> ("command-line argument " + ^ (string_of_int index) + ^ " is not included in argument count of " + ^ (string_of_int arg_count)) in + let dmsg = fun index -> ("no invariant found for argument count; " + ^ "unable to validate memory validity of " + ^ "command-line argument " + ^ (string_of_int index)) in + + poq#check_command_line_argument e safemsg vmsg dmsg + || self#global_free || (match invs with | [] -> false | _ ->