Skip to content

Commit

Permalink
Merge pull request #9 from Consensys/cfg
Browse files Browse the repository at this point in the history
Cfg
  • Loading branch information
cd1m0 authored Nov 20, 2023
2 parents 5cf8dbd + 1d40302 commit 196e596
Show file tree
Hide file tree
Showing 12 changed files with 315 additions and 7 deletions.
25 changes: 24 additions & 1 deletion scripts/gen_translation_modules.js
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,11 @@ const staticPreamble = `
.type SubdenominationT = TimeUnit | EtherUnit
.decl parent(parentId: id, childId: id)
.decl Expression(id: id)
.decl Statement(id: id)
.decl StatementWithChildren(id: id)
.decl PrimaryExpression(id: id)
.decl TypeName(id: id)
.decl ContractDefinition_linearizedBaseContracts(parentId: ContractDefinitionId, childId: ContractDefinitionId, idx: number)
.decl ContractDefinition_usedErrors(parentId: ContractDefinitionId, childId: ErrorDefinitionId, idx: number)
.decl ContractDefinition_usedEvents(parentId: ContractDefinitionId, childId: EventDefinitionId, idx: number)
Expand Down Expand Up @@ -337,6 +342,15 @@ function buildNodeDecls(name, constructor, baseName) {
}
}

if (idBaseType !== "id") {
res.push(
`${idBaseType.slice(0, -2)}(id) :- ${name}(id, ${repeat(
"_",
dynamicArgs.length + 1
).join(", ")}).`
);
}

res.push(
`.decl ${name}(id: ${name}Id, src: symbol${
dynamicArgs.length > 0 ? ", " + dynamicArgs.join(", ") : ""
Expand All @@ -346,6 +360,15 @@ function buildNodeDecls(name, constructor, baseName) {
return res;
}

function repeat(a, n) {
const res = [];
for (let i = 0; i < n; i++) {
res.push(a);
}

return res;
}

function buildNodeDeclarations(classDescs) {
const res = [];

Expand Down Expand Up @@ -811,7 +834,7 @@ function buildFactInvocation(name, constructor) {
dynamicArgs.push(dynamicArg);

if (optional) {
dynamicArgs.push(`nd.${paramName} === undefined`);
dynamicArgs.push(`nd.${paramName} !== undefined`);
}
}

Expand Down
18 changes: 16 additions & 2 deletions src/bin/cli.ts
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,11 @@ async function main() {
`Download specified kind of supported compilers to compiler cache. Supports multiple entries.`
)
.option("--run-detectors", "Run defined detecotrs")
.option("--dump", "Dump generated DL");
.option("--dump", "Dump generated DL")
.option(
"--dump-analyses <analysisName...>",
"Run analyses only and dump the results for the specified relations"
);

program.parse(process.argv);

Expand Down Expand Up @@ -287,11 +291,21 @@ async function main() {
}

if (options.runDetectors) {
const output = await analyze(units);
const output = await analyze(units, "");
console.log(getIssues(output, reader.context));

return;
}

if (options.dumpAnalyses) {
const outputDL = options.dumpAnalyses.map((x: string) => `.output ${x}`).join("\n");
const output = await analyze(units, outputDL);

for (const analysis of options.dumpAnalyses) {
console.log(analysis, output.get(analysis));
}
return;
}
}

main()
Expand Down
66 changes: 66 additions & 0 deletions src/lib/analyses/cfg/dominate.dl
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
.decl dominate(pred: id, succ: id)

/// Dominate inherits from dominateStmt for statements
dominate(pred, succ) :-
dominateStmt(pred, succ).

/// If statement A dominates statement B, then all ExpressionStatement in
/// statement A dominate all expressions in statement B
dominate(pred, succ) :-
dominateStmt(A, B),
ancestor(A, pred),
Expression(pred),
ancestor(B, succ),
Expression(succ).

/// All expressions "syntactically" inside a statement must evaluate before its
/// conisdered "executed"
dominate(pred, succ) :-
Statement(succ),
ancestor(succ, pred),
Expression(pred).

/// All expressions "syntactically" inside another expression must finish evaluating
/// before the parent expression has evaluated
dominate(pred, succ) :-
Expression(succ),
ancestor(succ, pred),
Expression(pred).

/// Assignment
dominate(pred, succ) :-
Assignment(_, _, _, _, succ, pred).

/// BinaryOperation
dominate(pred, succ) :-
BinaryOperation(boId, _, _, _, pred, succ, _, _).

/// Conditional
dominate(pred, succ) :-
Conditional(_, _, _, pred, succ, _).

dominate(pred, succ) :-
Conditional(_, _, _, pred, _, succ).

/// FunctionCall
dominate(pred, succ) :-
FunctionCall(fcId, _, _, _, _),
FunctionCall_vArguments(fcId, pred, i),
FunctionCall_vArguments(fcId, succ, i + 1).

/// IndexAccess
dominate(pred, succ) :-
IndexAccess(_, _, _, succ, pred, 1).

/// IndexRangeAccess
dominate(pred, succ) :-
IndexRangeAccess(_, _, _, succ, pred, 1, _, _).

dominate(pred, succ) :-
IndexRangeAccess(_, _, _, succ, _, _, pred, 1).

/// TupleExpression
dominate(pred, succ) :-
TupleExpression(tId, _, _, _),
TupleExpression_components(tId, pred, i),
TupleExpression_components(tId, succ, i + 1).
86 changes: 86 additions & 0 deletions src/lib/analyses/cfg/dominateStmt.dl
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
// Helper relation for expressing the CFG domination relation only between statements (and modifier invocations)
.decl dominateStmt(pred: id, succ: id)

// ForStatement
// Initialization stmt comes before body
dominateStmt(pred, succ) :-
ForStatement(_, _, succ, pred, 1, _, _, _, _).

// All stmts dominating the for dominate the init statement
dominateStmt(pred, succ) :-
ForStatement(fId, _, _, succ, 1, _, _, _, _),
dominateStmt(pred, fId).

// No init statement - all stmts dominating the for dominate the body
dominateStmt(pred, succ) :-
ForStatement(fId, _, succ, _, 0, _, _, _, _),
dominateStmt(pred, fId).

// TryStatement
dominateStmt(pred, succ) :-
TryStatement(tId, _, _),
dominateStmt(pred, tId),
TryStatement_vClauses(tId, cId, _),
TryCatchClause(cId, _, _, succ, _, _).

// BlockStatement
dominateStmt(pred, succ) :-
Block(bId, _),
dominateStmt(pred, bId),
Block_vStatements(bId, succ, 0).

dominateStmt(pred, succ) :-
Block(bId, _),
Block_vStatements(bId, pred, i),
Block_vStatements(bId, succ, i + 1).

// UncheckedBlockStatement
dominateStmt(pred, succ) :-
UncheckedBlock(bId, _),
dominateStmt(pred, bId),
UncheckedBlock_vStatements(bId, succ, 0).

dominateStmt(pred, succ) :-
UncheckedBlock(bId, _),
UncheckedBlock_vStatements(bId, pred, i),
UncheckedBlock_vStatements(bId, succ, i + 1).

// WhileStatement
dominateStmt(pred, succ) :-
WhileStatement(wId, _, _, succ),
dominateStmt(pred, wId).

// IfStatement
dominateStmt(pred, succ) :-
IfStatement(ifId, _, _, succ, _, _),
dominateStmt(pred, ifId).

dominateStmt(pred, succ) :-
IfStatement(ifId, _, _, _, succ, 1),
dominateStmt(pred, ifId).

// DoWhile statement
dominateStmt(pred, succ) :-
DoWhileStatement(dwId, _, _, succ),
dominateStmt(pred, dwId).

// ModifierInvocations
dominateStmt(pred, succ) :-
FunctionDefinition(id, _, _, _, _, _, _, _, _, _, _, _, _, _, _),
FunctionDefinition_vModifiers(id, pred, i),
modifierInvocation_isModifier(pred),
FunctionDefinition_vModifiers(id, succ, i + 1),
modifierInvocation_isModifier(pred).

// ModifierInvocations
dominateStmt(pred, succ) :-
FunctionDefinition(id, _, _, _, _, _, _, _, _, _, _, _, _, succ, 1),
FunctionDefinition_vModifiers(id, pred, i),
modifierInvocation_isModifier(pred).

// Transitivity
dominateStmt(pred, succ) :-
dominateStmt(pred, x),
dominateStmt(x, succ).

// @todo Base constructors
13 changes: 12 additions & 1 deletion src/lib/analyses/common.dl
Original file line number Diff line number Diff line change
Expand Up @@ -30,4 +30,15 @@ inherits(childContractId, baseContractId) :-

/// Specifies that a method with `methodId` belongs to contract `contractId` or one of its bases.
.decl method(contractId: ContractDefinitionId, methodId: FunctionDefinitionId)
method(contractId, methodId) :- inherits(contractId, baseId), functionIn(_ ,methodId, baseId).
method(contractId, methodId) :- inherits(contractId, baseId), functionIn(_ ,methodId, baseId).

.decl ModifierInvocation_vReferencedDeclaration(mId: id, rId: id)
ModifierInvocation_vReferencedDeclaration(mId, rId) :-
ModifierInvocation(mId, _, mNameId, _, _),
(Identifier(mNameId, _, _, _, rId); IdentifierPath(mNameId, _, _, rId)).

.decl modifierInvocation_isModifier(mid: id)
modifierInvocation_isModifier(mId) :-
ModifierInvocation(mId, _, _, _, _),
ModifierInvocation_vReferencedDeclaration(mId, rId),
ModifierDefinition(rId, _, _, _, _, _, _, _, _, _).
7 changes: 5 additions & 2 deletions src/lib/souffle.ts
Original file line number Diff line number Diff line change
Expand Up @@ -94,8 +94,11 @@ export function buildDatalog(units: sol.SourceUnit[]): string {
].join("\n");
}

export async function analyze(units: sol.SourceUnit[]): Promise<OutputRelations> {
const datalog = [buildDatalog(units)].join("\n");
export async function analyze(
units: sol.SourceUnit[],
additionalDL: string
): Promise<OutputRelations> {
const datalog = [buildDatalog(units), additionalDL].join("\n");
return souffle(datalog);
}

Expand Down
48 changes: 48 additions & 0 deletions test/analyses.spec.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
import expect from "expect";
import fse from "fs-extra";
import * as sol from "solc-typed-ast";
import { OutputRelations, analyze } from "../src";
import { searchRecursive } from "../src/lib/utils";

const samples = searchRecursive("test/samples/analyses", (fileName) => fileName.endsWith(".json"));

describe("Analyses", () => {
for (const json of samples) {
const sample = json.replace(".json", ".sol");

describe(sample, () => {
let units: sol.SourceUnit[];
let expectedOutput: OutputRelations;
let reader: sol.ASTReader;

before(async () => {
reader = new sol.ASTReader();
const result = await sol.compileSol(sample, "auto");

const data = result.data;
const errors = sol.detectCompileErrors(data);

expect(errors).toHaveLength(0);

units = reader.read(data);

expect(units.length).toBeGreaterThanOrEqual(1);

expectedOutput = fse.readJSONSync(json, {
encoding: "utf-8"
}) as OutputRelations;
});

it("Detectors produce expected results", async () => {
const targetAnalyses = [...Object.keys(expectedOutput)];
const addtionalDL = targetAnalyses.map((x: string) => `.output ${x}`).join("\n");

const analysisResults = await analyze(units, addtionalDL);

for (const [key, val] of Object.entries(expectedOutput)) {
expect(analysisResults.get(key)).toEqual(val);
}
});
});
}
});
2 changes: 1 addition & 1 deletion test/detectors.spec.ts
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ describe("Detectors", () => {
});

it("Detectors produce expected results", async () => {
const analysisResults = await analyze(units);
const analysisResults = await analyze(units, "");

const actualIssues = getIssues(analysisResults, reader.context);
expect(actualIssues).toEqual(expectedIssues);
Expand Down
11 changes: 11 additions & 0 deletions test/samples/analyses/cfg/if.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"dominateStmt": [
[7, 13],
[7, 14],
[7, 17],
[7, 18],
[7, 19],
[7, 23],
[19, 23]
]
}
14 changes: 14 additions & 0 deletions test/samples/analyses/cfg/if.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
pragma solidity 0.8.17;

contract Foo {
function main() public {
uint x = 1;
if ( x > 0 ) {
x++;
} else {
x--;
}

uint y = x;
}
}
17 changes: 17 additions & 0 deletions test/samples/analyses/cfg/while.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"dominateStmt": [
[9, 13],
[9, 20],
[9, 26],
[9, 27],
[9, 28],
[9, 30],
[13, 20],
[13, 26],
[13, 27],
[13, 28],
[13, 30],
[20, 26],
[28, 30]
]
}
15 changes: 15 additions & 0 deletions test/samples/analyses/cfg/while.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
pragma solidity 0.8.17;

contract Foo {
function main() public returns (uint) {
uint x = 1;
uint sum = 0;

while (x < 10) {
sum += x;
x = x + 1;
}

return sum;
}
}

0 comments on commit 196e596

Please sign in to comment.