diff --git a/regression/goto-diff/java-add-package/test.desc b/regression/goto-diff/java-add-package/test.desc index 84d88004486..7562b7bb7e2 100644 --- a/regression/goto-diff/java-add-package/test.desc +++ b/regression/goto-diff/java-add-package/test.desc @@ -5,8 +5,8 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n + "deletedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n "modifiedFunctions": \[ \], - "newFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], + "newFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], -- ^warning: ignoring diff --git a/regression/goto-diff/java-del-package/test.desc b/regression/goto-diff/java-del-package/test.desc index 7ef3b6f631b..2106c6a8557 100644 --- a/regression/goto-diff/java-del-package/test.desc +++ b/regression/goto-diff/java-del-package/test.desc @@ -5,8 +5,8 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], + "deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], "modifiedFunctions": \[ \], - "newFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n + "newFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)\V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n -- ^warning: ignoring diff --git a/regression/goto-diff/java-deleted-function/test.desc b/regression/goto-diff/java-deleted-function/test.desc index d68520e8038..4aa71eb90e7 100644 --- a/regression/goto-diff/java-deleted-function/test.desc +++ b/regression/goto-diff/java-deleted-function/test.desc @@ -5,7 +5,7 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \}\n \], + "deletedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \}\n \], "modifiedFunctions": \[ \], "newFunctions": \[ \], -- diff --git a/regression/goto-diff/java-mod-identifier2/test.desc b/regression/goto-diff/java-mod-identifier2/test.desc index 30ca04ea85b..85e358df745 100644 --- a/regression/goto-diff/java-mod-identifier2/test.desc +++ b/regression/goto-diff/java-mod-identifier2/test.desc @@ -6,7 +6,7 @@ activate-multi-line-match EXIT=0 SIGNAL=0 "deletedFunctions": \[ \], - "modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \],\n + "modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \],\n "newFunctions": \[ \], -- ^warning: ignoring diff --git a/regression/goto-diff/java-mod-package/test.desc b/regression/goto-diff/java-mod-package/test.desc index f05162a49f1..d64ab3bde31 100644 --- a/regression/goto-diff/java-mod-package/test.desc +++ b/regression/goto-diff/java-mod-package/test.desc @@ -5,8 +5,8 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], + "deletedFunctions": \[\n \{\n "name": "java::foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.:\(\)V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.foo:\(I\)I",\n "line": "5"\n \}\n \},\n \{\n "name": "java::foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "foo/Test\.java",\n "function": "java::foo\.Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \], "modifiedFunctions": \[ \], - "newFunctions": \[\n \{\n "name": "java::com\.diffblue\.foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.:\(\)\V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n + "newFunctions": \[\n \{\n "name": "java::com\.diffblue\.foo\.Test\.:\(\)V",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.:\(\)\V",\n "line": "3"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::com\.diffblue\.foo\.Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "com/diffblue/foo/Test\.java",\n "function": "java::com\.diffblue\.foo\.Test.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n -- ^warning: ignoring diff --git a/regression/goto-diff/java-new-function/test.desc b/regression/goto-diff/java-new-function/test.desc index fd7e52f4fa2..6b11bbd326c 100644 --- a/regression/goto-diff/java-new-function/test.desc +++ b/regression/goto-diff/java-new-function/test.desc @@ -7,6 +7,6 @@ EXIT=0 SIGNAL=0 "deletedFunctions": \[ \], "modifiedFunctions": \[ \], - "newFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \], + "newFunctions": \[\n \{\n "name": "java::Test\.foo:\(II\)I",\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test\.foo:\(II\)I",\n "line": "4"\n \}\n \}\n \], -- ^warning: ignoring diff --git a/regression/goto-diff/java-properties/test.desc b/regression/goto-diff/java-properties/test.desc index 895f7360e7f..a2d74f5bfad 100644 --- a/regression/goto-diff/java-properties/test.desc +++ b/regression/goto-diff/java-properties/test.desc @@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n + "deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n -- ^warning: ignoring diff --git a/regression/goto-diff/java-scope-change/test.desc b/regression/goto-diff/java-scope-change/test.desc index 70e43809dd8..0583be7e77a 100644 --- a/regression/goto-diff/java-scope-change/test.desc +++ b/regression/goto-diff/java-scope-change/test.desc @@ -5,7 +5,7 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n "newFunctions": \[ \], + "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "4"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "12"\n \}\n \}\n \],\n "newFunctions": \[ \], -- ^warning: ignoring -- diff --git a/regression/goto-diff/java-scope-change2/test.desc b/regression/goto-diff/java-scope-change2/test.desc index 54c1fcd201e..4085770f555 100644 --- a/regression/goto-diff/java-scope-change2/test.desc +++ b/regression/goto-diff/java-scope-change2/test.desc @@ -5,7 +5,7 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \], + "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \], -- ^warning: ignoring -- diff --git a/regression/goto-diff/java-scope-change3/test.desc b/regression/goto-diff/java-scope-change3/test.desc index 54c1fcd201e..4085770f555 100644 --- a/regression/goto-diff/java-scope-change3/test.desc +++ b/regression/goto-diff/java-scope-change3/test.desc @@ -5,7 +5,7 @@ old.jar --json-ui activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \], + "deletedFunctions": \[ \],\n "modifiedFunctions": \[\n \{\n "name": "java::Test\.:\(\)V",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "1"\n \}\n \},\n \{\n "name": "java::Test\.foo:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.foo:\(I\)I",\n "line": "6"\n \}\n \},\n \{\n "name": "java::Test\.bar:\(I\)I",\n "sourceLocation": \{\n "file": "Test\.java",\n "function": "java::Test\.bar:\(I\)I",\n "line": "14"\n \}\n \}\n \],\n "newFunctions": \[ \], -- ^warning: ignoring -- diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 72d5b7cf1f2..421b8111edc 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -206,24 +206,26 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) case ui_message_handlert::uit::JSON_UI: { - json_objectt json_result; - json_arrayt &result_array=json_result["result"].make_array(); + json_stream_objectt &json_result = + result().json_stream().push_back_stream_object(); + json_stream_arrayt &result_array = + json_result.push_back_stream_array("result"); for(const auto &g : goal_map) { - json_objectt &result=result_array.push_back().make_object(); + json_stream_objectt &result = result_array.push_back_stream_object(); result["property"]=json_stringt(id2string(g.first)); result["description"]=json_stringt(id2string(g.second.description)); result["status"]=json_stringt(g.second.status_string()); if(g.second.status==goalt::statust::FAILURE) { - jsont &json_trace=result["trace"]; - convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options()); + json_stream_arrayt &json_trace = + result.push_back_stream_array("trace"); + convert( + bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options()); } } - - result() << json_result; } break; } diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ca942f38cbf..4b674c3afbb 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -86,18 +87,17 @@ void bmct::error_trace() case ui_message_handlert::uit::JSON_UI: { - json_objectt json; - json_arrayt &result_array=json["results"].make_array(); - json_objectt &json_result=result_array.push_back().make_object(); + json_stream_objectt &json_result = + status().json_stream().push_back_stream_object(); const goto_trace_stept &step=goto_trace.steps.back(); json_result["property"]= json_stringt(id2string(step.pc->source_location.get_property_id())); json_result["description"]= json_stringt(id2string(step.pc->source_location.get_comment())); json_result["status"]=json_stringt("failed"); - jsont &json_trace=json_result["trace"]; - convert(ns, goto_trace, json_trace, trace_options()); - status() << json_result; + json_stream_arrayt &json_trace = + json_result.push_back_stream_array("trace"); + convert(ns, goto_trace, json_trace, trace_options()); } break; } diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index e1a9f916ad0..72d64a184a5 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -346,19 +347,19 @@ bool bmc_covert::operator()() case ui_message_handlert::uit::JSON_UI: { - json_objectt json_result; - json_arrayt &goals_array=json_result["goals"].make_array(); + json_stream_objectt &json_result = + status().json_stream().push_back_stream_object(); for(const auto &goal_pair : goal_map) { const goalt &goal=goal_pair.second; - json_objectt &result=goals_array.push_back().make_object(); - result["status"]=json_stringt(goal.satisfied?"satisfied":"failed"); - result["goal"]=json_stringt(id2string(goal_pair.first)); - result["description"]=json_stringt(goal.description); + json_result["status"] = + json_stringt(goal.satisfied ? "satisfied" : "failed"); + json_result["goal"] = json_stringt(id2string(goal_pair.first)); + json_result["description"] = json_stringt(goal.description); if(goal.source_location.is_not_nil()) - result["sourceLocation"]=json(goal.source_location); + json_result["sourceLocation"] = json(goal.source_location); } json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size())); json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); @@ -369,12 +370,12 @@ bool bmc_covert::operator()() json_objectt &result=tests_array.push_back().make_object(); if(bmc.options.get_bool_option("trace")) { - jsont &json_trace=result["trace"]; + json_arrayt &json_trace = json_result["trace"].make_array(); convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options()); } else { - json_arrayt &json_test=result["inputs"].make_array(); + json_arrayt &json_test = json_result["inputs"].make_array(); for(const auto &step : test.goto_trace.steps) { @@ -396,7 +397,6 @@ bool bmc_covert::operator()() } } - result() << json_result; break; } } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index fa4964d4d52..e72b7454ff5 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "interpreter_class.h" +#include "json_goto_trace.h" #include "remove_returns.h" const std::size_t interpretert::npos=std::numeric_limits::max(); @@ -151,8 +152,8 @@ void interpretert::command() } else if(ch=='j') { - jsont json_steps; - convert(ns, steps, json_steps); + json_arrayt json_steps; + convert(ns, steps, json_steps); ch=tolower(command[1]); if(ch==' ') { diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 3de31f8d06d..1095a3ad281 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -12,278 +12,294 @@ Author: Daniel Kroening /// Traces of GOTO Programs #include "json_goto_trace.h" +#include "goto_trace.h" #include +#include +#include #include #include #include #include - -#include #include +#include -/// Produce a json representation of a trace. -/// \param ns: a namespace -/// \param goto_trace: a trace in a goto program -/// \param dest: referecence to a json object in which the goto trace will be -/// added -void convert( - const namespacet &ns, - const goto_tracet &goto_trace, - jsont &dest, - trace_optionst trace_options) +/// Convert an ASSERT goto_trace step. +/// \param [out] json_failure: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_assert( + json_objectt &json_failure, + const conversion_dependenciest &conversion_dependencies) { - json_arrayt &dest_array=dest.make_array(); - - source_locationt previous_source_location; + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &location = conversion_dependencies.location; + const source_locationt &source_location = + conversion_dependencies.source_location; + + irep_idt property_id = + step.pc->is_assert() + ? source_location.get_property_id() + : step.pc->is_goto() + ? id2string(step.pc->source_location.get_function()) + ".unwind." + + std::to_string(step.pc->loop_number) + : ""; + + json_failure["stepType"] = json_stringt("failure"); + json_failure["hidden"] = jsont::json_boolean(step.hidden); + json_failure["internal"] = jsont::json_boolean(step.internal); + json_failure["thread"] = json_numbert(std::to_string(step.thread_nr)); + json_failure["reason"] = json_stringt(id2string(step.comment)); + json_failure["property"] = json_stringt(id2string(property_id)); + + if(!location.is_null()) + json_failure["sourceLocation"] = location; +} - for(const auto &step : goto_trace.steps) - { - const source_locationt &source_location=step.pc->source_location; +/// Convert a DECL goto_trace step. +/// \param [out] json_assignment: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +/// \param trace_options: Extra information used by this +/// particular conversion function. +void convert_decl( + json_objectt &json_assignment, + const conversion_dependenciest &conversion_dependencies, + const trace_optionst &trace_options) +{ + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &json_location = conversion_dependencies.location; + const namespacet &ns = conversion_dependencies.ns; - jsont json_location; + irep_idt identifier = step.lhs_object.get_identifier(); - if(source_location.is_not_nil() && source_location.get_file()!="") - json_location=json(source_location); - else - json_location=json_nullt(); + json_assignment["stepType"] = json_stringt("assignment"); - switch(step.type) - { - case goto_trace_stept::typet::ASSERT: - if(!step.cond_value) - { - irep_idt property_id; + if(!json_location.is_null()) + json_assignment["sourceLocation"] = json_location; - if(step.pc->is_assert()) - property_id=source_location.get_property_id(); - else if(step.pc->is_goto()) // unwinding, we suspect - { - property_id= - id2string(step.pc->source_location.get_function())+ - ".unwind."+std::to_string(step.pc->loop_number); - } + std::string value_string, binary_string, type_string, full_lhs_string; + json_objectt full_lhs_value; - json_objectt &json_failure=dest_array.push_back().make_object(); + DATA_INVARIANT( + step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil"); + exprt simplified = simplify_expr(step.full_lhs, ns); - json_failure["stepType"]=json_stringt("failure"); - json_failure["hidden"]=jsont::json_boolean(step.hidden); - json_failure["internal"]=jsont::json_boolean(step.internal); - json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_failure["reason"]=json_stringt(id2string(step.comment)); - json_failure["property"]=json_stringt(id2string(property_id)); + if(trace_options.json_full_lhs) + { + class comment_base_name_visitort : public expr_visitort + { + private: + const namespacet &ns; - if(!json_location.is_null()) - json_failure["sourceLocation"]=json_location; + public: + explicit comment_base_name_visitort(const namespacet &ns) : ns(ns) + { } - break; - case goto_trace_stept::typet::ASSIGNMENT: - case goto_trace_stept::typet::DECL: + void operator()(exprt &expr) override { - irep_idt identifier=step.lhs_object.get_identifier(); - json_objectt &json_assignment=dest_array.push_back().make_object(); - - json_assignment["stepType"]=json_stringt("assignment"); - - if(!json_location.is_null()) - json_assignment["sourceLocation"]=json_location; - - std::string value_string, binary_string, type_string, full_lhs_string; - json_objectt full_lhs_value; - - DATA_INVARIANT( - step.full_lhs.is_not_nil(), - "full_lhs in assignment must not be nil"); - exprt simplified=simplify_expr(step.full_lhs, ns); - - if(trace_options.json_full_lhs) + if(expr.id() == ID_symbol) { - class comment_base_name_visitort : public expr_visitort - { - private: - const namespacet &ns; - - public: - explicit comment_base_name_visitort(const namespacet &ns) : ns(ns) - { - } - - void operator()(exprt &expr) override - { - if(expr.id() == ID_symbol) - { - const symbolt &symbol = ns.lookup(expr.get(ID_identifier)); - if(expr.find(ID_C_base_name).is_not_nil()) - INVARIANT( - expr.find(ID_C_base_name).id() == symbol.base_name, - "base_name comment does not match symbol's base_name"); - else - expr.add(ID_C_base_name, irept(symbol.base_name)); - } - } - }; - comment_base_name_visitort comment_base_name_visitor(ns); - simplified.visit(comment_base_name_visitor); + const symbolt &symbol = ns.lookup(expr.get(ID_identifier)); + if(expr.find(ID_C_base_name).is_not_nil()) + INVARIANT( + expr.find(ID_C_base_name).id() == symbol.base_name, + "base_name comment does not match symbol's base_name"); + else + expr.add(ID_C_base_name, irept(symbol.base_name)); } + } + }; + comment_base_name_visitort comment_base_name_visitor(ns); + simplified.visit(comment_base_name_visitor); + } - full_lhs_string=from_expr(ns, identifier, simplified); + full_lhs_string = from_expr(ns, identifier, simplified); - const symbolt *symbol; - irep_idt base_name, display_name; + const symbolt *symbol; + irep_idt base_name, display_name; - if(!ns.lookup(identifier, symbol)) - { - base_name=symbol->base_name; - display_name=symbol->display_name(); - if(type_string=="") - type_string=from_type(ns, identifier, symbol->type); + if(!ns.lookup(identifier, symbol)) + { + base_name = symbol->base_name; + display_name = symbol->display_name(); + if(type_string == "") + type_string = from_type(ns, identifier, symbol->type); - json_assignment["mode"]=json_stringt(id2string(symbol->mode)); - exprt simplified=simplify_expr(step.full_lhs_value, ns); + json_assignment["mode"] = json_stringt(id2string(symbol->mode)); + exprt simplified = simplify_expr(step.full_lhs_value, ns); - full_lhs_value=json(simplified, ns, symbol->mode); - } - else - { - DATA_INVARIANT( - step.full_lhs_value.is_not_nil(), - "full_lhs_value in assignment must not be nil"); - full_lhs_value=json(step.full_lhs_value, ns, ID_unknown); - } + full_lhs_value = json(simplified, ns, symbol->mode); + } + else + { + DATA_INVARIANT( + step.full_lhs_value.is_not_nil(), + "full_lhs_value in assignment must not be nil"); + full_lhs_value = json(step.full_lhs_value, ns, ID_unknown); + } - json_assignment["value"]=full_lhs_value; - json_assignment["lhs"]=json_stringt(full_lhs_string); - if(trace_options.json_full_lhs) - { - // Not language specific, still mangled, fully-qualified name of lhs - json_assignment["rawLhs"] = - json_irept(true).convert_from_irep(simplified); - } - json_assignment["hidden"]=jsont::json_boolean(step.hidden); - json_assignment["internal"]=jsont::json_boolean(step.internal); - json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); - - json_assignment["assignmentType"]= - json_stringt( - step.assignment_type== - goto_trace_stept::assignment_typet::ACTUAL_PARAMETER? - "actual-parameter": - "variable"); - } - break; + json_assignment["value"] = full_lhs_value; + json_assignment["lhs"] = json_stringt(full_lhs_string); + if(trace_options.json_full_lhs) + { + // Not language specific, still mangled, fully-qualified name of lhs + json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified); + } + json_assignment["hidden"] = jsont::json_boolean(step.hidden); + json_assignment["internal"] = jsont::json_boolean(step.internal); + json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr)); + + json_assignment["assignmentType"] = json_stringt( + step.assignment_type == goto_trace_stept::assignment_typet::ACTUAL_PARAMETER + ? "actual-parameter" + : "variable"); +} - case goto_trace_stept::typet::OUTPUT: - { - json_objectt &json_output=dest_array.push_back().make_object(); - - json_output["stepType"]=json_stringt("output"); - json_output["hidden"]=jsont::json_boolean(step.hidden); - json_output["internal"]=jsont::json_boolean(step.internal); - json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_output["outputID"]=json_stringt(id2string(step.io_id)); - - // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode=ID_unknown; - else - mode=function_name->mode; - json_output["mode"]=json_stringt(id2string(mode)); - json_arrayt &json_values=json_output["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns, mode)); - } +/// Convert an OUTPUT goto_trace step. +/// \param [out] json_output: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_output( + json_objectt &json_output, + const conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &location = conversion_dependencies.location; + const namespacet &ns = conversion_dependencies.ns; + const source_locationt &source_location = step.pc->source_location; + + json_output["stepType"] = json_stringt("output"); + json_output["hidden"] = jsont::json_boolean(step.hidden); + json_output["internal"] = jsont::json_boolean(step.internal); + json_output["thread"] = json_numbert(std::to_string(step.thread_nr)); + json_output["outputID"] = json_stringt(id2string(step.io_id)); + + // Recovering the mode from the function + irep_idt mode; + const symbolt *function_name; + if(ns.lookup(source_location.get_function(), function_name)) + // Failed to find symbol + mode = ID_unknown; + else + mode = function_name->mode; + json_output["mode"] = json_stringt(id2string(mode)); + json_arrayt &json_values = json_output["values"].make_array(); + + for(const auto &arg : step.io_args) + { + arg.is_nil() ? json_values.push_back(json_stringt("")) + : json_values.push_back(json(arg, ns, mode)); + } - if(!json_location.is_null()) - json_output["sourceLocation"]=json_location; - } - break; + if(!location.is_null()) + json_output["sourceLocation"] = location; +} - case goto_trace_stept::typet::INPUT: - { - json_objectt &json_input=dest_array.push_back().make_object(); - - json_input["stepType"]=json_stringt("input"); - json_input["hidden"]=jsont::json_boolean(step.hidden); - json_input["internal"]=jsont::json_boolean(step.internal); - json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); - json_input["inputID"]=json_stringt(id2string(step.io_id)); - - // Recovering the mode from the function - irep_idt mode; - const symbolt *function_name; - if(ns.lookup(source_location.get_function(), function_name)) - // Failed to find symbol - mode=ID_unknown; - else - mode=function_name->mode; - json_input["mode"]=json_stringt(id2string(mode)); - json_arrayt &json_values=json_input["values"].make_array(); - - for(const auto &arg : step.io_args) - { - if(arg.is_nil()) - json_values.push_back(json_stringt("")); - else - json_values.push_back(json(arg, ns, mode)); - } +/// Convert an INPUT goto_trace step. +/// \param [out] json_input: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_input( + json_objectt &json_input, + const conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &location = conversion_dependencies.location; + const namespacet &ns = conversion_dependencies.ns; + const source_locationt &source_location = step.pc->source_location; + + json_input["stepType"] = json_stringt("input"); + json_input["hidden"] = jsont::json_boolean(step.hidden); + json_input["internal"] = jsont::json_boolean(step.internal); + json_input["thread"] = json_numbert(std::to_string(step.thread_nr)); + json_input["inputID"] = json_stringt(id2string(step.io_id)); + + // Recovering the mode from the function + irep_idt mode; + const symbolt *function_name; + if(ns.lookup(source_location.get_function(), function_name)) + // Failed to find symbol + mode = ID_unknown; + else + mode = function_name->mode; + json_input["mode"] = json_stringt(id2string(mode)); + json_arrayt &json_values = json_input["values"].make_array(); + + for(const auto &arg : step.io_args) + { + arg.is_nil() ? json_values.push_back(json_stringt("")) + : json_values.push_back(json(arg, ns, mode)); + } - if(!json_location.is_null()) - json_input["sourceLocation"]=json_location; - } - break; + if(!location.is_null()) + json_input["sourceLocation"] = location; +} - case goto_trace_stept::typet::FUNCTION_CALL: - case goto_trace_stept::typet::FUNCTION_RETURN: - { - std::string tag= - (step.type==goto_trace_stept::typet::FUNCTION_CALL)? - "function-call":"function-return"; - json_objectt &json_call_return=dest_array.push_back().make_object(); - - json_call_return["stepType"]=json_stringt(tag); - json_call_return["hidden"]=jsont::json_boolean(step.hidden); - json_call_return["internal"]=jsont::json_boolean(step.internal); - json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); - - const symbolt &symbol=ns.lookup(step.identifier); - json_objectt &json_function=json_call_return["function"].make_object(); - json_function["displayName"]= - json_stringt(id2string(symbol.display_name())); - json_function["identifier"]=json_stringt(id2string(step.identifier)); - json_function["sourceLocation"]=json(symbol.location); - - if(!json_location.is_null()) - json_call_return["sourceLocation"]=json_location; - } - break; +/// Convert a FUNCTION_RETURN goto_trace step. +/// \param [out] json_call_return: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_return( + json_objectt &json_call_return, + const conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &location = conversion_dependencies.location; + const namespacet &ns = conversion_dependencies.ns; + + std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL) + ? "function-call" + : "function-return"; + + json_call_return["stepType"] = json_stringt(tag); + json_call_return["hidden"] = jsont::json_boolean(step.hidden); + json_call_return["internal"] = jsont::json_boolean(step.internal); + json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr)); + + const symbolt &symbol = ns.lookup(step.identifier); + json_objectt &json_function = json_call_return["function"].make_object(); + json_function["displayName"] = json_stringt(id2string(symbol.display_name())); + json_function["identifier"] = json_stringt(id2string(step.identifier)); + json_function["sourceLocation"] = json(symbol.location); + + if(!location.is_null()) + json_call_return["sourceLocation"] = location; +} - default: - if(source_location!=previous_source_location) - { - // just the source location - if(!json_location.is_null()) - { - json_objectt &json_location_only=dest_array.push_back().make_object(); - json_location_only["stepType"]=json_stringt("location-only"); - json_location_only["hidden"]=jsont::json_boolean(step.hidden); - json_location_only["internal"]=jsont::json_boolean(step.internal); - json_location_only["thread"]= - json_numbert(std::to_string(step.thread_nr)); - json_location_only["sourceLocation"]=json_location; - } - } - } +/// Convert all other types of steps not already handled +/// by the other conversion functions. +/// \param [out] json_location_only: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_default( + json_objectt &json_location_only, + const conversion_dependenciest &conversion_dependencies) +{ + const goto_trace_stept &step = conversion_dependencies.step; + const jsont &location = conversion_dependencies.location; - if(source_location.is_not_nil() && source_location.get_file()!="") - previous_source_location=source_location; - } + json_location_only["stepType"] = json_stringt("location-only"); + json_location_only["hidden"] = jsont::json_boolean(step.hidden); + json_location_only["thread"] = json_numbert(std::to_string(step.thread_nr)); + json_location_only["sourceLocation"] = location; } diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 2777ec44673..820de78ee78 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -14,14 +14,178 @@ Date: November 2005 #ifndef CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H #define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H +#include "goto_trace.h" + #include +#include +#include +#include -#include "goto_trace.h" +/// This is structure is here to facilitate +/// passing arguments to the conversion +/// functions. +typedef struct +{ + const jsont &location; + const goto_trace_stept &step; + const namespacet &ns; + const source_locationt &source_location; +} conversion_dependenciest; + +/// Convert an ASSERT goto_trace step. +/// \param [out] json_failure: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_assert( + json_objectt &json_failure, + const conversion_dependenciest &conversion_dependencies); + +/// Convert a DECL goto_trace step. +/// \param [out] json_assignment: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +/// \param trace_options: Extra information used by this +/// particular conversion function. +void convert_decl( + json_objectt &json_assignment, + const conversion_dependenciest &conversion_dependencies, + const trace_optionst &trace_options); +/// Convert an OUTPUT goto_trace step. +/// \param [out] json_output: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_output( + json_objectt &json_output, + const conversion_dependenciest &conversion_dependencies); + +/// Convert an INPUT goto_trace step. +/// \param [out] json_input: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_input( + json_objectt &json_input, + const conversion_dependenciest &conversion_dependencies); + +/// Convert a FUNCTION_RETURN goto_trace step. +/// \param [out] json_call_return: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_return( + json_objectt &json_call_return, + const conversion_dependenciest &conversion_dependencies); + +/// Convert all other types of steps not already handled +/// by the other conversion functions. +/// \param [out] json_location_only: The JSON object that +/// will contain the information about the step +/// after this function has run. +/// \param conversion_dependencies: A structure +/// that contains information the conversion function +/// needs. +void convert_default( + json_objectt &json_location_only, + const conversion_dependenciest &conversion_dependencies); + +/// Templated version of the conversion method. +/// Works by dispatching to the more specialised +/// conversion functions based on the type of the +/// step that is being handled. +/// \param ns: The namespace used for resolution of symbols. +/// \param goto_trace: The goto_trace from which we are +/// going to convert the steps from. +/// \param dest_array: The JSON object that we are going +/// to append the step information to. +/// \param trace_options: A list of trace options +template void convert( - const namespacet &, - const goto_tracet &, - jsont &, - trace_optionst trace_options = trace_optionst::default_options); + const namespacet &ns, + const goto_tracet &goto_trace, + json_arrayT &dest_array, + trace_optionst trace_options = trace_optionst::default_options) +{ + source_locationt previous_source_location; + + for(const auto &step : goto_trace.steps) + { + const source_locationt &source_location = step.pc->source_location; + + jsont json_location; + + source_location.is_not_nil() && !source_location.get_file().empty() + ? json_location = json(source_location) + : json_location = json_nullt(); + + // NOLINTNEXTLINE(whitespace/braces) + conversion_dependenciest conversion_dependencies = { + json_location, step, ns, source_location}; + + switch(step.type) + { + case goto_trace_stept::typet::ASSERT: + if(!step.cond_value) + { + json_objectt &json_failure = dest_array.push_back().make_object(); + convert_assert(json_failure, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::ASSIGNMENT: + case goto_trace_stept::typet::DECL: + { + json_objectt &json_assignment = dest_array.push_back().make_object(); + convert_decl(json_assignment, conversion_dependencies, trace_options); + } + break; + + case goto_trace_stept::typet::OUTPUT: + { + json_objectt &json_output = dest_array.push_back().make_object(); + convert_output(json_output, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::INPUT: + { + json_objectt &json_input = dest_array.push_back().make_object(); + convert_input(json_input, conversion_dependencies); + } + break; + + case goto_trace_stept::typet::FUNCTION_CALL: + case goto_trace_stept::typet::FUNCTION_RETURN: + { + json_objectt &json_call_return = dest_array.push_back().make_object(); + convert_return(json_call_return, conversion_dependencies); + } + break; + + default: + if(source_location != previous_source_location) + { + json_objectt &json_location_only = dest_array.push_back().make_object(); + convert_default(json_location_only, conversion_dependencies); + } + } + + if(source_location.is_not_nil() && !source_location.get_file().empty()) + previous_source_location = source_location; + } +} #endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H diff --git a/src/util/Makefile b/src/util/Makefile index f4a06e1198a..cb9d221dd60 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -37,6 +37,7 @@ SRC = arith_tools.cpp \ json.cpp \ json_expr.cpp \ json_irep.cpp \ + json_stream.cpp \ lispexpr.cpp \ lispirep.cpp \ memory_info.cpp \ diff --git a/src/util/json.cpp b/src/util/json.cpp index 79352da4f7e..5fa037273fa 100644 --- a/src/util/json.cpp +++ b/src/util/json.cpp @@ -50,6 +50,9 @@ void jsont::escape_string(const std::string &src, std::ostream &out) } } +/// Recursive printing of the json object. +/// \param out: The stream object to have the json printed to. +/// \param indent: The indentation level. void jsont::output_rec(std::ostream &out, unsigned indent) const { switch(kind) @@ -66,23 +69,7 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const case kindt::J_OBJECT: out << '{'; - for(objectt::const_iterator o_it=object.begin(); - o_it!=object.end(); - o_it++) - { - if(o_it!=object.begin()) - out << ','; - - out << '\n'; - - out << std::string((indent+1)*2, ' '); - - out << '"'; - escape_string(o_it->first, out); - out << '"'; - out << ": "; - o_it->second.output_rec(out, indent+1); - } + output_object(out, object, indent); if(!object.empty()) { out << '\n'; @@ -133,6 +120,41 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const } } +/// Basic handling of the printing of a JSON object. +/// Dispatches to output_rec for most of the hard work. +/// \param out: The stream that the JSON object is to be +/// printed to. +/// \param object: The JSON object. +/// \param indent: The indentation level. +void jsont::output_object( + std::ostream &out, + const objectt &object, + unsigned indent) +{ + for(objectt::const_iterator o_it = object.begin(); o_it != object.end(); + o_it++) + { + if(o_it != object.begin()) + out << ','; + + // A JSON object always starts with an opening brace, + // after which we put a newline. + out << '\n'; + + out << std::string((indent + 1) * 2, ' '); + + jsont::output_key(out, o_it->first); + o_it->second.output_rec(out, indent + 1); + } +} + +void jsont::output_key(std::ostream &out, const std::string &key) +{ + out << '"'; + jsont::escape_string(key, out); + out << "\": "; +} + void jsont::swap(jsont &other) { std::swap(other.kind, kind); diff --git a/src/util/json.h b/src/util/json.h index 5095a3044df..018b92606f6 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -106,12 +106,13 @@ class jsont return it->second; } -protected: void output_rec(std::ostream &, unsigned indent) const; - static void escape_string(const std::string &, std::ostream &); static const jsont null_json_object; +protected: + static void escape_string(const std::string &, std::ostream &); + explicit jsont(kindt _kind):kind(_kind) { } @@ -127,6 +128,9 @@ class jsont typedef std::map objectt; objectt object; + static void + output_object(std::ostream &out, const objectt &object, unsigned indent); + static void output_key(std::ostream &out, const std::string &key); std::string value; }; diff --git a/src/util/json_stream.cpp b/src/util/json_stream.cpp new file mode 100644 index 00000000000..7bb28a3897d --- /dev/null +++ b/src/util/json_stream.cpp @@ -0,0 +1,155 @@ +/*******************************************************************\ + +Module: + +Author: Peter Schrammel + +\*******************************************************************/ + +#include "json_stream.h" + +#include + +/// Output the element delimiter to the output stream +void json_streamt::output_delimiter() +{ + if(!first) + out << ','; + else + first = false; + out << '\n'; + out << std::string((indent + 1) * 2, ' '); +} + +/// Construct a new JSON array stream +/// \param out: output stream +/// \param indent: indentation level +json_stream_arrayt::json_stream_arrayt(std::ostream &out, unsigned indent) + : json_streamt(out, indent) +{ + out << '['; +} + +/// Output the non-streaming JSON objects and closes the current child stream +void json_stream_arrayt::output_child_stream() +{ + if(!object.empty()) + { + output_delimiter(); + object["array_element"].output_rec(out, indent + 1); + object.clear(); + } + if(child_stream) + { + child_stream->close(); + child_stream = nullptr; + } +} + +/// Output the finalizing character for a JSON array +void json_stream_arrayt::output_finalizer() +{ + out << '\n' << std::string(indent * 2, ' '); + out << ']'; +} + +/// Constructor for json_stream_objectt. +/// \param out: The stream that is to be used to output the JSON object. +/// \param indent: Current indentation level. +json_stream_objectt::json_stream_objectt(std::ostream &out, unsigned indent) + : json_streamt(out, indent) +{ + out << '{'; +} + +/// Create a new JSON array child stream. +json_stream_arrayt &json_streamt::create_child_stream_array() +{ + child_stream = + std::unique_ptr(new json_stream_arrayt(out, indent + 1)); + return static_cast(*child_stream); +} + +/// Create a new JSON object child stream. +json_stream_objectt &json_streamt::create_child_stream_object() +{ + child_stream = + std::unique_ptr(new json_stream_objectt(out, indent + 1)); + return static_cast(*child_stream); +} + +/// Add a JSON object child stream +json_stream_objectt &json_stream_arrayt::push_back_stream_object() +{ + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before creating the new one. + output_child_stream(); + output_delimiter(); + return create_child_stream_object(); +} + +/// Add a JSON array child stream +json_stream_arrayt &json_stream_arrayt::push_back_stream_array() +{ + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before creating the new one. + output_child_stream(); + output_delimiter(); + return create_child_stream_array(); +} + +/// Add a JSON object stream for a specific key +/// \param key: key of the JSON property +json_stream_objectt & +json_stream_objectt::push_back_stream_object(const std::string &key) +{ + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before creating the new one. + output_child_stream(); + output_delimiter(); + jsont::output_key(out, key); + return create_child_stream_object(); +} + +/// Add a JSON array stream for a specific key +/// \param key: key of the JSON property +json_stream_arrayt & +json_stream_objectt::push_back_stream_array(const std::string &key) +{ + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before creating the new one. + output_child_stream(); + output_delimiter(); + jsont::output_key(out, key); + return create_child_stream_array(); +} + +/// Output non-streaming JSON properties and flushes and closes +/// the child stream +void json_stream_objectt::output_child_stream() +{ + for(const auto &obj : object) + { + output_delimiter(); + jsont::output_key(out, obj.first); + obj.second.output_rec(out, indent + 1); + } + object.clear(); + if(child_stream) + { + child_stream->close(); + child_stream = nullptr; + } +} + +/// Output the finalizing character for a JSON object +void json_stream_objectt::output_finalizer() +{ + jsont::output_object(out, object, indent); + out << '\n' << std::string(indent * 2, ' '); + out << '}'; +} diff --git a/src/util/json_stream.h b/src/util/json_stream.h new file mode 100644 index 00000000000..4f1541d0496 --- /dev/null +++ b/src/util/json_stream.h @@ -0,0 +1,180 @@ +/*******************************************************************\ + +Module: + +Author: Peter Schrammel + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_JSON_STREAM_H +#define CPROVER_UTIL_JSON_STREAM_H + +#include +#include + +#include "json.h" +#include "invariant.h" + +class json_stream_objectt; +class json_stream_arrayt; + +/// This class provides a facility for streaming JSON objects directly to the +/// output instead of waiting for the object to be fully formed in memory and +/// then print it (as done using `jsont`). This reduces memory consumption +/// when preparing e.g. large traces for output. +/// +/// `json_streamt` is the base class from which the classes for streaming +/// arrays (`json_stream_arrayt`) and objects (`json_stream_objectt`) are +/// derived. `json_streamt` wraps an output stream and stores the current +/// element to be output. This can be either a child stream (of type +/// `json_streamt` that outputs JSON objects incrementally) or a +/// non-streaming JSON `object` (of type `jsont` that will be output as a +/// whole) To ensure consistency of the output, a class invariant is that +/// there is at most one child stream at any time. For this reason, the +/// existing child stream is flushed and closed when creating a new child +/// stream. +class json_streamt +{ +public: + /// Outputs the current current child stream and closes this JSON stream + void close() + { + if(open) + { + output_child_stream(); + output_finalizer(); + open = false; + } + } + + virtual ~json_streamt() = default; + +protected: + /// Constructor to be used by derived classes + /// \param _out: output stream + /// \param _indent: indentation level + json_streamt(std::ostream &_out, unsigned _indent) + : open(true), out(_out), indent(_indent), first(true), child_stream(nullptr) + { + } + + /// Denotes whether the current stream is open or has been invalidated. + bool open; + std::ostream &out; + unsigned indent; + + /// Is the current element the first element in the object or array? + /// This is required to know whether a delimiter must be output or not. + bool first; + + /// Non-streaming JSON elements + /// These will be printed when closing the stream or creating a child stream. + typedef std::map objectt; + objectt object; + + /// The current child stream. One can create and close many child streams + /// sequentially (timewise), e.g. for each element in an array or each + /// property in an object. The invariant is that there can only be at + /// most child *one* stream at a time. + std::unique_ptr child_stream; + json_stream_arrayt &create_child_stream_array(); + json_stream_objectt &create_child_stream_object(); + + /// Outputs the delimiter between JSON elements + void output_delimiter(); + + // To be overridden by derived classes: + virtual void output_child_stream() = 0; + virtual void output_finalizer() = 0; +}; + +/// Provides methods for streaming JSON arrays +class json_stream_arrayt : public json_streamt +{ +public: + explicit json_stream_arrayt(std::ostream &out, unsigned indent = 0); + + /// Flushes and closes the stream on destruction + ~json_stream_arrayt() override + { + close(); + } + + /// Push back a JSON element into the current array stream. + /// Provided for compatibility with `jsont`. + /// \param json: a non-streaming JSON element + void push_back(const jsont &json) + { + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before printing the given element. + output_child_stream(); + output_delimiter(); + json.output_rec(out, indent + 1); + } + + /// Push back and return a new non-streaming JSON element into the current + /// array stream. + /// Provided for compatibility with `jsont`. + /// \return a new empty, non-streaming JSON object + jsont &push_back() + { + PRECONDITION(open); + // To ensure consistency of the output, we flush and + // close the current child stream before adding the given element. + output_child_stream(); + // We store the new element in the object map. + return object["array_element"]; + } + + json_stream_objectt &push_back_stream_object(); + json_stream_arrayt &push_back_stream_array(); + +protected: + void output_child_stream() override; + void output_finalizer() override; +}; + +/// Provides methods for streaming JSON objects +class json_stream_objectt : public json_streamt +{ +public: + explicit json_stream_objectt(std::ostream &out, unsigned indent = 0); + + /// Provide key-value lookup capabilities for the + /// JSON object. Provided for compatibility with `jsont`. + /// \param key: The key to be looked up inside the + /// attributes of the JSON object. + jsont &operator[](const std::string &key) + { + return object[key]; + } + + ~json_stream_objectt() override + { + close(); + } + + /// Lookup the key of a non-streaming JSON element. + /// \param key: The key to be looked up inside the + /// attributes of the JSON object. + /// \return: The value that corresponds to the key + /// if found, a null_json_object otherwise. + const jsont &operator[](const std::string &key) const + { + objectt::const_iterator it = object.find(key); + if(it == object.end()) + return jsont::null_json_object; + else + return it->second; + } + + json_stream_objectt &push_back_stream_object(const std::string &key); + json_stream_arrayt &push_back_stream_array(const std::string &key); + +protected: + void output_child_stream() override; + void output_finalizer() override; +}; + +#endif // CPROVER_UTIL_JSON_STREAM_H diff --git a/src/util/message.h b/src/util/message.h index cf0f92013aa..528233145be 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" #include "xml.h" +class json_stream_arrayt; + class message_handlert { public: @@ -33,6 +35,12 @@ class message_handlert // no-op by default } + /// Return the underlying JSON stream + virtual json_stream_arrayt &get_json_stream() + { + UNREACHABLE; + } + virtual void print(unsigned level, const jsont &json) { // no-op by default @@ -232,6 +240,13 @@ class messaget return func(*this); } + /// Returns a reference to the top-level JSON array stream + json_stream_arrayt &json_stream() + { + *this << eom; // force end of previous message + return message.message_handler->get_json_stream(); + } + private: void assign_from(const mstreamt &other) { diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index d725e701315..61771eb6c70 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -15,39 +15,57 @@ Author: Daniel Kroening, kroening@kroening.com #include "json.h" #include "xml_expr.h" #include "json_expr.h" +#include "json_stream.h" #include "cout_message.h" #include "cmdline.h" +ui_message_handlert::ui_message_handlert() + : _ui(uit::PLAIN), + time(timestampert::make(timestampert::clockt::NONE)), + out(std::cout), + json_stream(nullptr) +{ +} + ui_message_handlert::ui_message_handlert( uit __ui, const std::string &program, timestampert::clockt clock_type) - : _ui(__ui), time(timestampert::make(clock_type)) + : _ui(__ui), + time(timestampert::make(clock_type)), + out(std::cout), + json_stream(nullptr) { - switch(__ui) + switch(_ui) { case uit::PLAIN: break; case uit::XML_UI: - std::cout << "" << "\n"; - std::cout << "" << "\n"; + out << "" + << "\n"; + out << "" + << "\n"; { xmlt program_xml; program_xml.name="program"; program_xml.data=program; - std::cout << program_xml; + out << program_xml; } break; case uit::JSON_UI: { - std::cout << "[\n"; - json_objectt json_program; - json_program["program"] = json_stringt(program); - std::cout << json_program; + if(!json_stream) + { + json_stream = + std::unique_ptr(new json_stream_arrayt(out)); + } + + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream->push_back().make_object()["program"] = json_stringt(program); } break; } @@ -76,11 +94,15 @@ ui_message_handlert::~ui_message_handlert() switch(get_ui()) { case uit::XML_UI: - std::cout << "" << "\n"; + + out << "" + << "\n"; break; case uit::JSON_UI: - std::cout << "\n]\n"; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream->close(); + out << '\n'; break; case uit::PLAIN: @@ -140,7 +162,7 @@ void ui_message_handlert::print( INVARIANT(false, "Cannot print xml data on PLAIN UI"); break; case uit::XML_UI: - std::cout << data << '\n'; + out << data << '\n'; flush(level); break; case uit::JSON_UI: @@ -165,7 +187,8 @@ void ui_message_handlert::print( INVARIANT(false, "Cannot print json data on XML UI"); break; case uit::JSON_UI: - std::cout << ',' << '\n' << data; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_stream->push_back(data); flush(level); break; } @@ -249,8 +272,8 @@ void ui_message_handlert::xml_ui_msg( if(!timestamp.empty()) result.set_attribute("timestamp", timestamp); - std::cout << result; - std::cout << '\n'; + out << result; + out << '\n'; } void ui_message_handlert::json_ui_msg( @@ -259,7 +282,8 @@ void ui_message_handlert::json_ui_msg( const std::string &msg2, const source_locationt &location) { - json_objectt result; + INVARIANT(json_stream, "JSON stream must be initialized before use"); + json_objectt &result = json_stream->push_back().make_object(); if(location.is_not_nil() && !location.get_file().empty()) @@ -291,7 +315,7 @@ void ui_message_handlert::flush(unsigned level) case uit::XML_UI: case uit::JSON_UI: { - std::cout << std::flush; + out << std::flush; } break; } diff --git a/src/util/ui_message.h b/src/util/ui_message.h index e3886961385..62756df777e 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -10,7 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_UI_MESSAGE_H #define CPROVER_UTIL_UI_MESSAGE_H +#include + #include "message.h" +#include "json_stream.h" #include "timestamper.h" class ui_message_handlert : public message_handlert @@ -25,10 +28,8 @@ class ui_message_handlert : public message_handlert ui_message_handlert(const class cmdlinet &, const std::string &program); - ui_message_handlert() - : _ui(uit::PLAIN), time(timestampert::make(timestampert::clockt::NONE)) - { - } + /// Default constructor; implementation is in .cpp file + ui_message_handlert(); virtual ~ui_message_handlert(); @@ -40,13 +41,25 @@ class ui_message_handlert : public message_handlert void set_ui(uit __ui) { _ui=__ui; + if(_ui == uit::JSON_UI && !json_stream) + { + json_stream = + std::unique_ptr(new json_stream_arrayt(out)); + } } virtual void flush(unsigned level) override; + json_stream_arrayt &get_json_stream() override + { + return *json_stream; + } + protected: uit _ui; std::unique_ptr time; + std::ostream &out; + std::unique_ptr json_stream; virtual void print( unsigned level,