Skip to content

Commit

Permalink
separate the <callStack> operation into two steps (StackOperation-2St…
Browse files Browse the repository at this point in the history 
…eps)
  • Loading branch information
Everett Hildenbrandt committed Dec 11, 2018
2 parents cddf1f5 + c0027db commit 6ad4362
Show file tree
Hide file tree
Showing 6 changed files with 75 additions and 171 deletions.
2 changes: 1 addition & 1 deletion configuration.k
View file
Expand Up @@ -69,7 +69,7 @@ configuration
<callDepth> 0 </callDepth>

<returnFlag> false:Bool </returnFlag>
<returnValue> 0:Value </returnValue>
//<returnValue> 0:Value </returnValue>
<isExternalFunctionCall> false:Bool </isExternalFunctionCall>
</callState>

Expand Down
217 changes: 61 additions & 156 deletions function.k
View file
Expand Up @@ -121,48 +121,58 @@ syntax SolidityItem
| "#returnContract"
| #BindInputParams(FParameters, Values)
| #BindReturnParams(FParameters, Values)
| "#pushCallStack"
| "#popCallStack"
| #upDateCallStateBeforeExternalCall(Int)
| "#upDateCallStateAfterExternalCall"
| "#upDateCallStateBeforeInternalCall"


rule [External-Function-Call]:
<k> functionCall(C:Int; F:Id; Vs:Values) => #Call(F,Vs) ~> #returnContract ...</k>
<k> ( functionCall(C:Int; F:Id; Vs:Values) =>
#pushCallStack ~>
#upDateCallStateBeforeExternalCall(C) ~>
#Call(F,Vs) ~>
#upDateCallStateAfterExternalCall ~>
#popCallStack ~>
#returnContract
) ...
</k>
[structural]


rule [Internal-Function-Call]:
<k> (functionCall(F:Id; Vs:Values) =>
#pushCallStack ~>
#upDateCallStateBeforeInternalCall ~>
#Call(F,Vs) ~>
#popCallStack ~>
#return
) ...
</k>
[structural]

rule [Push-CallStack]:
<k> #pushCallStack => . ... </k>
<callState> CS </callState>
<callStack> ( .List => ListItem(CS) ) ... </callStack>


rule [Pop-CallStack]:
<k> #popCallStack => . ... </k>
<callState> _ => CS </callState>
<callStack> ( ListItem(CS) => .List ) ... </callStack>


rule [Update-CallStack-Before-ExternalCall]:
<k> #upDateCallStateBeforeExternalCall(C) => . ... </k>
<currentAccount> #account(C1,N1) => #account(C,N) </currentAccount>
<callStack> .List =>
ListItem(
<callState>
<program> PROGRAM </program>
<id> ID </id>
<caller> CALLER </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
<env> Rho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep </callDepth>
<returnFlag> RETURNFLAG </returnFlag>
<returnValue> RETURNVALUE </returnValue>
<isExternalFunctionCall> EXFUNCALL </isExternalFunctionCall>
</callState>
) ...
</callStack>
<callState>
<program> PROGRAM </program>
<id> ID </id>
<caller> CALLER => #account(C1,N1) </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
...
<caller> _ => #account(C1,N1) </caller>
<env> Rho:Map => CRho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep => Dep +Int 1 </callDepth>
<returnFlag> RETURNFLAG => false </returnFlag>
<returnValue> RETURNVALUE => #undef_Value </returnValue>
<isExternalFunctionCall> EXFUNCALL => true </isExternalFunctionCall>
</callState>
<account>
Expand All @@ -171,48 +181,24 @@ rule [External-Function-Call]:
...
</account>

rule [Internal-Function-Call]:
<k> functionCall(F:Id; Vs:Values) => #Call(F,Vs) ~> #return ... </k>

rule [Update-CallStack-After-ExternalCall]:
<k> #upDateCallStateAfterExternalCall => . ... </k>
<currentAccount> _ => C </currentAccount>
<callState>
...
<caller> C </caller>
</callState>


rule [Update-CallStack-Before-InternalCall]:
<k> #upDateCallStateBeforeInternalCall => . ... </k>
<currentAccount> #account(C,N) </currentAccount>
//<env> ENV:Map </env>
<callStack> .List =>
ListItem(
<callState>
<program> PROGRAM </program>
<id> ID </id>
<caller> CALLER </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
<env> Rho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep </callDepth>
<returnFlag> RETURNFLAG </returnFlag>
<returnValue> RETURNVALUE </returnValue>
<isExternalFunctionCall> EXFUNCALL </isExternalFunctionCall>
</callState>
) ...
</callStack>
<callState>
<program> PROGRAM </program>
<id> ID </id>
...
<caller> CALLER => #account(C,N) </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
<env> Rho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep => Dep +Int 1 </callDepth>
<returnFlag> RETURNFLAG => false </returnFlag>
<returnValue> RETURNVALUE => #undef_Value </returnValue>
<isExternalFunctionCall> EXFUNCALL => false </isExternalFunctionCall>
</callState>

Expand Down Expand Up @@ -279,100 +265,19 @@ rule

rule [Local-Call-Return]:
<k> #return => V ... </k>
<callStack>
ListItem(
<callState>
<program> PROGRAM </program>
<id> ID </id>
<caller> CALLER </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
<env> Rho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep </callDepth>
<returnFlag> RETURNFLAG </returnFlag>
<returnValue> RETURNVALUE </returnValue>
<isExternalFunctionCall> EXFUNCALL </isExternalFunctionCall>
</callState>
)
=> .List ...
</callStack>
<callState>
<program> _ => PROGRAM </program>
<id> _ => ID </id>
<caller> _ => CALLER </caller>
<callData> _ => CALLDATA </callData>
<callValue> _ => CALLVALUE </callValue>
<env> _ => Rho </env>
<tenv> _ => TENV </tenv>
<localMem> _ => LOCALMEM </localMem>
<gas> _ => GAS </gas>
<memoryUsed> _ => MEMUSED </memoryUsed>
<previousGas> _ => PGAS </previousGas>
<static> _ => STATIC </static>
<callDepth> _ => Dep </callDepth>
<returnFlag> _ => RETURNFLAG </returnFlag>
<returnValue> V => RETURNVALUE </returnValue>
<isExternalFunctionCall> false => EXFUNCALL </isExternalFunctionCall>
</callState>
<result> V </result>

rule [External-Call-Return]:
<k> #returnContract => V ... </k>
<currentAccount> _ => C </currentAccount>
<callStack>
ListItem(
<callState>
<program> PROGRAM </program>
<id> ID </id>
<caller> CALLER </caller>
<callData> CALLDATA </callData>
<callValue> CALLVALUE </callValue>
<env> Rho </env>
<tenv> TENV </tenv>
<localMem> LOCALMEM </localMem>
<gas> GAS </gas>
<memoryUsed> MEMUSED </memoryUsed>
<previousGas> PGAS </previousGas>
<static> STATIC </static>
<callDepth> Dep </callDepth>
<returnFlag> RETURNFLAG </returnFlag>
<returnValue> RETURNVALUE </returnValue>
<isExternalFunctionCall> EXFUNCALL </isExternalFunctionCall>
</callState>
)
=> .List ...
</callStack>
<callState>
<program> _ => PROGRAM </program>
<id> _ => ID </id>
<caller> C => CALLER </caller>
<callData> _ => CALLDATA </callData>
<callValue> _ => CALLVALUE </callValue>
<env> _ => Rho </env>
<tenv> _ => TENV </tenv>
<localMem> _ => LOCALMEM </localMem>
<gas> _ => GAS </gas>
<memoryUsed> _ => MEMUSED </memoryUsed>
<previousGas> _ => PGAS </previousGas>
<static> _ => STATIC </static>
<callDepth> _ => Dep </callDepth>
<returnFlag> _ => RETURNFLAG </returnFlag>
<returnValue> V => RETURNVALUE </returnValue>
<isExternalFunctionCall> true => EXFUNCALL </isExternalFunctionCall>
</callState>
<result> V </result>


rule [ReturnValue]:
<k> return V:Value => #end_Exp ... </k>
<result> _ => V </result>
<callState>
...
<returnFlag> _:Bool => true </returnFlag>
<returnValue> _:Value => V </returnValue>
</callState>

rule [Return]:
Expand Down
8 changes: 4 additions & 4 deletions tests/functionCall.sol
View file
Expand Up @@ -28,17 +28,17 @@ contract C {

function f (int x) public returns (int y) {
int sum;

if (x < 0 ) {
sum = 0;
}
else {
sum = x + f(x - 1);
b = b + 1;
}

return sum;

}
}

Expand All @@ -49,7 +49,7 @@ contract C {
"code" : #solidity( functionCall(new C();f;1); new B(); int sum ; sum = 3 + 4;)
},
"post" : {
"mem" : #exists("sum",7)
"mem" : #exists("sum",7)
}
}
}
7 changes: 3 additions & 4 deletions tests/functionCall_2.sol
View file
Expand Up @@ -5,17 +5,16 @@ contract C {

function f (int x, int m) public returns (int y) {
int sum;

if (x < 0 ) {
sum = 0;
}
else {
sum = x + f(x - 1, m);
b = b + 1;
}

return sum;

}
}

Expand All @@ -26,7 +25,7 @@ contract C {
"code" : #solidity( int sum; sum = functionCall(new C();f;2, 1); )
},
"post" : {
"mem" : #exists("sum",3)
"mem" : #exists("sum",3)
}
}
}
10 changes: 5 additions & 5 deletions tests/functionCall_3.sol
View file
Expand Up @@ -5,28 +5,28 @@ contract C {

function f (int x, int m) public returns (int y) {
int sum;

if (x < 0 ) {
sum = 0;
}
else {
sum = x + f(x - 1, m);
b = b + 1;
}

return sum;

}
}

{

"Test1" : {
"exec" : {
"code" : #solidity( int sum = functionCall(new C();f;2, 1); )
"code" : #solidity( int sum = functionCall(new C();f;3, 1); )
},
"post" : {
"mem" : #exists("sum",3)
"mem" : #exists("sum",6)
}
}
}
2 changes: 1 addition & 1 deletion tests/t1.sol
View file
Expand Up @@ -5,7 +5,7 @@
"code" : #solidity(int sum ; sum = 3 + 4;)
},
"post" : {
"mem" : #exists("sum",7)
"mem" : #exists("sum",7)
}
}
}

0 comments on commit 6ad4362

Please sign in to comment.