-
Notifications
You must be signed in to change notification settings - Fork 0
/
.gitlab-ci.yml
71 lines (68 loc) · 3.38 KB
/
.gitlab-ci.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
variables:
GIT_SUBMODULE_STRATEGY: recursive
stages:
- build
- release
build:
stage: build
image: $CI_REGISTRY/psyco/gdart/development:22.2.0
script:
- git rev-parse --short HEAD > version.txt
- git submodule update --init --recursive
- pip3 install pyyaml
- ./compile-all.sh
- ./run-gwit.sh --witness examples/witnesses/spec1-5_product56.yml/witness.GraphML examples/benchmarks/spec1-5_product56.prp examples/benchmarks/spec1-5_product56/
- ./run-gwit.sh --witness examples/witnesses/assert2.yml/witness.GraphML examples/benchmarks/assert2.prp examples/benchmarks/assert2/
- ./run-gwit.sh --witness examples/witnesses/Ackermann01.yml/witness.GraphML examples/benchmarks/Ackermann01.prp examples/benchmarks/Ackermann01/
- mkdir -p val_gwit/dse/target
- mv version.txt val_gwit
- mv run-gwit.sh val_gwit
- mv weave-witness.py val_gwit
- mv executor.sh val_gwit
- mv README.md val_gwit
- mv LICENSE val_gwit
- mv dse/README.md val_gwit/dse/
- mv dse/LICENSE val_gwit/dse/LICENSE
- mkdir -p val_gwit/SPouT
- mv SPouT/README.md val_gwit/SPouT/
- mv SPouT/LICENSE val_gwit/SPouT/
- mkdir -p val_gwit/SPouT/sdk/mxbuild/linux-amd64/GRAALVM_ESPRESSO_NATIVE_CE_JAVA17/graalvm-espresso-native-ce-java17-22.2.0.1-dev/
- mv SPouT/sdk/mxbuild/linux-amd64/GRAALVM_ESPRESSO_NATIVE_CE_JAVA17/graalvm-espresso-native-ce-java17-22.2.0.1-dev/* val_gwit/SPouT/sdk/mxbuild/linux-amd64/GRAALVM_ESPRESSO_NATIVE_CE_JAVA17/graalvm-espresso-native-ce-java17-22.2.0.1-dev/
- mkdir -p val_gwit/verifier-stub/target
- mv verifier-stub/README.md val_gwit/verifier-stub/
- mv verifier-stub/LICENSE val_gwit/verifier-stub/
- mv ./dse/target/dse-0.0.1-SNAPSHOT-jar-with-dependencies.jar val_gwit/dse/target/dse-0.0.1-SNAPSHOT-jar-with-dependencies.jar
- mv ./verifier-stub/target/verifier-stub-1.0.jar val_gwit/verifier-stub/target/verifier-stub-1.0.jar
artifacts:
name: "val_gwit"
paths:
- val_gwit
witness-check-short:
stage: release
image: $CI_REGISTRY/sv-comp/sv-comp-base-images/vcloud-ready-witness:latest
script:
- export BENCHMARK_BASE=$(realpath --relative-to="${PWD}" /data/gdart-witnesses)
- echo "Benchmarks relative $BENCHMARK_BASE $PWD"
- >
echo '<?xml version="1.0"?>
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
<benchmark tool="gwit-tudo" timelimit="5 min" memlimit="4 GB" cpuCores="3">
<resultfiles>**.graphml</resultfiles>
<rundefinition name="sv-comp20_prop-reachsafety_java">
<tasks name="ReachSafety-Java">
<includesfile>'"${BENCHMARK_BASE}"'/witness.set</includesfile>
<propertyfile>'"${BENCHMARK_BASE}"'/java/properties/assert_java.prp</propertyfile>
</tasks>
</rundefinition>
</benchmark>' > val_gwit.xml
- cat val_gwit.xml
- /data/benchexec/contrib/vcloud-benchmark.py --vcloudMaster $VCLOUD_MASTER --vcloudClientHeap 1560 --vcloudAdditionalFiles ./val_gwit /data/sv-benchmarks/java/* /data/gdart-witnesses/* --vcloudJar /srv/vcloud/lib/vcloud.jar --no-container --tool-directory ./val_gwit val_gwit.xml | tee vcloud.run
- $(cat vcloud.run | grep table-generator)
artifacts:
paths:
- results
dependencies:
- build
rules:
- if: $CI_PIPELINE_SOURCE != "schedule"
when: on_success