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/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 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 | _ -> 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"