Merge pull request #6611 from diffblue/argc-may-be-zero

argc may be zero

Author: kroening

regression/cbmc/argc-and-argv/argc1.c

@@ -0,0 +1,13 @@
+int main(int argc, char **argv)
+{
+  // There is no guarantee that there is at least one, so this
+  // program is not memory safe.
+  int n;
+
+  for(n = 1; n < argc; n++)
+  {
+    // nothing
+  }
+
+  char *path = argv[n]; // out-of-bounds when argc == 0
+}

regression/cbmc/argc-and-argv/argc1.desc

@@ -0,0 +1,9 @@
+CORE
+argc1.c
+--bounds-check --pointer-check --unwind 0
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] line .* dereference failure: pointer outside object bounds in argv\[.*n\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/argc-and-argv/argv1.c

@@ -0,0 +1,12 @@
+int main(int main_argc, char **main_argv)
+{
+  char *x;
+
+  // there is no guarantee that there is at least one,
+  // but note that argv is NULL-terminated
+  x = main_argv[0];
+  assert(main_argc >= 0);
+
+  // last one must be NULL
+  assert(main_argv[main_argc] == 0);
+}

regression/cbmc/argv1/test.desc regression/cbmc/argc-and-argv/argv1.descregression/cbmc/argv1/test.desc renamed to regression/cbmc/argc-and-argv/argv1.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+argv1.c
 --bounds-check --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/argv1/main.c

@@ -1,11 +1,13 @@
 #include <assert.h>
 
-int main(int argc, char **argv)
+int main()
 {
   int x;
   const char *c = "Hello world";
+  _Bool dummy;
+  __CPROVER_assume(dummy);
 
-  int *p = (argc ? &x : (int *)c);
+  int *p = (dummy ? &x : (int *)c);
 
   *p = 1;
 

regression/cbmc/lhs-pointer-aliases-constant/test.c

@@ -5,7 +5,7 @@ int main(int argc, char **argv)
   assert(4 != argc);
   argc++;
   argc--;
-  assert(argc >= 1);
+  assert(argc >= 0);
   assert(argc != 4);
   argc++;
   argc--;

regression/cbmc/multiple-goto-traces/main.c

@@ -304,11 +304,15 @@ bool generate_ansi_c_start_function(
       const symbolt &argv_symbol=ns.lookup("argv'");
 
       {
-        // assume argc is at least one
-        exprt one=from_integer(1, argc_symbol.type);
+        // Assume argc is at least zero. Note that we don't assume it's
+        // at least one, since this isn't guaranteed, as exemplified by
+        // https://www.qualys.com/2022/01/25/cve-2021-4034/pwnkit.txt
+        // The C standard only guarantees "The value of argc shall be
+        // nonnegative." and "argv[argc] shall be a null pointer."
+        exprt zero = from_integer(0, argc_symbol.type);
 
         binary_relation_exprt ge(
-          argc_symbol.symbol_expr(), ID_ge, std::move(one));
+          argc_symbol.symbol_expr(), ID_ge, std::move(zero));
 
         init_code.add(code_assumet(std::move(ge)));
       }