From 5ea34971c4df0ce0d18c8de7773e65a779ff8f4c Mon Sep 17 00:00:00 2001 From: Shang-Wei LIN Date: Mon, 10 Dec 2018 23:14:50 +0800 Subject: [PATCH 1/3] separate the operation into two steps. --- configuration.k | 2 +- function.k | 218 ++++++++++++++---------------------------------- 2 files changed, 63 insertions(+), 157 deletions(-) diff --git a/configuration.k b/configuration.k index 8f3382f..c9664e5 100644 --- a/configuration.k +++ b/configuration.k @@ -69,7 +69,7 @@ configuration 0 false:Bool - 0:Value + // 0:Value false:Bool diff --git a/function.k b/function.k index 559f431..9d8d24b 100644 --- a/function.k +++ b/function.k @@ -121,48 +121,59 @@ syntax SolidityItem | "#returnContract" | #BindInputParams(FParameters, Values) | #BindReturnParams(FParameters, Values) + | "#pushCallStack" + | "#popCallStack" + | #upDateCallStateBeforeExternalCall(Int) + | "#upDateCallStateAfterExternalCall" + | "#upDateCallStateBeforeInternalCall" + rule [External-Function-Call]: - functionCall(C:Int; F:Id; Vs:Values) => #Call(F,Vs) ~> #returnContract ... + ( functionCall(C:Int; F:Id; Vs:Values) => + #pushCallStack ~> + #upDateCallStateBeforeExternalCall(C) ~> + #Call(F,Vs) ~> + #upDateCallStateAfterExternalCall ~> + #popCallStack ~> + #returnContract + ) ... + + [structural] + + +rule [Internal-Function-Call]: + (functionCall(F:Id; Vs:Values) => + #pushCallStack ~> + #upDateCallStateBeforeInternalCall ~> + #Call(F,Vs) ~> + #popCallStack ~> + #return + ) ... + + [structural] + + +rule [Push-CallStack]: + #pushCallStack => . ... + CS + ( .List => ListItem(CS) ) ... + + +rule [Pop-CallStack]: + #popCallStack => . ... + _ => CS + ( ListItem(CS) => .List ) ... + + +rule [Update-CallStack-Before-ExternalCall]: + #upDateCallStateBeforeExternalCall(C) => . ... #account(C1,N1) => #account(C,N) - .List => - ListItem( - - PROGRAM - ID - CALLER - CALLDATA - CALLVALUE - Rho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC - Dep - RETURNFLAG - RETURNVALUE - EXFUNCALL - - ) ... - - PROGRAM - ID - CALLER => #account(C1,N1) - CALLDATA - CALLVALUE + ... + _ => #account(C1,N1) Rho:Map => CRho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC Dep => Dep +Int 1 RETURNFLAG => false - RETURNVALUE => #undef_Value EXFUNCALL => true @@ -171,48 +182,24 @@ rule [External-Function-Call]: ... -rule [Internal-Function-Call]: - functionCall(F:Id; Vs:Values) => #Call(F,Vs) ~> #return ... + +rule [Update-CallStack-After-ExternalCall]: + #upDateCallStateAfterExternalCall => . ... + _ => C + + ... + C + + + +rule [Update-CallStack-Before-InternalCall]: + #upDateCallStateBeforeInternalCall => . ... #account(C,N) - // ENV:Map - .List => - ListItem( - - PROGRAM - ID - CALLER - CALLDATA - CALLVALUE - Rho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC - Dep - RETURNFLAG - RETURNVALUE - EXFUNCALL - - ) ... - - PROGRAM - ID + ... CALLER => #account(C,N) - CALLDATA - CALLVALUE - Rho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC Dep => Dep +Int 1 RETURNFLAG => false - RETURNVALUE => #undef_Value EXFUNCALL => false @@ -279,100 +266,19 @@ rule rule [Local-Call-Return]: #return => V ... - - ListItem( - - PROGRAM - ID - CALLER - CALLDATA - CALLVALUE - Rho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC - Dep - RETURNFLAG - RETURNVALUE - EXFUNCALL - - ) - => .List ... - - - _ => PROGRAM - _ => ID - _ => CALLER - _ => CALLDATA - _ => CALLVALUE - _ => Rho - _ => TENV - _ => LOCALMEM - _ => GAS - _ => MEMUSED - _ => PGAS - _ => STATIC - _ => Dep - _ => RETURNFLAG - V => RETURNVALUE - false => EXFUNCALL - + V rule [External-Call-Return]: #returnContract => V ... - _ => C - - ListItem( - - PROGRAM - ID - CALLER - CALLDATA - CALLVALUE - Rho - TENV - LOCALMEM - GAS - MEMUSED - PGAS - STATIC - Dep - RETURNFLAG - RETURNVALUE - EXFUNCALL - - ) - => .List ... - - - _ => PROGRAM - _ => ID - C => CALLER - _ => CALLDATA - _ => CALLVALUE - _ => Rho - _ => TENV - _ => LOCALMEM - _ => GAS - _ => MEMUSED - _ => PGAS - _ => STATIC - _ => Dep - _ => RETURNFLAG - V => RETURNVALUE - true => EXFUNCALL - + V rule [ReturnValue]: return V:Value => #end_Exp ... + _ => V ... _:Bool => true - _:Value => V rule [Return]: From 52e087d802509c8f3315b52dcd45bc128ad543c9 Mon Sep 17 00:00:00 2001 From: sammmas Date: Tue, 11 Dec 2018 18:03:31 +0800 Subject: [PATCH 2/3] Remove extra white spaces. --- function.k | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/function.k b/function.k index 9d8d24b..c4ed217 100644 --- a/function.k +++ b/function.k @@ -129,29 +129,28 @@ syntax SolidityItem rule [External-Function-Call]: - ( functionCall(C:Int; F:Id; Vs:Values) => - #pushCallStack ~> - #upDateCallStateBeforeExternalCall(C) ~> - #Call(F,Vs) ~> + ( functionCall(C:Int; F:Id; Vs:Values) => + #pushCallStack ~> + #upDateCallStateBeforeExternalCall(C) ~> + #Call(F,Vs) ~> #upDateCallStateAfterExternalCall ~> - #popCallStack ~> - #returnContract + #popCallStack ~> + #returnContract ) ... [structural] rule [Internal-Function-Call]: - (functionCall(F:Id; Vs:Values) => - #pushCallStack ~> - #upDateCallStateBeforeInternalCall ~> - #Call(F,Vs) ~> - #popCallStack ~> - #return - ) ... + (functionCall(F:Id; Vs:Values) => + #pushCallStack ~> + #upDateCallStateBeforeInternalCall ~> + #Call(F,Vs) ~> + #popCallStack ~> + #return + ) ... [structural] - rule [Push-CallStack]: #pushCallStack => . ... From c0027db9f823ef470ba5df6164b856ade773b428 Mon Sep 17 00:00:00 2001 From: sammmas Date: Tue, 11 Dec 2018 18:19:31 +0800 Subject: [PATCH 3/3] Remove the extra white spaces from test cases. --- tests/functionCall.sol | 8 ++++---- tests/functionCall_2.sol | 7 +++---- tests/functionCall_3.sol | 10 +++++----- tests/t1.sol | 2 +- 4 files changed, 13 insertions(+), 14 deletions(-) diff --git a/tests/functionCall.sol b/tests/functionCall.sol index f67b8c8..4c975c4 100644 --- a/tests/functionCall.sol +++ b/tests/functionCall.sol @@ -28,7 +28,7 @@ contract C { function f (int x) public returns (int y) { int sum; - + if (x < 0 ) { sum = 0; } @@ -36,9 +36,9 @@ contract C { sum = x + f(x - 1); b = b + 1; } - + return sum; - + } } @@ -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) } } } diff --git a/tests/functionCall_2.sol b/tests/functionCall_2.sol index 9ccf606..c9a4ab4 100644 --- a/tests/functionCall_2.sol +++ b/tests/functionCall_2.sol @@ -5,7 +5,7 @@ contract C { function f (int x, int m) public returns (int y) { int sum; - + if (x < 0 ) { sum = 0; } @@ -13,9 +13,8 @@ contract C { sum = x + f(x - 1, m); b = b + 1; } - + return sum; - } } @@ -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) } } } diff --git a/tests/functionCall_3.sol b/tests/functionCall_3.sol index 487e5b9..565e2bc 100644 --- a/tests/functionCall_3.sol +++ b/tests/functionCall_3.sol @@ -5,7 +5,7 @@ contract C { function f (int x, int m) public returns (int y) { int sum; - + if (x < 0 ) { sum = 0; } @@ -13,9 +13,9 @@ contract C { sum = x + f(x - 1, m); b = b + 1; } - + return sum; - + } } @@ -23,10 +23,10 @@ contract C { "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) } } } \ No newline at end of file diff --git a/tests/t1.sol b/tests/t1.sol index cce2b52..3b417c0 100644 --- a/tests/t1.sol +++ b/tests/t1.sol @@ -5,7 +5,7 @@ "code" : #solidity(int sum ; sum = 3 + 4;) }, "post" : { - "mem" : #exists("sum",7) + "mem" : #exists("sum",7) } } } \ No newline at end of file