Option evaluation (#250)

* Added target test

* Added evaultion of `Some(...)` and `None`

* Removed `ArgumentList` as it was a duplicate of `OperandList`

* Added evaluation of `Option<...>::unwrap()`

Uses internal function `#unwrap(...)` as an executed `Statement` before executing next basic block.

Passes 6 more tests, however many failing tests have changed from `4` to `113`. I believe this is not actually because of this commit, but because this commit has allowed the test to get further to run into other issues.

* Added test to demonstrate `match` works

* Whitelisted `Option` keywords

* Added `main` to `Whitelisted`

* Added token attribute to `Whitelisted`

* Removed `Whitespace` production. Using IdentifierToken instead.

* Refactored token declarations to be by relevant semantics.

Author: dkcumming

kmir/k-src/mir-lexer-syntax.md

@@ -9,9 +9,10 @@ This module defined the necessary `token` productions.
                       | LocalToken
                       | BBId
                       | DoubleHexDigitNoIntLetter
-                      | Whitelisted
 
-  syntax Whitelisted ::= "transmute" | "unwind" | "count"
+  syntax IdentifierToken ::= "transmute" [token] 
+                           | "unwind"    [token] 
+                           | "count"     [token]
 
   syntax String ::= IdentifierToken2String(IdentifierToken) [function, hook(STRING.token2string)]
   syntax IdentifierToken ::= StringIdentifierToken(String) [function, hook(STRING.string2token)]

kmir/k-src/mir-rvalue.md

@@ -119,7 +119,7 @@ The various kinds of rvalues that can appear in MIR.
   // `AssertKind` `Eq`, `Ne` conflict with BinaryOp names https://github.com/rust-lang/rust/blob/f562931178ff103f23b9e9a10dc0deb38e0d064f/library/core/src/panicking.rs#L259-L263
   syntax EnumConstructor ::= Identifier
                            | Identifier "(" OperandList ")"
-                           | PathExpression "::" Identifier
+                           | PathExpression "::" Identifier [avoid]
                            | PathExpression "::" "Eq"
                            | PathExpression "::" "Ne"
                           //  | PathExpression "::" "Match" // Match isn't conflicting at the moment but might later
@@ -138,6 +138,8 @@ The various kinds of rvalues that can appear in MIR.
   syntax OperandList ::= List{Operand, ","}
 
   syntax PtrModifiers ::= "" | "mut" | "raw" "mut" | "raw" "const"
+
+  syntax RValue ::= #unwrap(Operand)
 ```
 
 ```k
@@ -166,7 +168,10 @@ Evaluate a syntactic `RValue` into a semantics `RValueResult`. Inspired by [eval
   rule evalRValue(FN_KEY, ADDR:AddressOf)   => evalAddressOf(FN_KEY, ADDR)
   rule evalRValue(FN_KEY, CFD:CopyForDeref) => evalCopyForDeref(FN_KEY, CFD)
   rule evalRValue(FN_KEY, TUP:Tuple)        => evalTuple(FN_KEY, TUP)
+  rule evalRValue(FN_KEY, ENUM:EnumConstructor) => evalEnumConstructor(FN_KEY, ENUM) [priority(51)]
   rule evalRValue(_FN_KEY, RVALUE)          => Unsupported(RVALUE) [owise]
+
+  rule evalRValue(FN_KEY, #unwrap(OP))      => evalUnwrap(evalOperand(FN_KEY, OP)) 
 ```
 
 ### `Operand` evaluation
@@ -364,6 +369,26 @@ Locals only makes sense within a function-like, hence we evaluate them as a cont
     requires PLACE_INDEX ==Int Local2Int(PLACE)
 ```
 
+### `Enum` evaluation
+```k
+  syntax IdentifierToken ::= "Option" [token] 
+                           | "None"   [token] 
+                           | "Some"   [token] 
+                           | "unwrap" [token]
+
+  syntax MIRValue ::= evalEnumConstructor(FunctionLikeKey, EnumConstructor) [function]
+  //--------------------------------------------------------------
+  rule evalEnumConstructor( FN_KEY, Option :: < _TYPES > :: .ExpressionPathList :: Some ( OP , .OperandList ) ) => OptSome(evalOperand(FN_KEY, OP:Operand))
+  rule evalEnumConstructor(_FN_KEY, Option :: < _TYPES > :: .ExpressionPathList :: None ) => OptNone
+```
+
+### Internal Functions
+```k
+  syntax MIRValue ::= evalUnwrap(MIRValue) [function]
+  //-------------------------------------------------
+  rule evalUnwrap(OptSome( VALUE:MIRValue )) => VALUE
+```
+
 ```k
 endmodule
 ```

kmir/k-src/mir-terminator.md

@@ -59,17 +59,13 @@ These constructs need to be disambiguated at runtime. See the `MIR-AMBIGUITIES`
   syntax SwitchTargets ::= List{SwitchTarget, ","}
   syntax SwitchTarget ::= Int ":" BB
 
-  syntax CallLike ::= Callable "(" ArgumentList ")" | AssertCall
+  syntax CallLike ::= Callable "(" OperandList ")" | AssertCall
 
   syntax Callable ::= PathExpression
                     | "move" Local
 
   syntax AssertCall ::= "assert" "(" AssertArgument "," AssertKind ")"
-//   syntax AssertCall ::= "assert" "(" AssertArgumentList ")"
-  syntax AssertArgument ::= Operand | "!" Operand // | StringLiteral
-//   syntax AssertArgumentList ::= NeList{AssertArgument, ","}
-
-  syntax ArgumentList ::= List{Operand, ","}
+  syntax AssertArgument ::= Operand | "!" Operand
 
   syntax TerminatorDestination ::= BB | SwitchIntCases | CallDestination | AssertDestination
   syntax SwitchIntCases ::= "[" IntCaseList "," OtherwiseCase "]"

kmir/k-src/mir-types.md

@@ -450,9 +450,12 @@ TODO: add more domain sorts
                     | Bool
                     | "Never"
                     | TupleArgs
+                    | OptionVal
                     | "UNIMPLEMENTED"
 
   syntax TupleArgs ::= "(" MIRValueNeList ")"
+  syntax OptionVal ::= "OptSome" "(" MIRValue ")"
+                     | "OptNone"
   
   syntax RValueResult ::= MIRValue
 

kmir/k-src/mir.md

@@ -33,7 +33,7 @@ The presence of the empty program, `.Mir`, on the `<k>` cell indicates that the
 ```k
   rule <k> .Mir => #initialized() ... </k>
        <phase> Initialization </phase>
-  rule <k> #initialized() => #executeFunctionLike(Fn(String2IdentifierToken("main"):: .FunctionPath), .ArgumentList) ... </k>
+  rule <k> #initialized() => #executeFunctionLike(Fn(main :: .FunctionPath), .OperandList) ... </k>
        <phase> Initialization => Execution </phase>
 ```
 
@@ -45,11 +45,11 @@ If we are, then we stop execution and enter the finalization phase. Otherwise, i
        <callStack> ListItem(FUNCTION_KEY) => .List </callStack>
        <phase> Execution => Finalization </phase>
        <returncode> _ => 0 </returncode>
-    requires FUNCTION_KEY ==K Fn(String2IdentifierToken("main"))
+    requires FUNCTION_KEY ==K Fn(main)
 
   rule <k> #return(FUNCTION_KEY, _) => .K ... </k>
        <callStack> ListItem(FUNCTION_KEY) XS => XS </callStack>
-    requires FUNCTION_KEY =/=K Fn(String2IdentifierToken("main"))
+    requires FUNCTION_KEY =/=K Fn(main)
 endmodule
 ```
 
@@ -310,14 +310,16 @@ Executing a function-like means:
 Note that the `main` function is special: it does not have a caller.
 
 ```k
-  syntax MirSimulation ::= #executeFunctionLike(FunctionLikeKey, ArgumentList)
+  syntax IdentifierToken ::= "main" [token]
+
+  syntax MirSimulation ::= #executeFunctionLike(FunctionLikeKey, OperandList)
   //--------------------------------------------------------------------------
   rule <k> #executeFunctionLike(FN_KEY, _ARGS)
         => #executeBasicBlock(FN_KEY, 0)
         ...
        </k>
        <callStack> .List => ListItem(FN_KEY) </callStack>
-    requires FN_KEY ==K Fn(String2IdentifierToken("main"):: .FunctionPath)
+    requires FN_KEY ==K Fn(main :: .FunctionPath)
   rule <k> #executeFunctionLike(CALLEE_FN_KEY, ARGS)
         => #instantiateArguments(CALLER_FN_KEY, ARGS, 1)
         ~> #executeBasicBlock(CALLEE_FN_KEY, 0)
@@ -337,7 +339,7 @@ Note that the `main` function is special: it does not have a caller.
        <callStack> ListItem(Rec(PATH, _)) _STACK </callStack> [priority(49)]
 
   // TODO: Either save unimplemented stack frame for correct initial values, or clear values
-  syntax MirSimulation ::= #addRecursiveFrame(FunctionLikeKey, ArgumentList)
+  syntax MirSimulation ::= #addRecursiveFrame(FunctionLikeKey, OperandList)
   //-------------------------------------------------------------------------
   rule <k> #addRecursiveFrame(Fn(PATH), ARGS)
         => #instantiateArguments(Rec(PATH, 0), ARGS, 1)
@@ -364,10 +366,10 @@ Note that the `main` function is special: it does not have a caller.
 Assign arguments (actual parameters) to formal parameters of a function-like:
 
 ```k
-  syntax MirSimulation ::= #instantiateArguments(FunctionLikeKey, ArgumentList, Int)
+  syntax MirSimulation ::= #instantiateArguments(FunctionLikeKey, OperandList, Int)
   //--------------------------------------------------------------------------------
-  rule <k> #instantiateArguments(_FN_KEY, .ArgumentList, _) => .K ... </k>
-  rule <k> #instantiateArguments(FN_KEY, (ARG, REST):ArgumentList, ARGUMENT_NUMBER:Int)
+  rule <k> #instantiateArguments(_FN_KEY, .OperandList, _) => .K ... </k>
+  rule <k> #instantiateArguments(FN_KEY, (ARG, REST):OperandList, ARGUMENT_NUMBER:Int)
         => #writeLocal(CALLEE_FN_KEY, Int2Local(ARGUMENT_NUMBER), evalOperand(CALLER_FN_KEY, ARG))
         ~> #instantiateArguments(FN_KEY, REST, ARGUMENT_NUMBER +Int 1)
         ...
@@ -489,32 +491,38 @@ or panics if the function-like or the block is missing:
         ...
        </k>
        <callStack> ListItem(Fn(FNAME)) ... </callStack>
-       requires FNAME ==K toFunctionPath(OTHER_FN_NAME) [priority(49)]
+    requires FNAME ==K toFunctionPath(OTHER_FN_NAME) [priority(49)]
   rule <k> #executeTerminator(DEST_LOCAL:Local = OTHER_FN_NAME:PathInExpression ( ARGS ) -> ((NEXT:BBName _):BB))
         => #executeFunctionLike(Fn(toFunctionPath(OTHER_FN_NAME)), ARGS)
         ~> #transferLocal(Rec(toFunctionPath(OTHER_FN_NAME), DEPTH +Int 1), Int2Local(0), Rec(FNAME, DEPTH), DEST_LOCAL)
         ~> #executeBasicBlock(Rec(FNAME, DEPTH), BBName2Int(NEXT))
         ...
        </k>
        <callStack> ListItem(Rec(FNAME, DEPTH)) ... </callStack>
-       requires FNAME ==K toFunctionPath(OTHER_FN_NAME) [priority(49)]
+    requires FNAME ==K toFunctionPath(OTHER_FN_NAME) [priority(49)]
   rule <k> #executeTerminator(switchInt (ARG:Operand) -> [ TARGETS:SwitchTargets , otherwise : OTHERWISE:BB ])
         => #switchInt(FN_KEY, castMIRValueToInt(evalOperand(FN_KEY, ARG)), TARGETS, OTHERWISE)
         ...
        </k>
        <callStack> ListItem(FN_KEY) ... </callStack>
     requires isInt(castMIRValueToInt(evalOperand(FN_KEY, ARG)))
-  rule <k> #executeTerminator(_:Local = PANIC_CALL (ARG, .ArgumentList))
+  rule <k> #executeTerminator(_:Local = PANIC_CALL (ARG, .OperandList))
         => #panic(FN_KEY, PanicCall, ARG)
         ...
        </k>
        <callStack> ListItem(FN_KEY) ... </callStack>
-   requires PANIC_CALL ==K String2IdentifierToken("core") :: String2IdentifierToken("panicking") :: String2IdentifierToken("panic") :: .ExpressionPathList
+    requires PANIC_CALL ==K String2IdentifierToken("core") :: String2IdentifierToken("panicking") :: String2IdentifierToken("panic") :: .ExpressionPathList
   rule <k> #executeTerminator(TERMIANTOR:Terminator)
         => #internalPanic(FN_KEY, NotImplemented, TERMIANTOR)
         ...
        </k>
        <callStack> ListItem(FN_KEY) ... </callStack> [owise]
+
+  // Option Unwrap Call
+  rule <k> #executeTerminator(DEST_LOCAL:Local = Option :: < _TYPES > :: unwrap :: .ExpressionPathList ( ARG , .OperandList ) -> ((NEXT:BBName _):BB)) 
+        => #executeStatement(DEST_LOCAL = #unwrap(ARG)) ~> #executeBasicBlock(FN_KEY, BBName2Int(NEXT)) ...
+       </k>
+       <callStack> ListItem(FN_KEY) ... </callStack> [priority(48)]
 ```
 
 The following rule executes exists to copy a value of one local to another local, the locals may belong to different functions.