Vandal Static Analysis Library — Datalog Relations

The following relations are defined by the Vandal static analysis library (datalog/lib/vandal.dl) and may be used when writing new Datalog specifications.

---

• callResult(var:Variable, stmt:Statement)

  • var is a register variable in which the return value of a instruction is stored.

• checkedCallStateUpdate(callStmt:Statement)

  • callStmt is a statement whose return value is written to storage.

• checkedCallThrows(callStmt:Statement)

  • callStmt is a statement whose return value is used to conditionally execute a instruction.

• conditionVar(var: Variable, stmt:Statement)

  • var is a register variable whose value is used as the condition in stmt, which is either a or instruction.

• controls(x:Statement, y:Statement)

  • x is a conditional jump controlling the execution of the program branch containing statement y.

• controlsWith(x:Statement, y:Statement, cond:Variable)

  • Identical to controls, except that cond is the register variable used in the or instruction.

• depends(x:Variable, y:Variable)

  • Computation of the value stored in register variable x depends on the value stored in y. Transitive relation.

• unaryArith(opcode:Opcode)

  • opcode is the mnemonic of an instruction that accepts exactly one argument.

• binArith(opcode:Opcode)

  • opcode is the mnemonic of an instruction that accepts exactly two arguments.

• ternArith(opcode:Opcode)

  • opcode is the mnemonic of an instruction that accepts exactly three arguments.

• distinctArgs2(stmt:Statement, op1:Variable, op2:Variable)

  • stmt is a binArith statement with two distinct register variables as arguments: op1 and op2.

• distinctArgs3(stmt:Statement, op1:Variable, op2:Variable, op3:Variable)

  • stmt is a ternArith statement with three distinct register variables as arguments: op1, op2, and op3.

• twoDistinctArgs3(stmt:Statement, op1:Variable, op2:Variable)

  • stmt is a ternArith statement with at least two distinct register variables as arguments: op1 and op2.

• fromCallValue(var:Variable)

  • var is a register variable that stores a value derived from the return value of a statement.

• gasResult(var:Variable, stmt:Statement)

  • var is a register variable that stores the return value of stmt, which is a statement.

• gassy(stmt:Statement, var:Variable)

  • stmt is a statement with register variable var passed as an argument. The value stored in var depends on the return value of some statement.

• inaccessible(stmt:Statement)

  • stmt is either unreachable from the program entry point, or its program path is conditioned upon a value that is independent from program input.

• isThrow(stmt:Statement)

  • stmt is either a or statement.

• manipulableAddress(var:Variable)

  • var is a register variable with a runtime value that is either constant, comes directly from program input, or whose computation is dependent on program input.

• nonConstManipulable(var:Variable)

  • Same as manipulableAddress, except that the value stored in var is non-constant.

• originResult(var:Variable, stmt:Statement)

  • var is a register variable that stores the return value stmt, which is an statement.

• protectedByLoc(protectedStmt:Statement, sLoc:Value)

  • protectedStmt is a statement whose execution is controlled by a mutex-like structure. The lock/unlock state of the mutex persists in storage, at storage index sLoc, a constant value.

• reaches(p:Statement, q:Statement)

  • A path exists from statement p to statement q in the program’s control-flow graph.

• runtimeKnowable(opcode:Opcode)

  • opcode is the mnemonic of an instruction that reads from the metadata of the currently executing Ethereum transaction and/or message call.

• stateReadResult(var:Variable, stmt:Statement)

  • var is a register variable that stores the return value of stmt, an statement (i.e. value read from storage).

• stateWriteUse(var:Variable, stmt:Statement)

  • The value stored in register variable var is written to storage by the statement stmt.

• usedInStateOrCond(var:Variable, stmt:Statement)

  • Disjunction of the conditionVar and stateWriteUse relations.