Update regression tests (#2575)

* Update regression tests

* Update regression tests

* Update regression tests

* Trim variable parts of source path attributes

Co-authored-by: Thomas Tuegel <[email protected]>

Author: rv-jenkins

scripts/generate-regression-tests.sh

@@ -36,17 +36,17 @@ generate-evm() {
         kevm run --backend haskell \
             --mode VMTESTS --schedule DEFAULT \
             tests/ethereum-tests/VMTests/vmIOandFlowOperations/pop1.json
-    
+
     kollect test-add0 env \
         kevm run --backend haskell \
             --mode VMTESTS --schedule DEFAULT \
             tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json \
-    
+
     kollect test-sumTo10 \
         kevm run --backend haskell \
             --mode VMTESTS --schedule DEFAULT \
             tests/interactive/sumTo10.evm \
-    
+
     for search in \
         branching-no-invalid straight-line-no-invalid \
         branching-invalid straight-line
@@ -56,11 +56,13 @@ generate-evm() {
                 "tests/interactive/search/$search.evm" \
                 "<statusCode> EVMC_INVALID_INSTRUCTION </statusCode>"
     done
-            
+
     kollect test-sum-to-n \
         kevm prove --backend haskell \
             tests/specs/examples/sum-to-n-spec.k \
             VERIFICATION --format-failures
+
+    $KORE/scripts/trim-source-paths.sh *.kore
 }
 
 generate-wasm() {
@@ -76,16 +78,18 @@ generate-wasm() {
                 tests/proofs/"$spec"-spec.k \
                 KWASM-LEMMAS
     done
-    
+
     kollect "test-memory" \
         ./kwasm prove --backend haskell \
             tests/proofs/memory-spec.k \
             KWASM-LEMMAS \
             --concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive
-    
+
     kollect "test-wrc20" \
         ./kwasm prove --backend haskell tests/proofs/wrc20-spec.k WRC20-LEMMAS --format-failures \
         --concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive,WASM-DATA.get-Existing,WASM-DATA.set-Extend
+
+    $KORE/scripts/trim-source-paths.sh *.kore
 }
 
 replace-tests() {

scripts/trim-source-paths.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+sed \
+    -e 's|/home/jenkins-slave/workspace/[^/]\+/||' \
+    -i "$@"

test/regression-evm/test-add0-definition.kore

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-add0-definition.kore --module ETHEREUM-SIMULATION --pattern test-add0-tmp.in.mEbuUJx6Wl "$@"
+${KORE_EXEC:?} test-add0-definition.kore --module ETHEREUM-SIMULATION --pattern test-add0-tmp.in.LMCkBDlrJp "$@"

test/regression-evm/test-add0-tmp.in.mEbuUJx6Wl renamed to test/regression-evm/test-add0-tmp.in.LMCkBDlrJp

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-branching-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-branching-invalid-tmp.in.7cf3srjbcr --searchType FINAL --search test-branching-invalid-tmp.pattern.tZ7kesqBaw "$@"
+${KORE_EXEC:?} test-branching-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-branching-invalid-tmp.in.csPcFSpe3Y --searchType FINAL --search test-branching-invalid-tmp.pattern.d7Pd5DxkTJ "$@"

test/regression-evm/test-add0.sh

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-branching-no-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-branching-no-invalid-tmp.in.rscfMYRvLY --searchType FINAL --search test-branching-no-invalid-tmp.pattern.azNpCuI5ge "$@"
+${KORE_EXEC:?} test-branching-no-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-branching-no-invalid-tmp.in.0Lwj7yUEcE --searchType FINAL --search test-branching-no-invalid-tmp.pattern.7h1bFPaVKX "$@"

test/regression-evm/test-branching-invalid-definition.kore

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-pop1-definition.kore --module ETHEREUM-SIMULATION --pattern test-pop1-tmp.in.64t9hI9HTU "$@"
+${KORE_EXEC:?} test-pop1-definition.kore --module ETHEREUM-SIMULATION --pattern test-pop1-tmp.in.82CcCt7RpI "$@"

test/regression-evm/test-branching-invalid-tmp.in.7cf3srjbcr renamed to test/regression-evm/test-branching-invalid-tmp.in.csPcFSpe3Y

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-straight-line-no-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-straight-line-no-invalid-tmp.in.0QLRBXd1H7 --searchType FINAL --search test-straight-line-no-invalid-tmp.pattern.gvb2BmhKwH "$@"
+${KORE_EXEC:?} test-straight-line-no-invalid-definition.kore --module ETHEREUM-SIMULATION --pattern test-straight-line-no-invalid-tmp.in.fMMcAVsZIL --searchType FINAL --search test-straight-line-no-invalid-tmp.pattern.oG8PSrQ3PZ "$@"

test/regression-evm/test-branching-invalid-tmp.pattern.tZ7kesqBaw renamed to test/regression-evm/test-branching-invalid-tmp.pattern.d7Pd5DxkTJ

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-straight-line-definition.kore --module ETHEREUM-SIMULATION --pattern test-straight-line-tmp.in.qseSpMCXAo --searchType FINAL --search test-straight-line-tmp.pattern.36aSqKKp5l "$@"
+${KORE_EXEC:?} test-straight-line-definition.kore --module ETHEREUM-SIMULATION --pattern test-straight-line-tmp.in.LpmaOUXGKb --searchType FINAL --search test-straight-line-tmp.pattern.9bfWMqxBgf "$@"

test/regression-evm/test-branching-invalid.sh

@@ -1,2 +1,2 @@
 #!/bin/sh
-${KORE_EXEC:?} test-sumTo10-definition.kore --module ETHEREUM-SIMULATION --pattern test-sumTo10-tmp.in.fMaXmswtJJ "$@"
+${KORE_EXEC:?} test-sumTo10-definition.kore --module ETHEREUM-SIMULATION --pattern test-sumTo10-tmp.in.Bwb5KNkyjP "$@"

test/regression-evm/test-branching-no-invalid-definition.kore

@@ -1,17 +1,17 @@
-[]
+[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/././tests/proofs/locals-spec.k)")]
 module LOCALS-SPEC
 
 // imports
 import KWASM-LEMMAS []
 
 
 // claims
-// 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(/home/jenkins-slave/workspace/haskell-backend_PR-2548/wasm-semantics/././tests/proofs/locals-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
+// 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(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-'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{}} (
       \and{SortGeneratedTopCell{}} (
       \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{}))))
-  [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jenkins-slave/workspace/haskell-backend_PR-2548/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)")]
+  [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(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)")]
 
-endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3,1,10,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jenkins-slave/workspace/haskell-backend_PR-2548/wasm-semantics/././tests/proofs/locals-spec.k)")]
+endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3,1,10,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/././tests/proofs/locals-spec.k)")]