Preprocess constants (#5)

Co-authored-by: Virgil Serbanuta <Virgil Serbanuta>

Makefile

@@ -26,7 +26,6 @@ test: syntax-test indexing-test
 syntax-test: $(SYNTAX_OUTPUTS)
 
 indexing-test: $(INDEXING_OUTPUTS)
-	echo $(INDEXING_OUTPUTS)
 
 $(RUST_TIMESTAMP): $(SEMANTICS_FILES)
 	$$(which kompile) rust-semantics/rust.md -o $(RUST_KOMPILED)

rust-semantics/expression.md

@@ -0,0 +1,9 @@
+```k
+requires "expression/casts.md"
+requires "expression/literals.md"
+
+module RUST-EXPRESSION
+    imports private RUST-CASTS
+    imports private RUST-EXPRESSION-LITERALS
+endmodule
+```

rust-semantics/expression/casts.md

@@ -0,0 +1,41 @@
+```k
+
+module RUST-CASTS
+    imports private RUST-REPRESENTATION
+
+    syntax ValueOrError ::= cast(Value, Type)  [function, total]
+
+    rule cast(V:Value, T:Type) => error("Unknown cast.", ListItem(V) ListItem(T))
+        [owise]
+
+    // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast
+
+    rule cast(i32(Value), i32) => i32(Value)
+    rule cast(i32(Value), u32) => u32(Value)
+    rule cast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value)))
+    rule cast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value)))
+
+    rule cast(u32(Value), i32) => i32(Value)
+    rule cast(u32(Value), u32) => u32(Value)
+    rule cast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+
+    rule cast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value)))
+    rule cast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value)))
+    rule cast(i64(Value), i64) => i64(Value)
+    rule cast(i64(Value), u64) => u64(Value)
+
+    rule cast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u64(Value), i64) => i64(Value)
+    rule cast(u64(Value), u64) => u64(Value)
+
+    rule cast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule cast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+
+endmodule
+
+```

rust-semantics/expression/literals.md

@@ -0,0 +1,97 @@
+```k
+module RUST-EXPRESSION-LITERALS
+    imports private RUST-EXPRESSION-INTEGER-LITERALS
+endmodule
+
+module RUST-EXPRESSION-INTEGER-LITERALS
+    imports BOOL
+    imports INT
+    imports K-EQUAL-SYNTAX
+    imports STRING
+    imports private RUST-REPRESENTATION
+    imports RUST-SHARED-SYNTAX
+
+    // https://doc.rust-lang.org/stable/reference/expressions/literal-expr.html#integer-literal-expressions
+    // https://doc.rust-lang.org/stable/reference/tokens.html#number-literals
+
+    syntax String ::= IntegerLiteralToString(IntegerLiteral)  [function, total, hook(STRING.token2string)]
+
+    rule I:IntegerLiteral => parseInteger(I)
+
+    syntax ValueOrError ::= parseInteger(IntegerLiteral)  [function, total]
+                          | parseInteger(String)  [function, total]
+    rule parseInteger(I:IntegerLiteral) => parseInteger(IntegerLiteralToString(I))
+    rule parseInteger(I:String) => parseIntegerNormalized(replaceAll(I, "_", ""))
+
+    syntax ValueOrError ::= parseIntegerNormalized(String)  [function, total]
+    rule parseIntegerNormalized(I:String) => error("Literal not handled", I)
+        requires startsWith(I, "0b") orBool startsWith(I, "0x") orBool startsWith(I, "0o")
+    rule parseIntegerNormalized(I:String) => parseIntegerDecimalSplit(I, findSuffix(I))  [owise]
+
+    syntax IntegerSuffix ::= findSuffix(String)  [function, total]
+    rule findSuffix(S) => suffix(i32, 3) requires endsWith(S, "i32")
+    rule findSuffix(S) => suffix(u32, 3) requires endsWith(S, "u32")
+    rule findSuffix(S) => suffix(i64, 3) requires endsWith(S, "i64")
+    rule findSuffix(S) => suffix(u64, 3) requires endsWith(S, "u64")
+    rule findSuffix(_) => suffix(( ), 0)  [owise]
+
+    syntax IntegerSuffix ::= suffix(Type, Int)
+    syntax ValueOrError ::= parseIntegerDecimalSplit(String, IntegerSuffix)  [function, total]
+    rule parseIntegerDecimalSplit(I:String, suffix(T:Type, Length))
+        => parseIntegerDecimal(substrString(I, 0, lengthString(I) -Int Length), T)
+        requires Length <=Int lengthString(I)
+    rule parseIntegerDecimalSplit(S:String, IS:IntegerSuffix)
+        => error("parseIntegerDecimalSplit", ListItem(S) ListItem(IS))
+        [owise]
+
+    syntax ValueOrError ::= parseIntegerDecimal(String,  Type)  [function, total]
+    rule parseIntegerDecimal(I:String,  T:Type) => integerToValue(String2Int(I), T)
+        requires isDecimal(I) andBool lengthString(I) >Int 0
+    rule parseIntegerDecimal(S:String, T:Type)
+        => error("parseIntegerDecimal: Unrecognized integer", ListItem(S) ListItem(T))
+
+    syntax Bool ::= isDecimalDigit(String)  [function, total]
+    rule isDecimalDigit(S) => "0" <=String S andBool S <=String "9"
+
+    syntax Bool ::= isDecimal(String)  [function, total]
+    rule isDecimal("") => true
+    rule isDecimal(S:String) => isDecimalDigit(substrString(S, 0:Int, 1:Int)) andBool isDecimal(substrString(S, 1, lengthString(S)))
+        [owise]
+
+
+    syntax ValueOrError ::= integerToValue(Int, Type)  [function, total]
+    rule integerToValue(I:Int, i32) => i32(Int2MInt(I))
+        requires sminMInt(32) <=Int I andBool I <=Int smaxMInt(32)
+    rule integerToValue(I:Int, u32) => u32(Int2MInt(I))
+        requires uminMInt(32) <=Int I andBool I <=Int umaxMInt(32)
+    rule integerToValue(I:Int, i64) => i64(Int2MInt(I))
+        requires sminMInt(64) <=Int I andBool I <=Int smaxMInt(64)
+    rule integerToValue(I:Int, u64) => u64(Int2MInt(I))
+        requires uminMInt(64) <=Int I andBool I <=Int umaxMInt(64)
+    rule integerToValue(I:Int, ( )) => u128(Int2MInt(I))
+    rule integerToValue(I:Int, T:Type)
+        => error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem))
+        [owise]
+
+    syntax Bool ::= endsWith(containing:String, contained:String)  [function, total]
+    rule endsWith(Containing:String, Contained:String)
+        => substrString
+            ( Containing
+            , lengthString(Containing) -Int lengthString(Contained)
+            , lengthString(Containing)
+            ) ==K Contained
+        requires lengthString(Contained) <=Int lengthString(Containing)
+    rule endsWith(_, _) => false [owise]
+
+    syntax Bool ::= startsWith(containing:String, contained:String)  [function, total]
+    rule startsWith(Containing:String, Contained:String)
+        => substrString
+            ( Containing
+            , 0
+            , lengthString(Contained)
+            ) ==K Contained
+        requires lengthString(Contained) <=Int lengthString(Containing)
+    rule startsWith(_, _) => false [owise]
+
+endmodule
+```

rust-semantics/preprocessing.md

@@ -1,5 +1,6 @@
 ```k
 
+requires "preprocessing/constants.md"
 requires "preprocessing/crate.md"
 requires "preprocessing/configuration.md"
 requires "preprocessing/helpers.md"
@@ -9,11 +10,11 @@ requires "preprocessing/trait.md"
 requires "preprocessing/trait-methods.md"
 
 module RUST-PREPROCESSING
+    imports private RUST-CONSTANTS
     imports private CRATE
     imports private INITIALIZATION
     imports private TRAIT
     imports private TRAIT-METHODS
 endmodule
 
-
 ```

rust-semantics/preprocessing/configuration.md

@@ -10,7 +10,7 @@ module RUST-PREPROCESSING-CONFIGURATION
         <preprocessed>
             <constants>
                 <constant multiplicity="*" type="Map">
-                    <constant-name> my_identifier </constant-name>
+                    <constant-name> .Identifier </constant-name>
                     <constant-value> tuple(.ValueList) </constant-value>
                 </constant>
             </constants>
@@ -19,7 +19,7 @@ module RUST-PREPROCESSING-CONFIGURATION
                     <trait-path> my_identifier:TypePath </trait-path>
                     <methods>
                         <method multiplicity="*" type="Map">
-                            <method-name> my_identifier </method-name>
+                            <method-name> .Identifier </method-name>
                             <method-params> .NormalizedFunctionParameterList </method-params>
                             <method-return-type> ():Type </method-return-type>
                             <method-implementation> empty:FunctionBodyRepresentation </method-implementation>

rust-semantics/preprocessing/constants.md

@@ -0,0 +1,27 @@
+```k
+module RUST-CONSTANTS
+    imports private RUST-CASTS
+    imports private RUST-REPRESENTATION
+    imports private RUST-RUNNING-CONFIGURATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax KItem ::= setConstant(Identifier, ValueOrError)
+
+    rule
+        (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem
+        => setConstant(Name, cast(V, T))
+
+    rule
+        <k>
+            setConstant(Name, V:Value) => .K
+            ...
+        </k>
+        <constants>
+            .Bag => <constant>
+                <constant-name> Name </constant-name>
+                <constant-value> V </constant-value>
+            </constant>
+            ...
+        </constants>
+endmodule
+```

rust-semantics/preprocessing/crate.md

@@ -8,16 +8,14 @@ module CRATE
     imports private RUST-REPRESENTATION
     imports private RUST-RUNNING-CONFIGURATION
 
-    syntax MaybeIdentifier ::= ".Identifier" | Identifier
-    syntax Initializer  ::= crateParser(crate: Crate, constants: Map, traitName: MaybeIdentifier, traitFunctions: Map)
+    syntax Initializer  ::= crateParser(crate: Crate, traitName: MaybeIdentifier, traitFunctions: Map)
 
-    rule crateParser(C:Crate) => crateParser(... crate : C, constants : .Map, traitName : .Identifier, traitFunctions : .Map)
+    rule crateParser(C:Crate) => crateParser(... crate : C, traitName : .Identifier, traitFunctions : .Map)
 
     rule crateParser
         ( ... crate:
           (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate
           => (.InnerAttributes Is):Crate
-        , constants : _Constants:Map
         , traitName : _Name:MaybeIdentifier
         , traitFunctions: _TraitFunctions:Map
         )
@@ -27,7 +25,6 @@ module CRATE
           ( ... crate:
             (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
             => (.InnerAttributes (ItemAtts T):Item Is):Crate
-          , constants : _Constants:Map
           , traitName : .Identifier
           , traitFunctions: .Map
           )
@@ -38,38 +35,26 @@ module CRATE
             ( ... crate:
               (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _T:Trait):Item Is:Items):Crate
               => (.InnerAttributes Is):Crate
-            , constants : _Constants:Map
             , traitName : .Identifier => Name
             , traitFunctions: .Map => Functions
             )
 
-    // rule (.K => CI:ConstantItem:KItem)
-    //     ~> crateParser
-    //       ( ... crate:
-    //         (Atts:InnerAttributes (_ItemAtts:OuterAttributes CI:ConstantItem):Item Is:Items):Crate
-    //         => (Atts Is):Crate
-    //       , constants : _Constants:Map
-    //       , traitName : _Name:MaybeIdentifier
-    //       , traitFunctions: _TraitFunctions:Map
-    //       )
-    // rule ((const Name:Identifier : _T:Type = V:Value;):ConstantItem:KItem => .K)
-    //     ~> crateParser
-    //         ( ... crate : _C:Crate
-    //         , constants : Constants:Map => Constants[Name:Identifier:KItem <- V:Value:KItem]
-    //         , traitName : _Name:MaybeIdentifier
-    //         , traitFunctions: _TraitFunctions:Map
-    //         )
+    rule (.K => CI:ConstantItem:KItem)
+        ~> crateParser
+          ( ... crate:
+            (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility CI:ConstantItem):Item Is:Items):Crate
+            => (Atts Is):Crate
+          , traitName : _Name:MaybeIdentifier
+          , traitFunctions: _TraitFunctions:Map
+          )
 
     rule
         crateParser
             ( ... crate: (_Atts:InnerAttributes .Items):Crate
-            , constants : Constants:Map
             , traitName : Name:Identifier
             , traitFunctions: Functions:Map
             )
-          => constantInitializer
-              ( ... constantNames: keys_list(Constants), constants: Constants )
-          ~> traitInitializer(Name)
+          => traitInitializer(Name)
           ~> traitMethodInitializer
               ( ... traitName: Name
               , functionNames:keys_list(Functions), functions: Functions

rust-semantics/preprocessing/initialization.md

@@ -5,14 +5,12 @@ module INITIALIZATION
     imports private RUST-PREPROCESSING-PRIVATE-HELPERS
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 
-    rule constantInitializer(... constantNames : .List) => .K
-
     rule (.K => addMethod(TraitName, F, A))
           ~> traitMethodInitializer
               ( ... traitName : TraitName:TypePath
-              , functionNames: (ListItem(Name:Identifier) => .List) _Names:List
+              , functionNames: (ListItem(Name:Identifier:KItem) => .List) _Names:List
               , functions: _Functions:Map
-                ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map)
+                ((Name:Identifier:KItem |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map)
               )
     rule traitMethodInitializer(... functionNames: .List) => .K
 

rust-semantics/preprocessing/syntax.md

@@ -14,8 +14,6 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
 
     syntax Initializer  ::= traitParser(Trait)
                           | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier)
-                          | constantInitializer
-                                ( constantNames: List, constants: Map )
                           | traitInitializer
                                 ( traitName: TypePath
                                 )

rust-semantics/representation.md

@@ -2,13 +2,15 @@
 
 module RUST-REPRESENTATION
     imports INT
+    imports LIST  // for filling the second argument of `error`.
     imports MINT
     imports RUST-SHARED-SYNTAX
 
     syntax MInt{8}
     syntax MInt{16}
     syntax MInt{32}
     syntax MInt{64}
+    syntax MInt{128}
 
     syntax SemanticsError ::= error(String, KItem)
 
@@ -24,12 +26,22 @@ module RUST-REPRESENTATION
                     | u32(MInt{32})
                     | i64(MInt{64})
                     | u64(MInt{64})
+                    | u128(MInt{128})
                     | tuple(ValueList)
     syntax ValueList ::= List{Value, ","}
     syntax Expression ::= Value
+    syntax KResult ::= Value
+
+    syntax ValueOrError ::= Value | SemanticsError
 
     syntax Type ::= "$selftype"
 
+    syntax Identifier ::= "i32"  [token]
+                        | "u32"  [token]
+                        | "i64"  [token]
+                        | "u64"  [token]
+    syntax MaybeIdentifier ::= ".Identifier" | Identifier
+
 endmodule
 
 ```

rust-semantics/rust.md

@@ -1,11 +1,13 @@
 ```k
 requires "config.md"
+requires "expression.md"
 requires "preprocessing.md"
 requires "representation.md"
 requires "syntax.md"
 
 module RUST
   imports RUST-CONFIGURATION
+  imports RUST-EXPRESSION
   imports RUST-PREPROCESSING
   imports RUST-REPRESENTATION
   imports RUST-SHARED-SYNTAX