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 the standard solc compilation output with 2 additions:- In the
sourcesfield each file contains asourceproperty with the source code of the instrumented file, along with the AST. - A new
instrumentationMetadatafield is added, which 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 additional instrumented code added by scribble.
16
// I.e. this code doesn't directly correspond to un-instrumented code.
17
"otherInstrumentation": [
18
"681:38:0", // Source range in instrumented source
19
​
20
// ... may contain multiple entries ...
21
],
22
​
23
// Information for each annotation declared in the orignal code
24
"propertyMap": [
25
{
26
// Unique Annotation id (assigned internaly by scribble).
27
"id": 1,
28
​
29
// Contract where annotation was defined
30
"contract": "Test",
31
​
32
// Original file name where annotation was defined
33
"filename": "sample.sol",
34
​
35
// The source range of the annotation expression in the original file.
36
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
37
// the range would correspond to the `y = x + 1` fragment.
38
"propertySource": "85:11:0",
39
​
40
// The source range of a whole annotation in the original file.
41
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
42
// the range would correspond to the entire `if_succeeds {:msg "P0"} y == x + 1;` fragment.
43
"annotationSource": "61:36:0",
44
​
45
// Type of the annotation target (currently either function, contract, statement or state variable)
46
"target": "function",
47
​
48
// Name of the annotation target.
49
"targetName": "some",
50
​
51
// The signature (4 bytes in hex) for an additional debug event emitted when this annotation fails.
52
"debugEventSignature": "",
53
​
54
// The human-readable label for this annotation.
55
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
56
// this is the `P0` string.
57
"message": "P0",
58
​
59
// Array of source ranges of instrumentation code
60
// that corresponding to this annotation.
61
"instrumentationRanges": [
62
"251:29:0",
63
​
64
// ... may contain multiple entries ...
65
],
66
​
67
// Array of source ranges of instrumentation fragments
68
// that correspond to the annotation predicate evaluation.
69
"checkRanges": [
70
"221:14:0"
71
​
72
// ... may contain multiple entries ...
73
]
74
}
75
],
76
​
77
// Array of the original source file names,
78
// that have been instrumentated.
79
"originalSourceList": [
80
"sample.sol"
81
],
82
​
83
// Array of the generated instrumentation file names.
84
// `"--"` indicates we are outputing to STDOUT instead of files.
85
"instrSourceList": [
86
"--"
87
]
88
}
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 2mo ago
Copy link