Booster 2

auxil.md

@@ -14,23 +14,24 @@ module WASM-AUXIL
 
  syntax Auxil ::= "#clearConfig"
  // -------------------------------
- rule <instrs> #clearConfig => . ... </instrs>
- <curModIdx> _ => .Int </curModIdx>
- <valstack> _ => .ValStack </valstack>
- <locals> _ => .Map </locals>
- <moduleInstances> _ => .Bag </moduleInstances>
- <moduleIds> _ => .Map </moduleIds>
- <nextModuleIdx> _ => 0 </nextModuleIdx>
- <moduleRegistry> _ => .Map </moduleRegistry>
+ rule [clearConfig]:
+ <instrs> #clearConfig => . ... </instrs>
+ <curModIdx> _ => .Int </curModIdx>
+ <valstack> _ => .ValStack </valstack>
+ <locals> _ => .MapIntToVal </locals>
+ <moduleInstances> _ => .Bag </moduleInstances>
+ <moduleIds> _ => .Map </moduleIds>
+ <nextModuleIdx> _ => 0 </nextModuleIdx>
+ <moduleRegistry> _ => .Map </moduleRegistry>
  <mainStore>
- <nextFuncAddr> _ => 0 </nextFuncAddr>
- <funcs> _ => .Bag </funcs>
- <nextTabAddr> _ => 0 </nextTabAddr>
- <tabs> _ => .Bag </tabs>
- <nextMemAddr> _ => 0 </nextMemAddr>
- <mems> _ => .Bag </mems>
- <nextGlobAddr> _ => 0 </nextGlobAddr>
- <globals> _ => .Bag </globals>
+ <nextFuncAddr> _ => 0  </nextFuncAddr>
+ <funcs> _ => .Bag  </funcs>
+ <nextTabAddr> _ => 0  </nextTabAddr>
+ <tabs> _ => .Bag  </tabs>
+ <nextMemAddr> _ => 0  </nextMemAddr>
+ <mems> _ => .Bag  </mems>
+ <nextGlobAddr> _ => 0  </nextGlobAddr>
+ <globals> _ => .Bag  </globals>
  </mainStore>
 
 endmodule

data.md

@@ -152,6 +152,8 @@ module WASM-DATA-COMMON
  imports STRING
  imports LIST
  imports MAP
+ imports MAP-INT-TO-VAL
+ imports MAP-INT-TO-VAL-PRIMITIVE
  imports FLOAT
  imports BYTES
  imports K-EQUAL
@@ -378,6 +380,10 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit
  syntax Int ::= #signed ( IValType , Int ) [function]
  | #unsigned ( IValType , Int ) [function]
  | #signedWidth ( Int , Int ) [function]
+
+ syntax Bool ::= definedSigned ( IValType, Int ) [function, total]
+ | definedUnsigned( IValType, Int ) [function, total]
+
  // ---------------------------------------------------------
  rule #signed(ITYPE, N) => N requires 0 <=Int N andBool N <Int #pow1(ITYPE)
  rule #signed(ITYPE, N) => N -Int #pow(ITYPE) requires #pow1(ITYPE) <=Int N andBool N <Int #pow (ITYPE)
@@ -390,6 +396,79 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit
  rule #signedWidth(2, N) => N requires 0 <=Int N andBool N <Int 32768
  rule #signedWidth(2, N) => N -Int 65536 requires 32768 <=Int N andBool N <Int 65536
  rule #signedWidth(4, N) => #signed(i32, N)
+
+ rule definedSigned(T:IValType, N:Int) => 0 <=Int N andBool N <Int #pow(T)
+
+ rule #Ceil(#signed(@Arg0:IValType, @Arg1:Int))
+ => (({ definedSigned(@Arg0, @Arg1) #Equals true }
+ #And #Ceil(@Arg0))
+ #And #Ceil(@Arg1))
+ [simplification]
+
+ // Should this use `N <Int #pow1(T)`? If the argument is always signed, then
+ // it should, otherwise it may be better as below.
+ rule definedUnsigned(T:IValType, N:Int) => 0 -Int #pow1(T) <=Int N andBool N <Int #pow(T)
+
+ rule #Ceil(#unsigned(@Arg0:IValType, @Arg1:Int))
+ => (({ definedUnsigned(@Arg0, @Arg1) #Equals true }
+ #And #Ceil(@Arg0))
+ #And #Ceil(@Arg1))
+ [simplification]
+
+```
+
+#### Val getters
+
+```k
+
+ syntax Int ::= getI32ValOr0(Val) [function, total]
+ | getI64ValOr0(Val) [function, total]
+
+ rule getI32ValOr0(<i32> V:Int) => V
+ rule getI32ValOr0(_:Val) => 0 [owise]
+
+ rule getI64ValOr0(<i64> V:Int) => V
+ rule getI64ValOr0(_:Val) => 0 [owise]
+
+ syntax Bool ::= isIntWithType(Val, ValType) [function, total]
+ rule isIntWithType(<T> _:Int, T:ValType) => true
+ rule isIntWithType(_:Val, _:ValType) => false [owise]
+
+```
+
+#### Int -> Val map operations
+
+mapInt2ValHasValues checks that the map has entries with the provided types,
+numbered consecutively from 0, and only those entries.
+This means that the keys are exactly 0, 1, ..., N - 1.
+
+```k
+
+ syntax Bool ::= mapInt2ValHasValues(MapIntToVal, ValTypes) [function, total]
+ | #mapInt2ValHasValues(MapIntToVal, Int, ValTypes) [function, total]
+ rule mapInt2ValHasValues(M:MapIntToVal, VTs:ValTypes)
+ => size(M) ==Int lengthValTypes(VTs) andBool #mapInt2ValHasValues(M, 0, VTs)
+ rule #mapInt2ValHasValues(M:MapIntToVal, N:Int, VT VTs)
+ => N in_keys{{M}}
+ andBool isIntWithType(M{{N}} orDefault undefined, VT)
+ andBool #mapInt2ValHasValues(M, N +Int 1, VTs)
+ requires 0 <=Int N
+ rule #mapInt2ValHasValues(_:MapIntToVal, _:Int, _:ValTypes) => true [owise]
+
+```
+
+get<ValType>FromMapOr0 extract the int form the provided key if the value has
+ValType. Returns 0 otherwise.
+
+```k
+
+ syntax Int ::= getI32FromMapOr0(MapIntToVal, Int) [function, total]
+ | getI64FromMapOr0(MapIntToVal, Int) [function, total]
+ rule getI32FromMapOr0(M:MapIntToVal, N:Int)
+ => getI32ValOr0(M{{N}} orDefault undefined)
+ rule getI64FromMapOr0(M:MapIntToVal, N:Int)
+ => getI64ValOr0(M{{N}} orDefault undefined)
+
 ```
 
 #### Boolean Interpretation
@@ -620,6 +699,24 @@ endmodule
 module WASM-DATA-SYMBOLIC [symbolic]
  imports WASM-DATA-COMMON
 
+ syntax Int ::= #signedTotal ( IValType , Int) [function, total, klabel(#signedTotal), symbol, no-evaluators, smtlib(signedTotal)]
+
+ rule #signedTotal(Arg0:IValType, Arg1:Int)
+ => #signed(Arg0, Arg1)
+ requires definedSigned(Arg0, Arg1)
+ [concrete, simplification]
+
+ rule #signed(Arg0:IValType, Arg1:Int)
+ => #signedTotal(Arg0, Arg1)
+ requires definedSigned(Arg0, Arg1)
+ [symbolic(Arg0), simplification]
+
+ rule #signed(Arg0:IValType, Arg1:Int)
+ => #signedTotal(Arg0, Arg1)
+ requires definedSigned(Arg0, Arg1)
+ [symbolic(Arg1), simplification]
+
+
  rule [wrap-Positive] : #wrap(WIDTH, N) => N &Int ((1 <<Int (WIDTH *Int 8)) -Int 1)
  requires 0 <Int WIDTH
  [concrete,simplification]

data/int-type.k

@@ -0,0 +1,11 @@
+
+module INT-TYPE
+ import INT
+
+ syntax WrappedInt
+ syntax Int
+
+ syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)]
+ syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)]
+ rule unwrap(wrap(A:Int)) => A
+endmodule