278 lines
11 KiB
Plaintext
278 lines
11 KiB
Plaintext
/* ============ Selector Functions ============ */
|
|
|
|
/* === General Infrastructure === */
|
|
sel pcs: unit -> [int]; // gives all pcs of the contract
|
|
sel pcsForOpcode: int -> [int]; // gives all pcs for a certain opcode
|
|
sel argumentForPc: int -> [int]; // gives the argument for the opcode at pc (can only be invoked pcs containing a PUSH, JUMP or JUMPI)
|
|
|
|
/* ============ Opcodes ============= */
|
|
|
|
const ADD := 0;
|
|
const AND := 1;
|
|
const LE := 2;
|
|
const PUSH := 3;
|
|
const POP := 4;
|
|
const MLOAD := 5;
|
|
const MSTORE := 6;
|
|
const SLOAD := 7;
|
|
const SSTORE := 8;
|
|
const TIMESTAMP := 9;
|
|
const BALANCE := 10;
|
|
const INPUT := 11;
|
|
const ADDRESS := 12;
|
|
const GAS := 13;
|
|
const JUMP := 14;
|
|
const JUMPI := 15;
|
|
const RETURN := 16;
|
|
const STOP := 17;
|
|
const FAIL := 18;
|
|
const CALL := 19;
|
|
|
|
/* ============ Abstract Domain and abstract operations ============ */
|
|
|
|
eqtype AbsDom := @T | @V<int>; /* Abstract Domain: @T represents the top element, V(v) concrete elements of value v */
|
|
|
|
// operation that checks whether a value is concrete (not top)
|
|
op isConcrete(a:AbsDom): bool := match a with | @T => false | _ => true;
|
|
|
|
//operation that extracts the concrete value from an abstract value (in case of @T it defaults to 0)
|
|
op extractConcrete(a:AbsDom): int := match a with | @V(x) => x | _ => 0;
|
|
|
|
op isAbstract(a:AbsDom): bool := ~ isConcrete(a);
|
|
|
|
op absAdd(a:AbsDom, b:AbsDom): AbsDom :=
|
|
match (a, b) with
|
|
| (@V(n), @V(m)) => @V(n+m)
|
|
| _ => @T;
|
|
|
|
op absAnd(a:AbsDom, b:AbsDom): AbsDom :=
|
|
match (a, b) with
|
|
| (@V(n), @V(m)) => (n > 0 && m > 0) ? (@V(1)) : (@V(0))
|
|
| _ => @T;
|
|
|
|
op absLe(a:AbsDom, b:AbsDom): AbsDom :=
|
|
match (a, b) with
|
|
| (@V(n), @V(m)) => (n <= m) ? (@V(1)) : (@V(0))
|
|
| _ => @T;
|
|
|
|
/* ============ Predicates ============ */
|
|
|
|
pred ExState{int}: int * array<AbsDom> * array<AbsDom> * AbsDom * array<AbsDom> * bool; // Execution State: <pc>, size, stack, memory, input, storage, cl (call level)
|
|
pred Exc{}: bool; // Exceptional Halting: cl, predicate signalizing exceptional halting
|
|
pred Halt{}: array<AbsDom> * AbsDom * bool; // Successful Halting: storage, return value, cl
|
|
|
|
|
|
/* ============ Abstract Rules ============ */
|
|
|
|
rule exception :=
|
|
for (!pc: int) in pcs()
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> Exc(?cl);
|
|
|
|
rule add :=
|
|
for (!pc: int) in pcsForOpcode(ADD)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 1,
|
|
?x = select ?sa (?size - 1),
|
|
?y = select ?sa (?size - 2)
|
|
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAdd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule and :=
|
|
for (!pc: int) in pcsForOpcode(AND)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 1,
|
|
?x = select ?sa (?size - 1),
|
|
?y = select ?sa (?size - 2)
|
|
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAnd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule le :=
|
|
for (!pc: int) in pcsForOpcode(LE)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 1,
|
|
?x = select ?sa (?size - 1),
|
|
?y = select ?sa (?size - 2)
|
|
=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absLe(?x, ?y)), ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule push :=
|
|
for (!pc: int) in pcsForOpcode(PUSH), (!v: int) in argumentForPc(!pc)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!pc+1}(?size + 1, store ?sa ?size @V(!v), ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule pop :=
|
|
for (!pc: int) in pcsForOpcode(POP)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1
|
|
=> ExState{!pc+1}(?size - 1, ?sa, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule mstore :=
|
|
for (!pc: int) in pcsForOpcode(MSTORE)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 2,
|
|
?p = select ?sa (?size - 1),
|
|
isConcrete(?p),
|
|
?v = select ?sa (?size - 2)
|
|
=> ExState{!pc+1}(?size - 2, ?sa, store ?mem extractConcrete(?p) ?v, ?in, ?stor, ?cl),
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 2,
|
|
?p = select ?sa (?size - 1),
|
|
isAbstract(?p)
|
|
=> ExState{!pc+1}(?size - 2, ?sa, [@T], ?in, ?stor, ?cl);
|
|
|
|
rule mload :=
|
|
for (!pc: int) in pcsForOpcode(MLOAD)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size -1),
|
|
isConcrete(?p),
|
|
?v = select ?mem (extractConcrete(?p))
|
|
=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size -1),
|
|
isAbstract(?p)
|
|
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule sload :=
|
|
for (!pc: int) in pcsForOpcode(SLOAD)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size -1),
|
|
isConcrete(?p),
|
|
?v = select ?stor extractConcrete(?p)
|
|
=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size -1),
|
|
isAbstract(?p)
|
|
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule sstore :=
|
|
for (!pc: int) in pcsForOpcode(SSTORE)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 2,
|
|
?p = select ?sa (?size -1),
|
|
isConcrete(?p),
|
|
?v = select ?sa (?size -2)
|
|
=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, store ?stor extractConcrete(?p) ?v, ?cl),
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 2,
|
|
?p = select ?sa (?size -1),
|
|
isAbstract(?p)
|
|
=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, [@T], ?cl);
|
|
|
|
rule timestamp :=
|
|
for (!pc: int) in pcsForOpcode(TIMESTAMP)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule balance :=
|
|
for (!pc: int) in pcsForOpcode(BALANCE)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1
|
|
=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule input :=
|
|
for (!pc: int) in pcsForOpcode(INPUT)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!pc+1}(?size + 1, store ?sa ?size ?in, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule address :=
|
|
for (!pc: int) in pcsForOpcode(ADDRESS)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule gas :=
|
|
for (!pc: int) in pcsForOpcode(GAS)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule jump :=
|
|
for (!pc: int) in pcsForOpcode(JUMP), (!j: int) in argumentForPc(!pc)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> ExState{!j}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule jumpi :=
|
|
for (!pc: int) in pcsForOpcode(JUMPI), (!j: int) in argumentForPc(!pc)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size - 1),
|
|
(isAbstract(?p) || extractConcrete(?p) != 0)
|
|
=> ExState{!j}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size - 1),
|
|
(isAbstract(?p) || extractConcrete(?p) = 0)
|
|
=> ExState{!pc+1}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl);
|
|
|
|
rule return :=
|
|
for (!pc: int) in pcsForOpcode(RETURN)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size >= 1,
|
|
?p = select ?sa (?size -1)
|
|
=> Halt{}(?stor, ?p, ?cl);
|
|
|
|
rule stop :=
|
|
for (!pc: int) in pcsForOpcode(STOP)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> Halt{}(?stor, @V(0), ?cl);
|
|
|
|
rule fail :=
|
|
for (!pc: int) in pcsForOpcode(FAIL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
|
|
=> Exc(?cl);
|
|
|
|
rule call1 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3
|
|
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
|
|
|
|
rule call2 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv:array<AbsDom>, ?r: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3,
|
|
Halt{}(?storInv, ?r, true)
|
|
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
|
|
|
|
rule call3 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3
|
|
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
|
|
|
|
/* ============ Initialization ============ */
|
|
|
|
rule initOp :=
|
|
clause
|
|
true
|
|
=> ExState{0}(0, [@V(0)], [@V(0)], @T, [@T], false); // execution starts at pc 0 in empty execution state
|
|
|