Delete localCalls and rename Storage to acctStorage

kframework · Nov 19, 2018 · 48a94c3 · 48a94c3
1 parent c773e54
commit 48a94c3
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 33 deletions.
diff --git a/configuration.k b/configuration.k
@@ -67,7 +67,7 @@ configuration
                     // Not sure we need them, let's keep them around until figure it out. 
                     <static>    .K     </static>
                     <callDepth>   0    </callDepth>
-                    <localCalls> .List </localCalls>
+                    //<localCalls> .List </localCalls>
                 </callState>
 
                 // A_* (execution substate)
@@ -180,7 +180,7 @@ configuration
                     // so that the storage usage of solidity program and evm bytecode have
                     // the same effect on the storage.
 
-                    <Storage> .Map  </Storage>
+                    <acctStorage> .Map  </acctStorage>
 
                     // Q. Why include allocation rules in solidity semantics?
                     // A. 

diff --git a/contract.k b/contract.k
@@ -82,7 +82,7 @@ rule [New-Contract-Instance]:
 		<associatedContract> .K </associatedContract>
 		<availableContracts> .K </availableContracts>
 	  </code>
-	  <Storage> .Map </Storage>
+	  <acctStorage> .Map </acctStorage>
 	  <nonce> 0 </nonce>
 	  ...
        </account>)

diff --git a/expression.k b/expression.k
@@ -14,7 +14,7 @@ rule [Allocate-State-Variables]:
     <account>
         <acctID> #account(N, CN) </acctID>
         <context> CONTEXT:Map => CONTEXT[X <- #storedVar(!N:Int, T, #storage)] </context>
-        <Storage> STORAGE:Map => STORAGE[!N <- E] </Storage>
+        <acctStorage> STORAGE:Map => STORAGE[!N <- E] </acctStorage>
         ...
     </account>
 
@@ -41,7 +41,7 @@ rule [Read-State-Variables]:
     <currentAccount> #account(C, CN) </currentAccount>
     <account>
         <acctID> #account(C, CN) </acctID>
-        <Storage> ... N |-> I:Value ...</Storage>
+        <acctStorage> ... N |-> I:Value ...</acctStorage>
         ...
     </account>
 
@@ -56,7 +56,7 @@ rule [Write-State-Variables]:
     <currentAccount> #account(C, CN) </currentAccount>
     <account>
         <acctID> #account(C, CN) </acctID>
-        <Storage> ... ((N |-> _:Value) => (N |-> I)) ...</Storage>
+        <acctStorage> ... ((N |-> _:Value) => (N |-> I)) ...</acctStorage>
         ...
     </account>
 

diff --git a/function.k b/function.k
@@ -11,7 +11,6 @@ imports CONTRACT
 
 syntax State
        ::= #state(ContractInstanceSig,Map,ControlFlag)
-         | #state(Map,ControlFlag)
 
 syntax ControlFlag
        ::= #return(Bool,Value)
@@ -144,8 +143,9 @@ rule [External-Function-Call]:
 
 rule [Internal-Function-Call]:
      <k> functionCall(F:Id; Vs:Values) => #Call(F,Vs) ~> #return ... </k>
+     <currentAccount> #account(C,N) </currentAccount>
      <env> ENV:Map  </env>
-     <localCalls> .List => ListItem(#state(ENV,#return(false,#undef_Value))) ... </localCalls> 
+     <callStack> .List => ListItem(#state(#account(C,N),ENV,#return(false,#undef_Value))) ... </callStack> 
 
 rule 
      <k> #Call(F:Id, Vs:Values) => #BindInputParams(Ps, Vs) ~> #BindReturnParams(OPs, .Values) ~> #CallBody(Ss) ...</k>
@@ -193,27 +193,17 @@ rule [Call-Function-Body]:
 rule 
      <k> #CallBody(.Statements) => . ...</k>
 
-rule
-    <k> #exeStmt(S:SimpleStatement;) => S; ...</k>
-    <localCalls> ListItem(#state(_:Map,#return(false,_:Value))) ... </localCalls>
-
-rule
-     <k> #exeStmt(S:SimpleStatement;) => . ...</k>
-     <localCalls> ListItem(#state(_:Map,#return(true,_:Value))) ... </localCalls>
-
 rule
      <k> #exeStmt(S:SimpleStatement;) => S; ...</k>
-     <localCalls> .List </localCalls>
      <callStack> ListItem(#state(#account(_:Int,_:Id), _:Map, #return(false,_:Value))) ... </callStack>
 
 rule
      <k> #exeStmt(S:SimpleStatement;) => . ...</k>
-     <localCalls> .List </localCalls>
      <callStack> ListItem(#state(#account(_:Int,_:Id), _:Map, #return(true,_:Value))) ... </callStack>
 
 rule [Local-Call-Return]:
      <k> #return  => V  ... </k>
-     <localCalls> ListItem(#state(Rho,#return(_:Bool,V:Value))) => .List ... </localCalls> 
+     <callStack> ListItem(#state(C, Rho, #return(_:Bool,V:Value))) => .List ... </callStack> 
      <env> _ => Rho </env>
 
 rule [External-Call-Return]:
@@ -223,24 +213,14 @@ rule [External-Call-Return]:
      <currentAccount> _ => C  </currentAccount>
      <callDepth> Depth => Depth -Int 1 </callDepth>
 
-rule [ReturnValue-In-ExternalCall]:
+rule [ReturnValue]:
      <k> return V:Value  => #end_Exp ... </k>
-     <localCalls> .List </localCalls>
      <callStack> ListItem(#state(C, Rho, #return(_:Bool => true, _:Value => V))) ... </callStack>
 
-rule [ReturnValue-In-LocalCall]:
-     <k> return V:Value  => #end_Exp ... </k>
-     <localCalls> ListItem(#state(Rho,#return(_:Bool => true, _:Value => V))) ... </localCalls>
-
-rule [Return-In-ExternalCall]:
+rule [Return]:
      <k> return  => #end_Exp ... </k>
-     <localCalls> .List </localCalls>
      <callStack> ListItem(#state(C, Rho, #return(_:Bool => true, _:Value))) ... </callStack>
 
-rule [Return-In-LocalCall]:
-     <k> return  => #end_Exp ... </k>
-     <localCalls> ListItem(#state(Rho,#return(_:Bool => true, _:Value))) ... </localCalls>
-
 
 
 endmodule

diff --git a/statement.k b/statement.k
@@ -25,8 +25,6 @@ rule _:Value ; => .
 rule
     <k> #exeStmt(S:SimpleStatement;) => S; ...</k>
     <callStack> .List </callStack>
-    <localCalls> .List </localCalls>
-
 
 rule
    #localFunctionCall(FN:Id, ARGS:Values) => functionCall(FN; ARGS)      [structural]