Skip to content

Commit 7ea55fa

Browse files
ttuegelMirceaSemarzion
authored
Regenerate kevm and kwasm regression tests
* kollect.sh: Avoid unbound variable error * kollect.sh: Fix typo in variable name * rewrote kollect.sh file and regenerated wasm kore files * modifying command for test-wrc20 * updating wasm kore files * trigger build * regenerated evm files and fixed the generate script * added some additional needed kore files * regenerated evm golden files * fixed issue with wasm regression test * Removed comment Co-authored-by: MirceaS <[email protected]> Co-authored-by: emarzion <[email protected]>
1 parent 3975056 commit 7ea55fa

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+423829
-178391
lines changed

scripts/kollect.sh

Lines changed: 10 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -5,26 +5,21 @@
55

66
# Usage:
77
#
8-
# krun ... --debug --dry-run | xargs kollect.sh NAME
8+
# krun ... --save-temps --dry-run | xargs kollect.sh NAME
99
#
1010
# or
1111
#
12-
# kprove ... --debug --dry-run | xargs kollect.sh NAME
12+
# kprove ... --save-temps --dry-run | xargs kollect.sh NAME
1313
#
1414
# Output:
1515
# on standard output:
1616
# A command to run `kore-exec` equivalent to the `krun` or `kprove` command.
1717
# The `kore-exec` command is replaced by `$KORE_EXEC`, so that variable must
1818
# be set at runtime.
19-
# file NAME-definition.kore: `krun` only
20-
# file NAME-pgm.kore: `krun` only
21-
# file NAME-pattern.kore: `krun --search` only
22-
# file NAME-spec.kore: `kprove` only
23-
# file NAME-vdefinition.kore: `kprove` only
2419

2520
set -euo pipefail
2621

27-
kollect=
22+
kollected=
2823
name=${1:?}
2924
shift
3025

@@ -34,41 +29,18 @@ do
3429
*kore-exec)
3530
echo -n '$KORE_EXEC '
3631
;;
32+
--output)
33+
shift
34+
;;
3735
*/definition.kore)
3836
cp "$1" "$name-definition.kore"
3937
echo -n "$name-definition.kore "
4038
;;
41-
--output)
42-
;;
43-
*/result.kore)
44-
dir="$(dirname "$1")"
45-
if [[ -f "$dir/spec.kore" ]]
46-
then
47-
mv "$dir/spec.kore" "$name-spec.kore"
48-
mv "$dir/vdefinition.kore" "$name-vdefinition.kore"
49-
elif [[ -f "$dir/pgm.kore" ]]
50-
then
51-
mv "$dir/pgm.kore" "$name-pgm.kore"
52-
! [[ -f "$dir/pattern.kore" ]] || mv "$dir/pattern.kore" "$name-pattern.kore"
53-
else
54-
echo >&2 "$dir does not contain spec.kore or pgm.kore!"
55-
exit 1
56-
fi
57-
rmdir "$dir"
39+
*.kore)
40+
cp "$1" "$name-$(basename "$1")"
41+
echo -n "$name-$(basename "$1") "
5842
kollected=1
5943
;;
60-
*/pgm.kore)
61-
echo -n "$name-pgm.kore "
62-
;;
63-
*/spec.kore)
64-
echo -n "$name-spec.kore "
65-
;;
66-
*/vdefinition.kore)
67-
echo -n "$name-vdefinition.kore "
68-
;;
69-
*/pattern.kore)
70-
echo -n "$name-pattern.kore "
71-
;;
7244
*)
7345
echo -n "$1 "
7446
esac
@@ -77,7 +49,7 @@ done
7749

7850
echo '"$@"'
7951

80-
if [[ -z "$kollected" ]]
52+
if [[ -z "${kollected:-}" ]]
8153
then
8254
echo >&2 "Did not collect any Kore files!"
8355
exit 1

test/regression-evm-semantics-39dd1e5/generate.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ kollect() {
1515
local name="$1"
1616
shift
1717
echo '#!/bin/sh' > "$name.sh"
18+
# TODO Mircea: change debug to save-temps after the evm-semantics repo is updated to use the latest backend
1819
"$@" --debug --dry-run | xargs $KORE/scripts/kollect.sh "$name" >> "$name.sh"
1920
chmod +x "$name.sh"
2021
}
@@ -46,4 +47,4 @@ done
4647
kollect test-sum-to-n \
4748
./kevm prove --backend haskell \
4849
tests/specs/examples/sum-to-n-spec.k \
49-
--format-failures --def-module VERIFICATION
50+
VERIFICATION --format-failures

0 commit comments

Comments
 (0)