@@ -12,50 +12,64 @@ kollect() {
12
12
chmod +x " $name .sh"
13
13
}
14
14
15
+ build-evm () {
16
+ cd $KORE
17
+ git clone
[email protected] :kframework/evm-semantics.git
18
+ cd evm-semantics
19
+ git submodule update --init --recursive
20
+ make plugin-deps
21
+ make build-haskell
22
+ export PATH=$( pwd) /.build/usr/bin:$PATH
23
+ }
24
+
15
25
generate-evm () {
16
- # git clone [email protected] :kframework/evm-semantics.git
17
- # cd evm-semantics
18
- # local evm_commit=$(git rev-parse --short HEAD)
19
- # git submodule update --init --recursive
20
- # make plugin-deps
21
- # make build-haskell
22
- # export PATH=$(pwd)/.build/usr/bin:$PATH
23
- #
24
- # kollect test-pop1 env MODE=VMTESTS SCHEDULE=DEFAULT \
25
- # kevm run --backend haskell \
26
- # tests/ethereum-tests/VMTests/vmIOandFlowOperations/pop1.json
27
- #
28
- # kollect test-add0 env MODE=VMTESTS SCHEDULE=DEFAULT \
29
- # kevm run --backend haskell \
30
- # tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json \
31
- #
32
- # kollect test-sumTo10 env MODE=VMTESTS SCHEDULE=DEFAULT \
33
- # kevm run --backend haskell \
34
- # tests/interactive/sumTo10.evm \
35
- #
36
- # for search in \
37
- # branching-no-invalid straight-line-no-invalid \
38
- # branching-invalid straight-line
39
- # do
40
- # kollect "test-$search" \
41
- # kevm search --backend haskell \
42
- # "tests/interactive/search/$search.evm" \
43
- # "<statusCode> EVMC_INVALID_INSTRUCTION </statusCode>"
44
- # done
45
- #
46
- # kollect test-sum-to-n \
47
- # kevm prove --backend haskell \
48
- # tests/specs/examples/sum-to-n-spec.k \
49
- # VERIFICATION --format-failures
26
+ cd $KORE /evm-semantics
50
27
51
- cd evm-semantics
52
- testdir=$KORE /tests/regression-evm-*
53
- tests=test-*
54
- rm -r $testdir
55
- mkdir $KORE /tests/regression-evm-$evm_commit
56
- mv $tests $KORE /tests/regression-evm-$evm_commit
28
+ kollect test-pop1 env MODE=VMTESTS SCHEDULE=DEFAULT \
29
+ kevm run --backend haskell \
30
+ tests/ethereum-tests/VMTests/vmIOandFlowOperations/pop1.json
31
+
32
+ kollect test-add0 env MODE=VMTESTS SCHEDULE=DEFAULT \
33
+ kevm run --backend haskell \
34
+ tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json \
35
+
36
+ kollect test-sumTo10 env MODE=VMTESTS SCHEDULE=DEFAULT \
37
+ kevm run --backend haskell \
38
+ tests/interactive/sumTo10.evm \
39
+
40
+ for search in \
41
+ branching-no-invalid straight-line-no-invalid \
42
+ branching-invalid straight-line
43
+ do
44
+ kollect " test-$search " \
45
+ kevm search --backend haskell \
46
+ " tests/interactive/search/$search .evm" \
47
+ " <statusCode> EVMC_INVALID_INSTRUCTION </statusCode>"
48
+ done
49
+
50
+ kollect test-sum-to-n \
51
+ kevm prove --backend haskell \
52
+ tests/specs/examples/sum-to-n-spec.k \
53
+ VERIFICATION --format-failures
54
+ }
55
+
56
+ replace-tests () {
57
+ local testdir=$KORE /$1
58
+ local tests=$KORE /$2 /test-*
57
59
60
+ if [ -d $testdir ]
61
+ then
62
+ rm $testdir /test-*
63
+ else
64
+ mkdir $testdir
65
+ echo " include \$ (CURDIR)/../include.mk" > $testdir /Makefile
66
+ echo " " >> $testdir /Makefile
67
+ echo " test-%.sh.out: \$ (TEST_DIR)/test-%-*" >> $testdir /Makefile
68
+ fi
69
+ mv $tests $testdir
58
70
}
59
71
60
- cd $KORE
72
+ build-evm
61
73
generate-evm
74
+ replace-tests " test/regression-evm" " evm-semantics"
75
+ rm -rf $KORE /evm-semantics
0 commit comments