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 sources field each file contains a source property with the source code of the instrumented file, along with the AST.
A new instrumentationMetadata field 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:
{
// Instrumented-to-original source mapping.
// Each entry is an array where
// first element is the source range of instrumented source,
// and second element is the corresponding source range of original source.
"instrToOriginalMap": [
[
"61:532:0", // Source range in instrumented source
"37:139:0" // Source range in original source
],
// ... may contain multiple entries ...
],
// Source ranges of additional instrumented code added by scribble.
// I.e. this code doesn't directly correspond to un-instrumented code.
"otherInstrumentation": [
"681:38:0", // Source range in instrumented source
// ... may contain multiple entries ...
],
// Information for each annotation declared in the orignal code
"propertyMap": [
{
// Unique Annotation id (assigned internaly by scribble).
"id": 1,
// Contract where annotation was defined
"contract": "Test",
// Original file name where annotation was defined
"filename": "sample.sol",
// The source range of the annotation expression in the original file.
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
// the range would correspond to the `y = x + 1` fragment.
"propertySource": "85:11:0",
// The source range of a whole annotation in the original file.
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
// the range would correspond to the entire `if_succeeds {:msg "P0"} y == x + 1;` fragment.
"annotationSource": "61:36:0",
// Type of the annotation target (currently either function, contract, statement or state variable)
"target": "function",
// Name of the annotation target.
"targetName": "some",
// The signature (4 bytes in hex) for an additional debug event emitted when this annotation fails.
"debugEventSignature": "",
// The human-readable label for this annotation.
// For example in the annotation `if_succeeds {:msg "P0"} y == x + 1;`
// this is the `P0` string.
"message": "P0",
// Array of source ranges of instrumentation code
// that corresponding to this annotation.
"instrumentationRanges": [
"251:29:0",
// ... may contain multiple entries ...
],
// Array of source ranges of instrumentation fragments
// that correspond to the annotation predicate evaluation.
"checkRanges": [
"221:14:0"
// ... may contain multiple entries ...
]
}
],
// Array of the original source file names,
// that have been instrumentated.
"originalSourceList": [
"sample.sol"
],
// Array of the generated instrumentation file names.
// `"--"` indicates we are outputing to STDOUT instead of files.
"instrSourceList": [
"--"
]
}
Example
Assuming we have a sample.sol file with following Solidity code:
pragma solidity ^0.8.0;
/// #define inc(uint x) uint = x + 1;
contract Test {
/// #if_succeeds {:msg "P0"} y == inc(x);
function some(uint x) public returns (uint y) {
y = x + 1;
}
}
