Skip to content

Commit 2a67a33

Browse files
emarzionemarzion
committed
wasm regression tests
1 parent dc2e22b commit 2a67a33

12 files changed

+149669
-60935
lines changed

‎test/regression-wasm-semantics-5372938/generate.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,10 +30,10 @@ do
3030
kollect "test-$spec" \
3131
./kwasm prove --backend haskell \
3232
tests/proofs/"$spec"-spec.k \
33-
--def-module KWASM-LEMMAS
33+
KWASM-LEMMAS
3434
done
3535

3636
kollect "test-wrc20" \
3737
./kwasm prove --backend haskell \
3838
tests/proofs/wrc20-spec.k \
39-
--def-module WRC20-LEMMAS
39+
WRC20-LEMMAS

‎test/regression-wasm-semantics-5372938/test-locals-spec.kore

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,12 @@ import KWASM-LEMMAS []
66

77

88
// claims
9-
// rule `<generatedTop>`(`<wasm>`(`<k>`(inj{Instrs,KItem}(`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.get__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.set__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),inj{EmptyStmts,Instrs}(`.List{"___WASM_EmptyStmts_EmptyStmt_EmptyStmts"}_EmptyStmts`(.KList)))))~>DotVar2),_3,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2),_4,_5,_6,_7,_8,_9,_10),DotVar0)=>`<generatedTop>`(`<wasm>`(`<k>`(DotVar2),_3,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2),_4,_5,_6,_7,_8,_9,_10),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(10), contentStartLine(6), org.kframework.attributes.Location(Location(6,10,9,19)), org.kframework.attributes.Source(Source(/home/ana/kore/wasm-semantics/tests/proofs/locals-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
9+
// claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{Instr,KItem}(`aLocal.get`(X))~>inj{Instr,KItem}(`aLocal.set`(X))~>_DotVar2),_0,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_ValType_Number`(_ITYPE,VAL)))),_DotVar3),_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),_0,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_ValType_Number`(_ITYPE,VAL)))),_DotVar3),_1,_2,_3,_4,_5,_6),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(11), contentStartLine(6), org.kframework.attributes.Location(Location(6,11,9,20)), org.kframework.attributes.Source(Source(/Users/emarzion/wasm-semantics/././tests/proofs/locals-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
1010
claim{} \implies{SortGeneratedTopCell{}} (
1111
\and{SortGeneratedTopCell{}} (
12-
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInstrs{}, SortKItem{}}(Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'get'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'set'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),inj{SortEmptyStmts{}, SortInstrs{}}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM'Unds'EmptyStmts'Unds'EmptyStmt'Unds'EmptyStmts'QuotRBraUnds'EmptyStmts{}())))),VarDotVar2:SortK{})),Var'Unds'3:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortCurModIdxCell{},Var'Unds'1:SortLabelDepthCell{},Var'Unds'2:SortLabelIdsCell{}),Var'Unds'4:SortModuleRegistryCell{},Var'Unds'5:SortModuleIdsCell{},Var'Unds'6:SortModuleInstancesCell{},Var'Unds'7:SortNextModuleIdxCell{},Var'Unds'8:SortMainStoreCell{},Var'Unds'9:SortDeterministicMemoryGrowthCell{},Var'Unds'10:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
12+
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(kseq{}(inj{SortInstr{}, SortKItem{}}(LblaLocal'Stop'get{}(VarX:SortInt{})),kseq{}(inj{SortInstr{}, SortKItem{}}(LblaLocal'Stop'set{}(VarX:SortInt{})),Var'Unds'DotVar2:SortK{}))),Var'Unds'0:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(Var'Unds'ITYPE:SortValType{},VarVAL:SortNumber{})))),Var'Unds'DotVar3:SortCurModIdxCell{}),Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
1313
\and{SortGeneratedTopCell{}} (
14-
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar2:SortK{}),Var'Unds'3:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortCurModIdxCell{},Var'Unds'1:SortLabelDepthCell{},Var'Unds'2:SortLabelIdsCell{}),Var'Unds'4:SortModuleRegistryCell{},Var'Unds'5:SortModuleIdsCell{},Var'Unds'6:SortModuleInstancesCell{},Var'Unds'7:SortNextModuleIdxCell{},Var'Unds'8:SortMainStoreCell{},Var'Unds'9:SortDeterministicMemoryGrowthCell{},Var'Unds'10:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{}))))
15-
[org'Stop'kframework'Stop'attributes'Stop'Source{}(), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}()]
14+
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Var'Unds'0:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(Var'Unds'ITYPE:SortValType{},VarVAL:SortNumber{})))),Var'Unds'DotVar3:SortCurModIdxCell{}),Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
15+
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/emarzion/wasm-semantics/././tests/proofs/locals-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,11,9,20)")]
1616

17-
endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}()]
17+
endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3,1,10,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/emarzion/wasm-semantics/././tests/proofs/locals-spec.k)")]

0 commit comments

Comments
 (0)