Skip to content

Commit c6e80d0

Browse files
geo2ageo2a
committed
Add test-syntactic-simplification
Run test-syntactic-simplification Fix test
1 parent a5e16da commit c6e80d0

File tree

8 files changed

+3491
-0
lines changed

8 files changed

+3491
-0
lines changed

‎booster/test/rpc-integration/resources/syntactic-simplification.haskell.kore

Lines changed: 3017 additions & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/resources/syntactic-simplification.k

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
module SYNTACTIC-SIMPLIFICATION
2+
imports INT
3+
imports BOOL
4+
5+
syntax State ::= test1Init()
6+
| test1State1()
7+
| test1State2()
8+
9+
configuration <k> $PGM:State ~> .K </k>
10+
<int-x> 0:Int </int-x>
11+
<int-y> 0:Int </int-y>
12+
13+
////////////////////////////////////////////////////////////////////////////////
14+
//
15+
////////////////////////////////////////////////////////////////////////////////
16+
rule [test1-init]: <k> test1Init() => test1State1() ... </k>
17+
<int-x> _ => ?X </int-x>
18+
<int-y> _ => ?Y </int-y>
19+
ensures ?X <Int 100
20+
andBool ?Y <Int 50
21+
andBool ?X <Int ?Y
22+
23+
rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
24+
<int-x> X </int-x>
25+
requires X <Int 50
26+
27+
rule [test1-simplify]:
28+
X <Int Y => true
29+
requires X <Int Z
30+
andBool Z <Int Y
31+
// [simplification, syntactic(1)]
32+
[simplification]
33+
34+
// to produce input state:
35+
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
36+
// then edit state-test1Init.json to substitute test1State1() for test1Init()
37+
38+
endmodule

‎booster/test/rpc-integration/resources/syntactic-simplification.kompile

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
set -eux
2+
3+
SCRIPT_DIR=$(dirname $0)
4+
PLUGIN_DIR=${PLUGIN_DIR:-""}
5+
6+
if [ -z "$PLUGIN_DIR" ]; then
7+
echo "PLUGIN_DIR required to link in a crypto plugin dependency"
8+
exit 1
9+
else
10+
for lib in libff libcryptopp blake2; do
11+
LIBFILE=$(find ${PLUGIN_DIR} -name "${lib}.a" | head -1)
12+
[ -z "$LIBFILE" ] && (echo "[Error] Unable to locate ${lib}.a"; exit 1)
13+
PLUGIN_LIBS+="$LIBFILE "
14+
PLUGIN_INCLUDE+="-I$(dirname $LIBFILE) -I$(dirname $LIBFILE)/../include "
15+
done
16+
#PLUGIN_CPP=$(find ${PLUGIN_DIR}/plugin-c -name "*.cpp")
17+
PLUGIN_CPP="${PLUGIN_DIR}/include/plugin-c/crypto.cpp ${PLUGIN_DIR}/include/plugin-c/plugin_util.cpp"
18+
fi
19+
20+
NAME=$(basename ${0%.kompile})
21+
NAMETGZ=$(basename ${0%.kompile})
22+
23+
24+
# provide haskell definition
25+
cp ${NAME}.haskell.kore ${NAME}.kore
26+
27+
# Regenerate llvm backend decision tree
28+
mkdir -p ./dt
29+
llvm-kompile-matching ${NAME}.llvm.kore qbaL ./dt 0
30+
31+
# kompile llvm-definition to interpreter
32+
33+
case "$OSTYPE" in
34+
linux*) LPROCPS="-lprocps" ;;
35+
*) LPROCPS="" ;;
36+
esac
37+
38+
llvm-kompile ${NAME}.llvm.kore ./dt c -- \
39+
-fPIC -std=c++17 -o interpreter \
40+
$PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
41+
-lcrypto -lssl -lsecp256k1 $LPROCPS
42+
mv interpreter.* ${NAME}.dylib
43+
44+
# remove temporary artefacts
45+
rm -r dt

‎booster/test/rpc-integration/resources/syntactic-simplification.llvm.kore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
3934-smt.llvm.kore

‎booster/test/rpc-integration/test-syntactic-simplification/README.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# Test application of syntactic simplification rules
2+
3+
See `../resourses/syntactic-simplification.k`.
4+
5+
We have to keep `../resourses/syntactic-simplification.haskell.kore`, the K front-end does not yet support the `syntactic` attribute. The Kore encoding of the simplification rule `test1-simplify` is manually modified to contain the attribute `syntactic{}("1")`. `../resourses/syntactic-simplification.haskell.kore` should be removed from Git once the compiler supports this feature.
6+
7+
We also need an LLVM definition, and we are re-using ``../resourses/3934-smt.llvm.kore` as it is checked-in, but any definition with `INT` and `BOOL` would work.

‎booster/test/rpc-integration/test-syntactic-simplification/response-test1Init.json

Lines changed: 268 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,268 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "stuck",
6+
"depth": 2,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "App",
13+
"name": "Lbl'-LT-'generatedTop'-GT-'",
14+
"sorts": [],
15+
"args": [
16+
{
17+
"tag": "App",
18+
"name": "Lbl'-LT-'k'-GT-'",
19+
"sorts": [],
20+
"args": [
21+
{
22+
"tag": "App",
23+
"name": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "inj",
29+
"sorts": [
30+
{
31+
"tag": "SortApp",
32+
"name": "SortState",
33+
"args": []
34+
},
35+
{
36+
"tag": "SortApp",
37+
"name": "SortKItem",
38+
"args": []
39+
}
40+
],
41+
"args": [
42+
{
43+
"tag": "App",
44+
"name": "Lbltest1State2'LParRParUnds'SYNTACTIC-SIMPLIFICATION'Unds'State",
45+
"sorts": [],
46+
"args": []
47+
}
48+
]
49+
},
50+
{
51+
"tag": "App",
52+
"name": "dotk",
53+
"sorts": [],
54+
"args": []
55+
}
56+
]
57+
}
58+
]
59+
},
60+
{
61+
"tag": "App",
62+
"name": "Lbl'-LT-'int-x'-GT-'",
63+
"sorts": [],
64+
"args": [
65+
{
66+
"tag": "EVar",
67+
"name": "Var'Ques'X0",
68+
"sort": {
69+
"tag": "SortApp",
70+
"name": "SortInt",
71+
"args": []
72+
}
73+
}
74+
]
75+
},
76+
{
77+
"tag": "App",
78+
"name": "Lbl'-LT-'int-y'-GT-'",
79+
"sorts": [],
80+
"args": [
81+
{
82+
"tag": "EVar",
83+
"name": "Var'Ques'Y0",
84+
"sort": {
85+
"tag": "SortApp",
86+
"name": "SortInt",
87+
"args": []
88+
}
89+
}
90+
]
91+
},
92+
{
93+
"tag": "App",
94+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
95+
"sorts": [],
96+
"args": [
97+
{
98+
"tag": "DV",
99+
"sort": {
100+
"tag": "SortApp",
101+
"name": "SortInt",
102+
"args": []
103+
},
104+
"value": "0"
105+
}
106+
]
107+
}
108+
]
109+
}
110+
},
111+
"predicate": {
112+
"format": "KORE",
113+
"version": 1,
114+
"term": {
115+
"tag": "And",
116+
"sort": {
117+
"tag": "SortApp",
118+
"name": "SortGeneratedTopCell",
119+
"args": []
120+
},
121+
"patterns": [
122+
{
123+
"tag": "Equals",
124+
"argSort": {
125+
"tag": "SortApp",
126+
"name": "SortBool",
127+
"args": []
128+
},
129+
"sort": {
130+
"tag": "SortApp",
131+
"name": "SortGeneratedTopCell",
132+
"args": []
133+
},
134+
"first": {
135+
"tag": "DV",
136+
"sort": {
137+
"tag": "SortApp",
138+
"name": "SortBool",
139+
"args": []
140+
},
141+
"value": "true"
142+
},
143+
"second": {
144+
"tag": "App",
145+
"name": "Lbl'Unds-LT-'Int'Unds'",
146+
"sorts": [],
147+
"args": [
148+
{
149+
"tag": "EVar",
150+
"name": "Var'Ques'X0",
151+
"sort": {
152+
"tag": "SortApp",
153+
"name": "SortInt",
154+
"args": []
155+
}
156+
},
157+
{
158+
"tag": "DV",
159+
"sort": {
160+
"tag": "SortApp",
161+
"name": "SortInt",
162+
"args": []
163+
},
164+
"value": "100"
165+
}
166+
]
167+
}
168+
},
169+
{
170+
"tag": "Equals",
171+
"argSort": {
172+
"tag": "SortApp",
173+
"name": "SortBool",
174+
"args": []
175+
},
176+
"sort": {
177+
"tag": "SortApp",
178+
"name": "SortGeneratedTopCell",
179+
"args": []
180+
},
181+
"first": {
182+
"tag": "DV",
183+
"sort": {
184+
"tag": "SortApp",
185+
"name": "SortBool",
186+
"args": []
187+
},
188+
"value": "true"
189+
},
190+
"second": {
191+
"tag": "App",
192+
"name": "Lbl'Unds-LT-'Int'Unds'",
193+
"sorts": [],
194+
"args": [
195+
{
196+
"tag": "EVar",
197+
"name": "Var'Ques'X0",
198+
"sort": {
199+
"tag": "SortApp",
200+
"name": "SortInt",
201+
"args": []
202+
}
203+
},
204+
{
205+
"tag": "EVar",
206+
"name": "Var'Ques'Y0",
207+
"sort": {
208+
"tag": "SortApp",
209+
"name": "SortInt",
210+
"args": []
211+
}
212+
}
213+
]
214+
}
215+
},
216+
{
217+
"tag": "Equals",
218+
"argSort": {
219+
"tag": "SortApp",
220+
"name": "SortBool",
221+
"args": []
222+
},
223+
"sort": {
224+
"tag": "SortApp",
225+
"name": "SortGeneratedTopCell",
226+
"args": []
227+
},
228+
"first": {
229+
"tag": "DV",
230+
"sort": {
231+
"tag": "SortApp",
232+
"name": "SortBool",
233+
"args": []
234+
},
235+
"value": "true"
236+
},
237+
"second": {
238+
"tag": "App",
239+
"name": "Lbl'Unds-LT-'Int'Unds'",
240+
"sorts": [],
241+
"args": [
242+
{
243+
"tag": "EVar",
244+
"name": "Var'Ques'Y0",
245+
"sort": {
246+
"tag": "SortApp",
247+
"name": "SortInt",
248+
"args": []
249+
}
250+
},
251+
{
252+
"tag": "DV",
253+
"sort": {
254+
"tag": "SortApp",
255+
"name": "SortInt",
256+
"args": []
257+
},
258+
"value": "50"
259+
}
260+
]
261+
}
262+
}
263+
]
264+
}
265+
}
266+
}
267+
}
268+
}

0 commit comments

Comments
 (0)