runtimeverification · rv-jenkins · Apr 27, 2021 · Apr 25, 2021 · Apr 25, 2021 · Apr 26, 2021
diff --git a/scripts/generate-regression-tests.sh b/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() {

diff --git a/scripts/trim-source-paths.sh b/scripts/trim-source-paths.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+sed \
+    -e 's|/home/jenkins-slave/workspace/[^/]\+/||' \
+    -i "$@"
diff --git a/test/regression-evm/test-add0-definition.kore b/test/regression-evm/test-add0-definition.kore
diff --git a/...egression-evm/test-add0-tmp.in.mEbuUJx6Wl → ...egression-evm/test-add0-tmp.in.LMCkBDlrJp b/...egression-evm/test-add0-tmp.in.mEbuUJx6Wl → ...egression-evm/test-add0-tmp.in.LMCkBDlrJp
diff --git a/test/regression-evm/test-add0.sh b/test/regression-evm/test-add0.sh
@@ -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 "$@"
diff --git a/test/regression-evm/test-branching-invalid-definition.kore b/test/regression-evm/test-branching-invalid-definition.kore
diff --git a/.../test-branching-invalid-tmp.in.7cf3srjbcr → .../test-branching-invalid-tmp.in.csPcFSpe3Y b/.../test-branching-invalid-tmp.in.7cf3srjbcr → .../test-branching-invalid-tmp.in.csPcFSpe3Y
diff --git a/...-branching-invalid-tmp.pattern.tZ7kesqBaw → ...-branching-invalid-tmp.pattern.d7Pd5DxkTJ b/...-branching-invalid-tmp.pattern.tZ7kesqBaw → ...-branching-invalid-tmp.pattern.d7Pd5DxkTJ
diff --git a/test/regression-evm/test-branching-invalid.sh b/test/regression-evm/test-branching-invalid.sh
@@ -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 "$@"
diff --git a/test/regression-evm/test-branching-no-invalid-definition.kore b/test/regression-evm/test-branching-no-invalid-definition.kore
diff --git a/...st-branching-no-invalid-tmp.in.rscfMYRvLY → ...st-branching-no-invalid-tmp.in.0Lwj7yUEcE b/...st-branching-no-invalid-tmp.in.rscfMYRvLY → ...st-branching-no-invalid-tmp.in.0Lwj7yUEcE
diff --git a/...anching-no-invalid-tmp.pattern.azNpCuI5ge → ...anching-no-invalid-tmp.pattern.7h1bFPaVKX b/...anching-no-invalid-tmp.pattern.azNpCuI5ge → ...anching-no-invalid-tmp.pattern.7h1bFPaVKX
diff --git a/test/regression-evm/test-branching-no-invalid.sh b/test/regression-evm/test-branching-no-invalid.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 "$@"
diff --git a/test/regression-evm/test-pop1-definition.kore b/test/regression-evm/test-pop1-definition.kore
diff --git a/...egression-evm/test-pop1-tmp.in.64t9hI9HTU → ...egression-evm/test-pop1-tmp.in.82CcCt7RpI b/...egression-evm/test-pop1-tmp.in.64t9hI9HTU → ...egression-evm/test-pop1-tmp.in.82CcCt7RpI
diff --git a/test/regression-evm/test-pop1.sh b/test/regression-evm/test-pop1.sh
@@ -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 "$@"
diff --git a/test/regression-evm/test-straight-line-definition.kore b/test/regression-evm/test-straight-line-definition.kore
diff --git a/test/regression-evm/test-straight-line-no-invalid-definition.kore b/test/regression-evm/test-straight-line-no-invalid-definition.kore
diff --git a/...traight-line-no-invalid-tmp.in.0QLRBXd1H7 → ...traight-line-no-invalid-tmp.in.fMMcAVsZIL b/...traight-line-no-invalid-tmp.in.0QLRBXd1H7 → ...traight-line-no-invalid-tmp.in.fMMcAVsZIL
diff --git a/...ht-line-no-invalid-tmp.pattern.gvb2BmhKwH → ...ht-line-no-invalid-tmp.pattern.oG8PSrQ3PZ b/...ht-line-no-invalid-tmp.pattern.gvb2BmhKwH → ...ht-line-no-invalid-tmp.pattern.oG8PSrQ3PZ
diff --git a/test/regression-evm/test-straight-line-no-invalid.sh b/test/regression-evm/test-straight-line-no-invalid.sh
@@ -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 "$@"
diff --git a/...-evm/test-straight-line-tmp.in.qseSpMCXAo → ...-evm/test-straight-line-tmp.in.LpmaOUXGKb b/...-evm/test-straight-line-tmp.in.qseSpMCXAo → ...-evm/test-straight-line-tmp.in.LpmaOUXGKb
diff --git a/...test-straight-line-tmp.pattern.36aSqKKp5l → ...test-straight-line-tmp.pattern.9bfWMqxBgf b/...test-straight-line-tmp.pattern.36aSqKKp5l → ...test-straight-line-tmp.pattern.9bfWMqxBgf
diff --git a/test/regression-evm/test-straight-line.sh b/test/regression-evm/test-straight-line.sh
@@ -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 "$@"
diff --git a/test/regression-evm/test-sum-to-n-spec.kore b/test/regression-evm/test-sum-to-n-spec.kore
diff --git a/test/regression-evm/test-sum-to-n-vdefinition.kore b/test/regression-evm/test-sum-to-n-vdefinition.kore
diff --git a/test/regression-evm/test-sumTo10-definition.kore b/test/regression-evm/test-sumTo10-definition.kore
diff --git a/...ession-evm/test-sumTo10-tmp.in.fMaXmswtJJ → ...ession-evm/test-sumTo10-tmp.in.Bwb5KNkyjP b/...ession-evm/test-sumTo10-tmp.in.fMaXmswtJJ → ...ession-evm/test-sumTo10-tmp.in.Bwb5KNkyjP
diff --git a/test/regression-evm/test-sumTo10.sh b/test/regression-evm/test-sumTo10.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 "$@"
diff --git a/test/regression-wasm/test-locals-spec.kore b/test/regression-wasm/test-locals-spec.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)")]