Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into _update-deps/runtim…
Browse files Browse the repository at this point in the history 
…everification/pyk
  • Loading branch information
devops committed Oct 24, 2023
2 parents 14dc46a + 01e0d55 commit 69bc1f3
Show file tree
Hide file tree
Showing 5 changed files with 159 additions and 30 deletions.
90 changes: 90 additions & 0 deletions data/list-int.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
require "int-type.k"

module LIST-INT
imports private INT-SYNTAX
imports private BASIC-K
imports INT-TYPE

syntax Int

syntax ListInt [hook(LIST.List)]
syntax ListInt ::= ListInt ListInt
[ left, function, total, hook(LIST.concat),
klabel(_ListInt_), symbol, smtlib(smt_seq_concat),
assoc, unit(.ListInt), element(ListIntItem),
format(%1%n%2)
]
syntax ListInt ::= ".ListInt"
[ function, total, hook(LIST.unit), klabel(.ListInt),
symbol, smtlib(smt_seq_nil), latex(\dotCt{ListInt})
]
syntax ListInt ::= ListItem(WrappedInt)
[ function, total, hook(LIST.element), klabel(ListIntItem),
symbol, smtlib(smt_seq_elem)
]
syntax WrappedInt ::= ListInt "[" Int "]"
[ function, hook(LIST.get), klabel(ListInt:get), symbol ]
syntax ListInt ::= ListInt "[" index: Int "<-" value: WrappedInt "]"
[function, hook(LIST.update), symbol, klabel(ListInt:set)]
syntax ListInt ::= makeListInt(length: Int, value: WrappedInt)
[function, hook(LIST.make)]
syntax ListInt ::= updateList(dest: ListInt, index: Int, src: ListInt)
[function, hook(LIST.updateAll)]
syntax ListInt ::= fillList(ListInt, index: Int, length: Int, value: WrappedInt)
[function, hook(LIST.fill)]
syntax ListInt ::= range(ListInt, fromFront: Int, fromBack: Int)
[function, hook(LIST.range), klabel(ListInt:range), symbol]
syntax Bool ::= WrappedInt "in" ListInt
[function, total, hook(LIST.in), symbol, klabel(_inListInt_)]
syntax Int ::= size(ListInt)
[function, total, hook(LIST.size), symbol, klabel (sizeListInt), smtlib(smt_seq_len)]
endmodule

module LIST-INT-PRIMITIVE
imports BOOL
imports INT
imports LIST-INT

syntax WrappedInt ::= ListInt "[" Int "]" "orDefault" WrappedInt
[ function, total, klabel(ListInt:getOrDefault), symbol ]

syntax Int ::= ListInt "{{" Int "}}"
[function, symbol, klabel(ListInt:primitiveLookup)]
// -----------------------------------------------------------
rule L:ListInt {{ I:Int }} => unwrap( L[ I ] )

syntax Int ::= ListInt "{{" Int "}}" "orDefault" Int
[ function, total, symbol, klabel(ListInt:primitiveLookupOrDefault) ]
// -----------------------------------------------------------------------------
rule L:ListInt {{ I:Int }} orDefault Value:Int
=> unwrap( L [I] orDefault wrap(Value) )

rule ListItem(V:WrappedInt) _:ListInt [0] orDefault _:WrappedInt
=> V
rule _:ListInt ListItem(V:WrappedInt) [-1] orDefault _:WrappedInt
=> V
rule .ListInt [_:Int] orDefault D:WrappedInt => D

rule ListItem(_:WrappedInt) L:ListInt [I:Int] orDefault D:WrappedInt
=> L[I -Int 1] orDefault D
requires 0 <Int I
rule L:ListInt ListItem(_:WrappedInt) [I:Int] orDefault D:WrappedInt
=> L[I +Int 1] orDefault D
requires I <Int 0

rule L:ListInt[I:Int] orDefault D:WrappedInt => D
requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
[simplification]

syntax ListInt ::= ListItemWrap( Int )
[function, total, symbol, klabel(ListIntItemWrap)]
rule ListItemWrap( B:Int ) => ListItem(wrap(B))


syntax ListInt ::= ListInt "{{" Int "<-" Int "}}"
[function, symbol, klabel(ListInt:primitiveSet)]
// -----------------------------------------------------------
rule L:ListInt {{ I:Int <- V:Int }}
=> L[ I <- wrap(V)]

endmodule
19 changes: 10 additions & 9 deletions data/map-int-to-int.k
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@

require "int-type.k"
// require "int-type.k"
require "list-int.k"

module MAP-INT-TO-INT
imports private BOOL-SYNTAX
imports private INT-SYNTAX
// imports private LIST-INT
// imports private LIST-INT
imports private LIST
imports private LIST-INT
imports private LIST-INT
// imports private LIST
// imports private SET-INT
imports private SET
imports INT-TYPE
Expand Down Expand Up @@ -65,18 +66,18 @@ module MAP-INT-TO-INT
// syntax SetInt ::= keys(MapIntToInt)
// [function, total, hook(MAP.keys)]

syntax List ::= "keys_list" "(" MapIntToInt ")"
[function, hook(MAP.keys_list)]
// syntax ListInt ::= "keys_list" "(" MapIntToInt ")"
// syntax List ::= "keys_list" "(" MapIntToInt ")"
// [function, hook(MAP.keys_list)]
syntax ListInt ::= "keys_list" "(" MapIntToInt ")"
[function, hook(MAP.keys_list)]

syntax Bool ::= WrappedInt "in_keys" "(" MapIntToInt ")"
[function, total, hook(MAP.in_keys)]

syntax List ::= values(MapIntToInt)
[function, hook(MAP.values)]
// syntax ListInt ::= values(MapIntToInt)
// syntax List ::= values(MapIntToInt)
// [function, hook(MAP.values)]
syntax ListInt ::= values(MapIntToInt)
[function, hook(MAP.values)]

syntax Int ::= size(MapIntToInt)
[function, total, hook(MAP.size), klabel(MapIntToInt.sizeMap), symbol]
Expand Down
24 changes: 24 additions & 0 deletions data/tools.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
require "list-int.k"

module WASM-DATA-TOOLS
imports BOOL
imports LIST-INT
imports LIST-INT-PRIMITIVE

syntax ListInt ::= setExtend(ListInt, index:Int, value:Int, default:Int) [function]

rule setExtend(L:ListInt, I:Int, V:Int, _D:Int)
=> L{{I <- V}}
requires 0 <=Int I andBool I <Int size(L)
rule setExtend(L:ListInt, I:Int, V:Int, D:Int)
=> setExtend(L ListItem(wrap(D)), I, V, D)
requires size(L) <=Int I

rule #Ceil(setExtend(_L:ListInt, I:Int, _V:Int, _D:Int)) => {true #Equals 0 <=Int I}
[simplification]

syntax Bool ::= isListIndex(Int, ListInt) [function, total]

rule isListIndex(I:Int, L:ListInt) => 0 <=Int I andBool I <Int size(L)

endmodule
14 changes: 9 additions & 5 deletions test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,13 +164,14 @@ We allow 2 kinds of actions:
rule <instrs> ( invoke ID:Identifier ENAME:WasmString .Instrs ) => invoke MODIDX ENAME ... </instrs>
<moduleIds> ... ID |-> MODIDX ... </moduleIds>
rule <instrs> invoke MODIDX:Int ENAME:WasmString => ( invoke FADDR ):Instr ... </instrs>
rule <instrs> invoke MODIDX:Int ENAME:WasmString => ( invoke FUNCADDRS {{ IDX }} orDefault -1 ):Instr ... </instrs>
<moduleInst>
<modIdx> MODIDX </modIdx>
<exports> ... ENAME |-> IDX ... </exports>
<funcAddrs> ... wrap(IDX) Int2Int|-> wrap(FADDR) ... </funcAddrs>
<funcAddrs> FUNCADDRS </funcAddrs>
...
</moduleInst>
requires isListIndex(IDX, FUNCADDRS)
rule <instrs> ( get NAME:WasmString ) => get CUR NAME ... </instrs>
<curModIdx> CUR </curModIdx>
Expand Down Expand Up @@ -375,17 +376,20 @@ This simply checks that the given function exists in the `<funcs>` cell and has

```k
syntax Assertion ::= "#assertFunction" Index FuncType VecType WasmString
syntax Assertion ::= "#assertFunctionHelper" Int FuncType VecType
// ------------------------------------------------------------------------
rule <instrs> #assertFunction IDX FTYPE LTYPE _ => . ... </instrs>
rule <instrs> #assertFunction IDX FTYPE LTYPE _ => #assertFunctionHelper (FUNCADDRS {{ IDX }} orDefault -1) FTYPE LTYPE ... </instrs>
<curModIdx> CUR </curModIdx>
<moduleInst>
<modIdx> CUR </modIdx>
<funcAddrs> ... wrap(IDX) Int2Int|-> wrap(FADDR) ... </funcAddrs>
<funcAddrs> FUNCADDRS </funcAddrs>
...
</moduleInst>
requires isListIndex(IDX, FUNCADDRS)
rule <instrs> #assertFunctionHelper ADDR FTYPE LTYPE => . ... </instrs>
<funcs>
<funcDef>
<fAddr> FADDR </fAddr>
<fAddr> ADDR </fAddr>
<fType> FTYPE </fType>
<fLocal> LTYPE </fLocal>
...
Expand Down
42 changes: 26 additions & 16 deletions wasm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ WebAssembly State and Semantics

```k
require "data.md"
require "data/list-int.k"
require "data/map-int-to-int.k"
require "data/tools.k"
require "numeric.md"
module WASM-SYNTAX
Expand Down Expand Up @@ -157,10 +159,13 @@ Semantics

```k
module WASM
imports LIST-INT
imports LIST-INT-PRIMITIVE
imports MAP-INT-TO-INT
imports MAP-INT-TO-INT-PRIMITIVE
imports WASM-COMMON-SYNTAX
imports WASM-DATA
imports WASM-DATA-TOOLS
imports WASM-NUMERIC
```

Expand All @@ -183,7 +188,7 @@ module WASM
<exports> .Map </exports>
<types> .Map </types>
<nextTypeIdx> 0 </nextTypeIdx>
<funcAddrs> .MapIntToInt </funcAddrs>
<funcAddrs> .ListInt </funcAddrs>
<nextFuncIdx> 0 </nextFuncIdx>
<tabIds> .Map </tabIds>
<tabAddrs> .Map </tabAddrs>
Expand Down Expand Up @@ -700,7 +705,7 @@ The importing and exporting parts of specifications are dealt with in the respec
<modIdx> CUR </modIdx>
<types> ... TYPIDX |-> TYPE ... </types>
<nextFuncIdx> NEXTIDX => NEXTIDX +Int 1 </nextFuncIdx>
<funcAddrs> ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }} </funcAddrs>
<funcAddrs> ADDRS => setExtend(ADDRS, NEXTIDX, NEXTADDR, -1) </funcAddrs>
...
</moduleInst>
<nextFuncAddr> NEXTADDR => NEXTADDR +Int 1 </nextFuncAddr>
Expand Down Expand Up @@ -788,7 +793,7 @@ The `#take` function will return the parameter stack in the reversed order, then
<funcAddrs> FUNCADDRS </funcAddrs>
...
</moduleInst>
requires IDX in_keys {{ FUNCADDRS }}
requires isListIndex(IDX, FUNCADDRS)
```

```k
Expand Down Expand Up @@ -1143,7 +1148,7 @@ A table index is optional and will be default to zero.
syntax ElemDefn ::= #elem(index : Int, offset : Instrs, elemSegment : Ints) [klabel(aElemDefn), symbol]
| "elem" "{" Int Ints "}"
syntax Stmt ::= #initElements ( Int, Int, MapIntToInt, Ints )
syntax Stmt ::= #initElements ( Int, Int, ListInt, Ints )
// -----------------------------------------------------
rule <instrs> #elem(TABIDX, IS, ELEMSEGMENT ) => sequenceInstrs(IS) ~> elem { TABIDX ELEMSEGMENT } ... </instrs>
Expand Down Expand Up @@ -1206,13 +1211,14 @@ The `start` component of a module declares the function index of a `start functi
```k
syntax StartDefn ::= #start(Int) [klabel(aStartDefn), symbol]
// -------------------------------------------------------------
rule <instrs> #start(IDX) => ( invoke FADDR ) ... </instrs>
rule <instrs> #start(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault -1 ) ... </instrs>
<curModIdx> CUR </curModIdx>
<moduleInst>
<modIdx> CUR </modIdx>
<funcAddrs> ... wrap(IDX) Int2Int|-> wrap(FADDR) ... </funcAddrs>
<funcAddrs> FUNCADDRS </funcAddrs>
...
</moduleInst>
requires isListIndex(IDX, FUNCADDRS)
```

Export
Expand Down Expand Up @@ -1242,30 +1248,34 @@ The value of a global gets copied when it is imported.

```k
syntax ImportDefn ::= #import(mod : WasmString, name : WasmString, ImportDesc) [klabel(aImportDefn), symbol]
| #importHelper(ImportDesc, importedAddr:Int) [klabel(aImportDefnHelper), symbol]
syntax ImportDesc ::= #funcDesc (id: OptionalId, type: Int) [klabel(aFuncDesc), symbol]
| #globalDesc (id: OptionalId, type: GlobalType) [klabel(aGlobalDesc), symbol]
| #tableDesc (id: OptionalId, type: Limits) [klabel(aTableDesc), symbol]
| #memoryDesc (id: OptionalId, type: Limits) [klabel(aMemoryDesc), symbol]
syntax Alloc ::= ImportDefn
// --------------------------------
rule <instrs> #import(MOD, NAME, #funcDesc(... type: TIDX) ) => . ... </instrs>
rule <instrs> #import(MOD, NAME, #funcDesc(...) #as FD ) => #importHelper(FD, FS2 {{ IDX }} orDefault -1) ... </instrs>
<moduleRegistry> ... MOD |-> MODIDX ... </moduleRegistry>
<moduleInst>
<modIdx> MODIDX </modIdx>
<funcAddrs> FS2 </funcAddrs>
<exports> ... NAME |-> IDX ... </exports>
...
</moduleInst>
requires isListIndex(IDX, FS2)
rule <instrs> #importHelper(#funcDesc(... type: TIDX), IMPORTEDADDR ) => . ... </instrs>
<curModIdx> CUR </curModIdx>
<moduleInst>
<modIdx> CUR </modIdx>
<types> TYPES </types>
<funcAddrs> FS => FS {{ NEXT <- ADDR }} </funcAddrs>
<funcAddrs> FS => setExtend(FS, NEXT, IMPORTEDADDR, -1) </funcAddrs>
<nextFuncIdx> NEXT => NEXT +Int 1 </nextFuncIdx>
...
</moduleInst>
<moduleRegistry> ... MOD |-> MODIDX ... </moduleRegistry>
<moduleInst>
<modIdx> MODIDX </modIdx>
<funcAddrs> ... wrap(IDX) Int2Int|-> wrap(ADDR) ... </funcAddrs>
<exports> ... NAME |-> IDX ... </exports>
...
</moduleInst>
<funcDef>
<fAddr> ADDR </fAddr>
<fAddr> IMPORTEDADDR </fAddr>
<fType> FTYPE </fType>
...
</funcDef>
Expand Down

0 comments on commit 69bc1f3

Please sign in to comment.