Skip to content

Update wasm regression tests #1774

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 56 commits into from
Apr 29, 2020
Merged

Update wasm regression tests #1774

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
91c6427
Concrete implementation of ==K
ana-pantilie Mar 30, 2020
be19564
Builtin simplification rules for Bool and KEqual
ana-pantilie Apr 2, 2020
f8d13f1
WIP: remove/fix tests
ana-pantilie Apr 3, 2020
80b9f5f
Fixes + remove unit tests
ana-pantilie Apr 8, 2020
e663933
Update K release + fix imp specs
ana-pantilie Apr 8, 2020
e95961d
Re-generate evm-semantics regression tests
ana-pantilie Apr 8, 2020
0961fba
Fix + commented debugging traces
ana-pantilie Apr 10, 2020
7734c81
Fix
ana-pantilie Apr 13, 2020
a4dcb4a
Remove new evm-semantics regression tests
ana-pantilie Apr 13, 2020
c2a1362
Merge remote-tracking branch 'upstream/master' into no-branch-kequals
ana-pantilie Apr 13, 2020
439042b
Add test inspired by evm-semantics
ana-pantilie Apr 13, 2020
62de1dc
Add new evm-semantics regression tests
ana-pantilie Apr 13, 2020
bb8c735
Remove old evm-semantics regression tests
ana-pantilie Apr 13, 2020
db7b34d
Remove unused import
ana-pantilie Apr 13, 2020
eb8e3d0
Fix golden for pop1
ana-pantilie Apr 14, 2020
2cc4ad6
Remove wasm-semantics loops and memory-symbolic
ana-pantilie Apr 14, 2020
f48efef
Clean-up
ana-pantilie Apr 14, 2020
75298d8
Add another internal simplification rule
ana-pantilie Apr 15, 2020
cc5b659
Merge remote-tracking branch 'upstream/master' into no-branch-kequals
ana-pantilie Apr 15, 2020
6ef6bf7
Merge remote-tracking branch 'upstream/master' into no-branch-kequals
ana-pantilie Apr 21, 2020
404fbbe
Partially address review comments
ana-pantilie Apr 21, 2020
4c859a6
Add and remove semantics
ana-pantilie Apr 21, 2020
6653664
Review
ana-pantilie Apr 21, 2020
7e2ca0b
Remove accidentally added files
ana-pantilie Apr 21, 2020
b4bbbd1
Update kwasm with local frontend and no local semantics modifs
ana-pantilie Apr 21, 2020
4f9b9fa
Revert "Update kwasm with local frontend and no local semantics modifs"
ana-pantilie Apr 21, 2020
f0fb54d
Kwasm update
ana-pantilie Apr 21, 2020
d35c660
Fix KEqual unit tests
ana-pantilie Apr 21, 2020
8599de5
Revert remove tests
ana-pantilie Apr 21, 2020
a612075
Clean-up
ana-pantilie Apr 21, 2020
23557be
Rename wasm-semantics test directory
ana-pantilie Apr 21, 2020
7ab36ba
Revert imp changes
ana-pantilie Apr 21, 2020
6dfcb4c
Part of review
ana-pantilie Apr 23, 2020
b9c76dc
WIP dependency inversion, stuck at Simplification.Condition.create
ana-pantilie Apr 24, 2020
700f267
WIP dependency inversion, stuck at MonadSimplify.simplifyCondition
ana-pantilie Apr 24, 2020
35fbef6
WIP: redo refactoring
ana-pantilie Apr 27, 2020
cdc421f
Refactoring now compiles
ana-pantilie Apr 27, 2020
a41fe55
UnifierT with ReaderT ConditionSimplifier
ana-pantilie Apr 27, 2020
334630e
Remove undefineds
ana-pantilie Apr 28, 2020
db6d22b
Fix bug
ana-pantilie Apr 28, 2020
91d1b36
WIP clean-up: KEqual src and test
ana-pantilie Apr 28, 2020
ef956b5
WIP clean-up: AndTerms
ana-pantilie Apr 28, 2020
aeed1f9
General clean-up
ana-pantilie Apr 28, 2020
3873059
UnifierT: factor out evaluating the ReaderT
ana-pantilie Apr 28, 2020
5eed3ad
KEqual: Bug fix
ana-pantilie Apr 28, 2020
b208a45
Merge remote-tracking branch 'upstream/master' into no-branch-kequals
ana-pantilie Apr 28, 2020
1221789
Lint
ana-pantilie Apr 28, 2020
09c3164
Bug fixes
ana-pantilie Apr 28, 2020
21914ec
Update kore/src/Kore/Builtin/Bool.hs
ana-pantilie Apr 28, 2020
85fc565
Fix test
ana-pantilie Apr 28, 2020
d7db16a
Update kwasm
ana-pantilie Apr 28, 2020
dccdccb
Merge remote-tracking branch 'upstream/master' into no-branch-kequals
ana-pantilie Apr 28, 2020
2956069
Clean-up
ana-pantilie Apr 28, 2020
f7167c3
Add wrc20 spec
ana-pantilie Apr 29, 2020
2baf949
Revert KEqual changes
ana-pantilie Apr 29, 2020
77c2cdf
Remove KEqual test
ana-pantilie Apr 29, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
0 ...egression-wasm-semantics-840390f/Makefile → ...egression-wasm-semantics-75baf9b/Makefile
View file
Open in desktop
File renamed without changes.
5 changes: 5 additions & 0 deletions ...ession-wasm-semantics-840390f/generate.sh → ...ession-wasm-semantics-75baf9b/generate.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,3 +33,8 @@ do
tests/proofs/"$spec"-spec.k \
--def-module KWASM-LEMMAS
done

kollect "test-wrc20" \
./kwasm prove --backend haskell \
tests/proofs/wrc20-spec.k \
--def-module WRC20-LEMMAS
4 changes: 2 additions & 2 deletions ...m-semantics-840390f/test-locals-spec.kore → ...m-semantics-75baf9b/test-locals-spec.kore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@ import KWASM-LEMMAS []


// claims
// 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),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),DotVar0)=>`<generatedTop>`(`<wasm>`(`<k>`(DotVar2),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),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/ttuegel/wasm-semantics/tests/proofs/locals-spec.k)) org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions) symbol()])]
// 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),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),DotVar0)=>`<generatedTop>`(`<wasm>`(`<k>`(DotVar2),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),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])]
claim{} \implies{SortGeneratedTopCell{}} (
\and{SortGeneratedTopCell{}} (
\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'4: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:SortLocalIdsCell{},Var'Unds'1:SortCurModIdxCell{},Var'Unds'2:SortLabelDepthCell{},Var'Unds'3:SortLabelIdsCell{}),Var'Unds'5:SortModuleRegistryCell{},Var'Unds'6:SortModuleIdsCell{},Var'Unds'7:SortModuleInstancesCell{},Var'Unds'8:SortNextModuleIdxCell{},Var'Unds'9:SortMainStoreCell{},Var'Unds'10:SortDeterministicMemoryGrowthCell{},Var'Unds'11:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{})), weakExistsFinally{SortGeneratedTopCell{}} (
\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'4: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:SortLocalIdsCell{},Var'Unds'1:SortCurModIdxCell{},Var'Unds'2:SortLabelDepthCell{},Var'Unds'3:SortLabelIdsCell{}),Var'Unds'5:SortModuleRegistryCell{},Var'Unds'6:SortModuleIdsCell{},Var'Unds'7:SortModuleInstancesCell{},Var'Unds'8:SortNextModuleIdxCell{},Var'Unds'9:SortMainStoreCell{},Var'Unds'10:SortDeterministicMemoryGrowthCell{},Var'Unds'11:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
\and{SortGeneratedTopCell{}} (
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar2:SortK{}),Var'Unds'4: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:SortLocalIdsCell{},Var'Unds'1:SortCurModIdxCell{},Var'Unds'2:SortLabelDepthCell{},Var'Unds'3:SortLabelIdsCell{}),Var'Unds'5:SortModuleRegistryCell{},Var'Unds'6:SortModuleIdsCell{},Var'Unds'7:SortModuleInstancesCell{},Var'Unds'8:SortNextModuleIdxCell{},Var'Unds'9:SortMainStoreCell{},Var'Unds'10:SortDeterministicMemoryGrowthCell{},Var'Unds'11:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{}))))
[org'Stop'kframework'Stop'attributes'Stop'Source{}(), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}()]
Expand Down
Loading