Rust call expressions

rust-semantics/config.md

@@ -6,8 +6,8 @@ module RUST-CONFIGURATION
 
     configuration
         <rust>
-            <preprocessed/>
             <execution/>
+            <preprocessed/>
         </rust>
 
 endmodule

rust-semantics/execution/calls.md

@@ -41,19 +41,29 @@ module RUST-CALLS
         </k>
         <locals> _ => .Map </locals>
 
+    rule setArgs
+            ( (CP:Ptr, CPs:NormalizedCallParams)
+            , (P:NormalizedFunctionParameter, Ps:NormalizedFunctionParameterList)
+            )
+        => setArg(CP, P) ~> setArgs(CPs, Ps)
+
+    rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K
+
+    syntax Instruction ::= setArg(Ptr, NormalizedFunctionParameter)
+
     rule
         <k>
-            setArgs(
-                (ValueId:Int , Ids:NormalizedCallParams) => Ids,
-                ((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps
-            )
+            setArg
+                ( ptr(ValueId:Int)
+                , Name:ValueName : T:Type
+                )
+            => .K
             ...
         </k>
         <locals> Locals:Map => Locals[Name <- ValueId] </locals>
         <values> ValueId |-> Value ... </values>
-        requires notBool Name in_keys(Locals) andBool isSameType(Value, T)
-
-    rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K
+        requires notBool Name in_keys(Locals)
+            andBool isSameType(Value, T)
 
 endmodule
 

rust-semantics/expression.md

@@ -1,13 +1,19 @@
 ```k
+requires "expression/calls.md"
 requires "expression/constants.md"
 requires "expression/casts.md"
 requires "expression/literals.md"
+requires "expression/references.md"
+requires "expression/tools.md"
 requires "expression/variables.md"
 
 module RUST-EXPRESSION
     imports private RUST-CASTS
+    imports private RUST-EXPRESSION-CALLS
+    imports private RUST-EXPRESSION-CONSTANTS
     imports private RUST-EXPRESSION-LITERALS
+    imports private RUST-EXPRESSION-REFERENCES
+    imports private RUST-EXPRESSION-TOOLS
     imports private RUST-EXPRESSION-VARIABLES
-    imports private RUST-EXPRESSION-CONSTANTS
 endmodule
 ```

rust-semantics/expression/calls.md

@@ -0,0 +1,97 @@
+```k
+
+module RUST-EXPRESSION-CALLS
+    imports private COMMON-K-CELL
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-EXPRESSION-TOOLS
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax Instruction ::= methodCall
+                ( traitName: TypePath
+                , method: Identifier
+                , params: CallParamsList
+                , reversedNormalizedParams: NormalizedCallParams
+                )
+
+    syntax NormalizedCallParams ::= reverse(NormalizedCallParams, NormalizedCallParams)  [function, total]
+    rule reverse(.NormalizedCallParams, R:NormalizedCallParams) => R
+    rule reverse((P, Ps:NormalizedCallParams), R:NormalizedCallParams) => reverse(Ps, (P, R))
+
+    rule SelfName:Expression . MethodName:Identifier ( )
+        => methodCall(... self: SelfName, method: MethodName, params: .CallParamsList)
+    rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList )
+        => methodCall(... self: SelfName, method: MethodName, params: Args)
+    rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList, )
+        => methodCall(... self: SelfName, method: MethodName, params: Args)
+
+    rule
+        <k>
+            methodCall
+                (... self: ptrValue(ptr(A) #as P, _)
+                , method: MethodName:Identifier
+                , params: Args:CallParamsList
+                )
+            => methodCall
+                (... traitName: TraitName
+                , method: MethodName
+                , params: Args
+                , reversedNormalizedParams: P, .NormalizedCallParams
+                )
+            ...
+        </k>
+        <values> A |-> struct(TraitName:TypePath, _) ... </values>
+        requires isValueWithPtr(Args)
+
+    rule methodCall
+            (... traitName: _TraitName:TypePath
+            , method: _MethodName:Identifier
+            , params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps
+            , reversedNormalizedParams: Args:NormalizedCallParams
+                => P, Args
+            )
+    rule
+        <k>
+            methodCall
+                (... traitName: _TraitName:TypePath
+                , method: _MethodName:Identifier
+                , params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps
+                , reversedNormalizedParams: Args:NormalizedCallParams
+                    => ptr(NextId), Args
+                )
+            ...
+        </k>
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <values> Values:Map => Values[NextId <- V] </values>
+    rule
+        methodCall
+            (... traitName: TraitName:TypePath
+            , method: MethodName:Identifier
+            , params: .CallParamsList
+            , reversedNormalizedParams: Args:NormalizedCallParams
+            )
+        => normalizedMethodCall
+            ( TraitName
+            , MethodName
+            , reverse(Args, .NormalizedCallParams)
+            )
+
+    // Apparently contexts need the type of the HOLE to be K, and I'm not sure
+    // how to transform CallParamsList in some sort of K combination in a
+    // reasonable way. We're using heat/cool rules instead.
+    rule (.K => HOLE) ~> HOLE:Expression , _:CallParamsList
+        [heat, result(ValueWithPtr)]
+    rule (HOLE:Expression ~> (_:Expression , L:CallParamsList):CallParamsList)
+            => HOLE , L
+        [cool, result(ValueWithPtr)]
+    rule (.K => HOLE) ~> V:Expression , HOLE:CallParamsList
+        requires isValueWithPtr(V)
+        [heat, result(ValueWithPtr)]
+    rule (HOLE:CallParamsList ~> V:Expression , _:CallParamsList)
+        => V , HOLE
+        requires isValueWithPtr(V)
+        [cool, result(ValueWithPtr)]
+endmodule
+
+```

rust-semantics/expression/casts.md

@@ -36,6 +36,8 @@ module RUST-CASTS
     rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
     rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
+    rule implicitCast(struct(T, _) #as V, T) => V
+
     // Rewrites
 
     rule ptrValue(P:Ptr, V:Value) ~> implicitCastTo(T:Type) => wrapPtrValueOrError(P, implicitCast(V, T))

rust-semantics/expression/constants.md

@@ -9,6 +9,11 @@ module RUST-EXPRESSION-CONSTANTS
     rule <k> Name:Identifier::.PathExprSegments => ptrValue(null, V) ... </k>
         <constant-name> Name </constant-name>
         <constant-value> V:Value </constant-value>
+        requires notBool isLocalVariable(Name)
 
+    rule [[isConstant(Name:Identifier) => true]]
+        <constant-name> Name </constant-name>
+        requires notBool isLocalVariable(Name)
+    rule isConstant(_Name:ValueName) => false  [owise]
 endmodule
 ```

rust-semantics/expression/references.md

@@ -0,0 +1,11 @@
+```k
+
+module RUST-EXPRESSION-REFERENCES
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+
+    rule & E:Expression => E
+
+endmodule
+
+```

rust-semantics/expression/tools.md

@@ -0,0 +1,15 @@
+```k
+
+module RUST-EXPRESSION-TOOLS
+    imports private BOOL
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-VALUE-SYNTAX
+
+    rule isValueWithPtr(_) => false  [owise]
+    rule isValueWithPtr(_:PtrValue) => true
+    rule isValueWithPtr(.CallParamsList) => true
+    rule isValueWithPtr(P:Expression , Ps:CallParamsList) => isValueWithPtr(P) andBool isValueWithPtr(Ps)
+endmodule
+
+```

rust-semantics/expression/variables.md

@@ -1,10 +1,11 @@
 ```k
 
 module RUST-EXPRESSION-VARIABLES
-    imports COMMON-K-CELL
-    imports RUST-EXECUTION-CONFIGURATION
-    imports RUST-VALUE-SYNTAX
-    imports RUST-SHARED-SYNTAX
+    imports private COMMON-K-CELL
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-VALUE-SYNTAX
 
     rule
         <k>
@@ -13,6 +14,20 @@ module RUST-EXPRESSION-VARIABLES
         </k>
         <locals> Variable |-> VarId:Int ... </locals>
         <values> VarId |-> V:Value ... </values>
+
+    rule
+        <k>
+            self :: .PathExprSegments => ptrValue(ptr(VarId), V)
+            ...
+        </k>
+        <locals> self:PathIdentSegment |-> VarId:Int ... </locals>
+        <values> VarId |-> V:Value ... </values>
+
+    rule [[isLocalVariable(Name:ValueName) => true]]
+        <locals> Locals </locals>
+        requires Name in_keys(Locals)
+    rule isLocalVariable(_) => false  [owise]
+
 endmodule
 
 ```

rust-semantics/helpers.md

@@ -10,6 +10,7 @@ module RUST-HELPERS
 
     syntax Bool ::= isSameType(Value, Type)  [function, total]
     rule isSameType(_, _) => false  [owise]
+    rule isSameType(_:Value, & T => T)
     rule isSameType(_, $selftype) => true
     rule isSameType(i64(_), i64) => true
     rule isSameType(u64(_), u64) => true

rust-semantics/preprocessing/syntax.md

@@ -28,8 +28,6 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
                                 OuterAttributes
                             )
 
-    // TODO: Move to a more generic place
-    syntax Identifier ::= "self"  [token]
 endmodule
 
 ```

rust-semantics/representation.md

@@ -50,13 +50,21 @@ module RUST-REPRESENTATION
 
     syntax FunctionBodyRepresentation ::= block(BlockExpression)
                                         | "empty"
-    syntax NormalizedFunctionParameter ::= Identifier ":" Type
+                                        | storageAccessor(StringLiteral)
+    syntax ValueName ::= Identifier | SelfSort
+    syntax NormalizedFunctionParameter ::= ValueName ":" Type
     syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","}
 
-    syntax NormalizedCallParams ::=List{Int, ","}
+    syntax NormalizedCallParams ::=List{Ptr, ","}
 
     syntax Instruction  ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams)
                           | implicitCastTo(Type)
+                          | methodCall
+                              ( self: Expression
+                              , method:Identifier
+                              , params: CallParamsList
+                              )
+                            [seqstrict(1, 3), result(ValueWithPtr)]
 
     syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
 
@@ -68,6 +76,12 @@ module RUST-REPRESENTATION
                         | "u64"  [token]
     syntax MaybeIdentifier ::= ".Identifier" | Identifier
 
+    syntax ExpressionOrCallParams ::= Expression | CallParams 
+
+    syntax Bool ::= isConstant(ValueName)  [function, total]
+    syntax Bool ::= isLocalVariable(ValueName)  [function, total]
+    syntax Bool ::= isValueWithPtr(K)  [function, total, symbol(isValueWithPtr)]
+
 endmodule
 
 ```