Make user input non-deterministic

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

regression/overflows/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+FLAGS = --verbosity 10
+
+test:
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+tests.log: ../test.pl
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@rm -f *.log
+	@for dir in *; do rm -f $$dir/*.out; done;

regression/overflows/scanf-overflow-bad/main.c

@@ -0,0 +1,28 @@
+// Inspired by SV-comp:
+// https://sv-comp.sosy-lab.org/2023/results/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad.i
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+void printLine(const char * line);
+void printLongLine(long longNumber);
+
+void CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad()
+{
+    int64_t data;
+    data = 0LL;
+    fscanf (stdin, "%" "l" "d", &data);
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+}
+int main(int argc, char * argv[])
+{
+    srand( (unsigned)time(((void *)0)) );
+    printLine("Calling bad()...");
+    CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad();
+    printLine("Finished bad()");
+    return 0;
+}

regression/overflows/scanf-overflow-bad/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/overflows/scanf-overflow-good/main.c

@@ -0,0 +1,49 @@
+// Inspired by SV-comp:
+// https://sv-comp.sosy-lab.org/2023/results/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_good.i
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+void printLine(const char * line);
+void printLongLine(long longNumber);
+void printLongLongLine(int64_t longLongIntNumber);
+
+static void goodG2B()
+{
+    int64_t data;
+    data = 0LL;
+    data = 2;
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+}
+static void goodB2G()
+{
+    int64_t data;
+    data = 0LL;
+    fscanf (stdin, "%" "l" "d", &data);
+    if (data < 0x7fffffffffffffffLL)
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+    else
+    {
+        printLine("data value is too large to perform arithmetic safely.");
+    }
+}
+void CWE190_Integer_Overflow__int64_t_fscanf_add_01_good()
+{
+    goodG2B();
+    goodB2G();
+}
+int main(int argc, char * argv[])
+{
+    srand( (unsigned)time(((void *)0)) );
+    printLine("Calling good()...");
+    CWE190_Integer_Overflow__int64_t_fscanf_add_01_good();
+    printLine("Finished good()");
+    return 0;
+}

regression/overflows/scanf-overflow-good/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

src/2ls/2ls_parse_options.cpp

@@ -1048,6 +1048,8 @@ bool twols_parse_optionst::process_goto_program(
     if(options.get_bool_option("competition-mode"))
       assert_no_builtin_functions(goto_model);
 
+    make_scanf_nondet(goto_model);
+
 #if REMOVE_MULTIPLE_DEREFERENCES
     remove_multiple_dereferences(goto_model);
 #endif

src/2ls/2ls_parse_options.h

@@ -190,6 +190,7 @@ class twols_parse_optionst:
   void fix_goto_targets(goto_modelt &goto_model);
   void make_assertions_false(goto_modelt &goto_model);
   void make_symbolic_array_indices(goto_modelt &goto_model);
+  void make_scanf_nondet(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/preprocessing_util.cpp

@@ -849,3 +849,44 @@ void twols_parse_optionst::make_symbolic_array_indices(goto_modelt &goto_model)
   }
   goto_model.goto_functions.update();
 }
+
+/// Makes user input nondeterministic, i.e. arguments of fscanf starting
+/// from the second one are assigned a nondeterministic value.
+void twols_parse_optionst::make_scanf_nondet(goto_modelt &goto_model)
+{
+  for(auto &f_it : goto_model.goto_functions.function_map)
+  {
+    Forall_goto_program_instructions(i_it, f_it.second.body)
+    {
+      if(!i_it->is_function_call())
+        continue;
+      auto name = to_symbol_expr(i_it->call_function()).get_identifier();
+      // FIXME: this is a bit hacky and should probably be handled better in
+      //        coordination with CBMC.
+      int start;
+      if(name == "__isoc99_fscanf" || name == "fscanf")
+        start = 2;
+      else if(name == "__isoc99_scanf" || name == "scanf")
+        start = 1;
+      else
+        continue;
+      int i = 0;
+      for(const auto &arg : i_it->call_arguments()) {
+        if(i >= start)
+        {
+          if(arg.id() == ID_address_of)
+          {
+            auto lhs=dereference_exprt(arg);
+            side_effect_expr_nondett rhs(
+              to_address_of_expr(arg).object().type(),
+              i_it->source_location());
+            f_it.second.body.insert_after(
+              i_it,
+              goto_programt::make_assignment(lhs, rhs));
+          }
+        }
+        i++;
+      }
+    }
+  }
+}