Scribble
Search…
JSON output specification
When Scribble is executed with
--output-mode json (or -m json), it instruments the target file and compiles the instrumented source. It then returns slightly modified JSON output of used Solc compiler version.The differences are as follows:
- The
sourceskey contains entries with information about the compiled instrumentation files.When you are in--output-mode jsonmode this always contains a single entryflattened.sol, since all original files are flattened injsonmode. Scribble also adds additionalsourceproperty with the Solidity source code of the instrumentation file to each entry insources. - The
instrumentationMetadatakey contains helpful metadata and instrumented-to-original source mapping information.You can find an example of the instrumentation metadata format in the next section.
Instrumentation metadata
Scribble provides metadata that allows you to explore in more detail how exactly the original source code was instrumented. This gives an insight on the correspondence of the annotations to the added code fragments in instrumented source.
Data structure format of the metadata is following:
1
{
2
// Instrumented-to-original source mapping.
3
// Each entry is an array where
4
// first element is the source range of instrumented source,
5
// and second element is the corresponding source range of original source.
6
"instrToOriginalMap": [
7
[
8
"61:532:0", // Source range in instrumented source
9
"37:139:0" // Source range in original source
10
],
11
​
12
// ... may contain multiple entries ...
13
],
14
​
15
// Source ranges of instrumented source, that are corresponting to
16
// a code fragmets that are added by the tool for internal purposed.
17
// These source ranges are not related to a predicates.
18
"otherInstrumentation": [
19
"681:38:0", // Source range in instrumented source
20
​
21
// ... may contain multiple entries ...
22
],
23
​
24
// Array of defined properties in the original source.
25
// The mapping identifies the precise source location
26
// where the original annotation lives
27
// as well as the annotated target type and the target itself.
28
"propertyMap": [
29
{
30
// Property id.
31
"id": 1,
32
​
33
// Contract with the definition.
34
"contract": "Test",
35
​
36
// Original file name with the definition.
37
"filename": "sample.sol",
38
​
39
// The source range of a predicate fragment in the original file.
40
// For example annotation `if_succeeds {:msg "P0"} y == x + 1;`
41
// it would indicate the `y = x + 1` fragment.
42
"propertySource": "85:11:0",
43
​
44
// The source range of a whole annotation in the original file.
45
"annotationSource": "61:36:0",
46
​
47
// Annotation target entity.
48
"target": "function",
49
​
50
// Name of the annotation target entity.
51
"targetName": "some",
52
​
53
// The signature (4 bytes in hex) for an additional debug event.
54
"debugEventSignature": "",
55
​
56
// For example annotation `if_succeeds {:msg "P0"} y == x + 1;`
57
// it would indicate the `P0` string.
58
"message": "P0",
59
​
60
// Array of source ranges of instrumentation fragments
61
// that are corresponding to the annotation.
62
"instrumentationRanges": [
63
"251:29:0",
64
​
65
// ... may contain multiple entries ...
66
],
67
​
68
// Array of source ranges of instrumentation fragments
69
// that are corresponding to the annotation predicate check.
70
"checkRanges": [
71
"221:14:0"
72
​
73
// ... may contain multiple entries ...
74
]
75
}
76
],
77
​
78
// Array of the original source file names,
79
// that been used for generating an instrumentation.
80
"originalSourceList": [
81
"sample.sol"
82
],
83
​
84
// Array of the generated instrumentation file names.
85
// The `"--"` is indicating that instrumentation source
86
// was provided to STDOUT instead of files.
87
"instrSourceList": [
88
"--"
89
]
90
}
Copied!
Example
Assuming we have a
sample.sol file with following Solidity code:1
pragma solidity ^0.8.0;
2
​
3
/// #define inc(uint x) uint = x + 1;
4
contract Test {
5
/// #if_succeeds {:msg "P0"} y == inc(x);
6
function some(uint x) public returns (uint y) {
7
y = x + 1;
8
}
9
}
Copied!
If we run it with command:
1
scribble sample.sol --output-mode json --output --
Copied!
Scribble will produce and compile following instrumented source:
1
pragma solidity 0.8.0;
2
​
3
/// #define inc(uint x) uint = x + 1;
4
contract Test {
5
event AssertionFailed(string message);
6
​
7
function some(uint x) public returns (uint y) {
8
y = _original_Test_some(x);
9
if (!(y == inc(x))) {
10
emit AssertionFailed("1: P0");
11
assert(false);
12
}
13
}
14
​
15
function _original_Test_some(uint x) private returns (uint y) {
16
y = x + 1;
17
}
18
​
19
/// Implementation of user function define inc(uint256 x) uint256 = (x + 1)
20
function inc(uint256 x1) internal view returns (uint256) {
21
return x1 + 1;
22
}
23
}
24
/// Utility contract holding a stack counter
25
contract __scribble_ReentrancyUtils {
26
bool __scribble_out_of_contract = true;
27
}
Copied!
And then will produce following JSON output:
1
{
2
"errors": [
3
// Common output of the Solc
4
],
5
"sources": {
6
// The flattened instrumented source, produced by Scribble:
7
"flattened.sol": {
8
"ast": {
9
// Common output of the Solc
10
},
11
"id": 0,
12
​
13
// Generated instrumentation source:
14
"source": "pragma solidity 0.8.0;\n\n/// define inc(uint x) uint = x + 1;\ncontract Test {\n event AssertionFailed(string message);\n\n function some(uint x) public returns (uint y) {\n y = _original_Test_some(x);\n if (!(y == inc(x))) {\n emit AssertionFailed(\"1: P0\");\n assert(false);\n }\n }\n\n function _original_Test_some(uint x) private returns (uint y) {\n y = x + 1;\n }\n\n /// Implementation of user function define inc(uint256 x) uint256 = (x + 1)\n function inc(uint256 x1) internal view returns (uint256) {\n return x1 + 1;\n }\n}\n/// Utility contract holding a stack counter\ncontract __scribble_ReentrancyUtils {\n bool __scribble_out_of_contract = true;\n}"
15
}
16
},
17
"contracts": {
18
// Common output of the Solc
19
},
20
// Instrumentation metadata, produced by Scribble:
21
"instrumentationMetadata": {
22
"instrToOriginalMap": [
23
[
24
"61:532:0",
25
"62:139:0"
26
],
27
[
28
"330:88:0",
29
"127:72:0"
30
],
31
[
32
"358:8:0",
33
"140:8:0"
34
],
35
[
36
"359:6:0",
37
"141:6:0"
38
],
39
[
40
"359:4:0",
41
"141:4:0"
42
],
43
[
44
"383:8:0",
45
"164:8:0"
46
],
47
[
48
"384:6:0",
49
"165:6:0"
50
],
51
[
52
"384:4:0",
53
"165:4:0"
54
],
55
[
56
"392:26:0",
57
"173:26:0"
58
],
59
[
60
"402:9:0",
61
"183:9:0"
62
],
63
[
64
"402:9:0",
65
"183:9:0"
66
],
67
[
68
"402:1:0",
69
"183:1:0"
70
],
71
[
72
"406:5:0",
73
"187:5:0"
74
],
75
[
76
"406:1:0",
77
"187:1:0"
78
],
79
[
80
"410:1:0",
81
"191:1:0"
82
],
83
[
84
"221:14:0",
85
"86:36:0"
86
]
87
],
88
"otherInstrumentation": [
89
"681:38:0",
90
"571:13:0",
91
"163:6:0",
92
"181:26:0"
93
],
94
"propertyMap": [
95
{
96
"id": 1,
97
"contract": "Test",
98
"filename": "sample.sol",
99
"propertySource": "110:11:0",
100
"annotationSource": "86:36:0",
101
"target": "function",
102
"targetName": "some",
103
"debugEventSignature": "",
104
"message": "P0",
105
"instrumentationRanges": [
106
"251:29:0",
107
"217:101:0"
108
],
109
"checkRanges": [
110
"221:14:0"
111
]
112
}
113
],
114
"originalSourceList": [
115
"sample.sol"
116
],
117
"instrSourceList": [
118
"--"
119
]
120
}
121
}
Copied!
Last modified 6mo ago
Copy link