CHC: A number of fixes for command line arguments handling

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

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
 

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

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

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

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

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

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

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

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"