Merge pull request #5079 from owen-mc-diffblue/owen/fix-json-parsing-bug

[TG-9218] Fix parsing of escaped characters in json

Author: owen-mc-diffblue

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.class

@@ -12,7 +12,8 @@ public static void testIntFail() {
   public static char asciiCharField = 'a';
   public static char hexCharField = '\u0001';
   public static char chineseCharField = '字';
-  public static char specialCharField = '\n';
+  public static char newLineCharField = '\n';
+  public static char specialCharField = '\\';
   public static char fibCharField = (char) Util.fib(15);
   public static void testAsciiCharPass() {
     assert asciiCharField == 'a';
@@ -32,12 +33,10 @@ public static void testChineseCharPass() {
   public static void testChineseCharFail() {
     assert chineseCharField != '字';
   }
-  public static void testSpecialCharPass() {
-    assert specialCharField == '\n';
-  }
-  public static void testSpecialCharFail() {
-    assert specialCharField != '\n';
-  }
+  public static void testNewLineCharPass() { assert newLineCharField == '\n'; }
+  public static void testNewLineCharFail() { assert newLineCharField != '\n'; }
+  public static void testSpecialCharPass() { assert specialCharField == '\\'; }
+  public static void testSpecialCharFail() { assert specialCharField != '\\'; }
   public static void testFibCharPass() {
     assert fibCharField == 'ɢ';
   }

jbmc/regression/jbmc/deterministic_assignments_json/StaticValues.java

@@ -343,10 +343,14 @@
         "x":4
       }
     },
-    "specialCharField":{
+    "newLineCharField":{
       "@type":"java.lang.Character",
       "value":"\n"
     },
+    "specialCharField":{
+      "@type":"java.lang.Character",
+      "value":"\\"
+    },
     "hexCharField":{
       "@type":"java.lang.Character",
       "value":"\u0001"

jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testNewLineCharFail
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_new_line_char_fail.desc

@@ -0,0 +1,8 @@
+CORE
+StaticValues.class
+--unwind 1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --static-values clinit-state.json --function StaticValues.testNewLineCharPass
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc/deterministic_assignments_json/test_new_line_char_pass.desc

@@ -1,5 +1,9 @@
 %{
 // Strictly follows http://www.json.org/
+//
+// The rule for char and its dependencies is based on
+//   https://gist.github.com/justjkk/436828
+// which is MIT-licensed (retrieved on 2019-09-03)
 %}
 
 %option 8bit nodefault
@@ -33,7 +37,11 @@
 
 string  \"\"|\"{chars}\"
 chars   {char}+
-char    [^\"]|\\\"
+unescapedchar [^"\\]
+escapedchar   \\["\\/bfnrt]
+hexdigit      [0-9a-fA-F]
+unicodechar   \\u{hexdigit}{hexdigit}{hexdigit}{hexdigit}
+char          {unescapedchar}|{escapedchar}|{unicodechar}
 
 number  {int}|{int}{frac}|{int}{exp}|{int}{frac}{exp}
 int     {digit}|{digit19}{digits}|-{digit}|-{digit19}{digits}

src/json/scanner.l

@@ -132,6 +132,65 @@ SCENARIO("Loading JSON files")
       }
     }
   }
+  GIVEN("A JSON file containing escaped characters")
+  {
+    temporary_filet unicode_json_file("cbmc_unit_json_parser_escaped", ".json");
+    const std::string unicode_json_path = unicode_json_file();
+    {
+      std::ofstream unicode_json_out(unicode_json_path);
+      unicode_json_out << "{\n"
+                       << "  \"doublequote\": \"\\\"\",\n"
+                       << "  \"backslash\": \"\\\\\",\n"
+                       << "  \"slash\": \"\\/\",\n"
+                       << "  \"backspace\": \"\\b\",\n"
+                       << "  \"formfeed\": \"\\f\",\n"
+                       << "  \"newline\": \"\\n\",\n"
+                       << "  \"return\": \"\\r\",\n"
+                       << "  \"tab\": \"\\t\",\n"
+                       << "  \"several\": \"\\\"\\\\\\/\\b\\f\\n\\r\\t\"\n"
+                       << "}\n";
+    }
+    WHEN("Loading the JSON file with the escaped characters")
+    {
+      jsont unicode_json;
+      const auto unicode_parse_error =
+        parse_json(unicode_json_path, null_message_handler, unicode_json);
+      THEN("The JSON file should be parsed correctly")
+      {
+        REQUIRE_FALSE(unicode_parse_error);
+        REQUIRE(unicode_json.is_object());
+
+        const json_objectt &json_object = to_json_object(unicode_json);
+
+        REQUIRE(json_object.find("doublequote") != json_object.end());
+        REQUIRE(json_object["doublequote"].value == "\"");
+
+        REQUIRE(json_object.find("backslash") != json_object.end());
+        REQUIRE(json_object["backslash"].value == "\\");
+
+        REQUIRE(json_object.find("slash") != json_object.end());
+        REQUIRE(json_object["slash"].value == "/");
+
+        REQUIRE(json_object.find("backspace") != json_object.end());
+        REQUIRE(json_object["backspace"].value == "\b");
+
+        REQUIRE(json_object.find("formfeed") != json_object.end());
+        REQUIRE(json_object["formfeed"].value == "\f");
+
+        REQUIRE(json_object.find("newline") != json_object.end());
+        REQUIRE(json_object["newline"].value == "\n");
+
+        REQUIRE(json_object.find("return") != json_object.end());
+        REQUIRE(json_object["return"].value == "\r");
+
+        REQUIRE(json_object.find("tab") != json_object.end());
+        REQUIRE(json_object["tab"].value == "\t");
+
+        REQUIRE(json_object.find("several") != json_object.end());
+        REQUIRE(json_object["several"].value == "\"\\/\b\f\n\r\t");
+      }
+    }
+  }
 }
 
 TEST_CASE("json equality", "[core][util][json]")