Skip to content

Commit fe2f681

Browse files
author
Dwight Guth
committed
Revert "Revert "use ml constructs in k and encode them into kore (runtimeverification#336)""
This reverts commit 2f07aba.
1 parent 2f07aba commit fe2f681

21 files changed

Lines changed: 398 additions & 104 deletions

File tree

‎k-distribution/include/builtin/domains.k‎

Lines changed: 28 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -343,11 +343,9 @@ module INT-SYNTAX
343343
syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)]
344344
endmodule
345345

346-
module INT
346+
module INT-COMMON
347347
imports INT-SYNTAX
348348
imports BOOL
349-
imports K-EQUAL
350-
351349
syntax Int ::= "~Int" Int [function, functional, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not)]
352350
> left:
353351
Int "^Int" Int [function, left, smtlib(^), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)]
@@ -373,6 +371,7 @@ module INT
373371
Int "xorInt" Int [function, functional, left, latex({#1}\mathrel{\oplus_{\scriptstyle\it Int}}{#2}), hook(INT.xor)]
374372
> left:
375373
Int "|Int" Int [function, functional, left, latex({#1}\mathrel{|_{\scriptstyle\it Int}}{#2}), hook(INT.or)]
374+
376375
syntax Int ::= "minInt" "(" Int "," Int ")" [function, functional, smtlib(int_min), hook(INT.min)]
377376
| "maxInt" "(" Int "," Int ")" [function, functional, smtlib(int_max), hook(INT.max)]
378377
| absInt ( Int ) [function, functional, smtlib(int_abs), hook(INT.abs)]
@@ -381,6 +380,32 @@ module INT
381380
syntax Int ::= bitRangeInt ( Int, indexInt: Int, lengthInt: Int ) [function, hook(INT.bitRange)]
382381
syntax Int ::= signExtendBitRangeInt ( Int, indexInt: Int, lengthInt: Int ) [function, hook(INT.signExtendBitRange)]
383382

383+
syntax Bool ::= Int "<=Int" Int [function, functional, left, smtlib(<=), latex({#1}\mathrel{\leq_{\scriptstyle\it Int}}{#2}), hook(INT.le)]
384+
| Int "<Int" Int [function, functional, left, smtlib(<), latex({#1}\mathrel{<_{\scriptstyle\it Int}}{#2}), hook(INT.lt)]
385+
| Int ">=Int" Int [function, functional, left, smtlib(>=), latex({#1}\mathrel{\geq_{\scriptstyle\it Int}}{#2}), hook(INT.ge)]
386+
| Int ">Int" Int [function, functional, left, smtlib(>), latex({#1}\mathrel{>_{\scriptstyle\it Int}}{#2}), hook(INT.gt)]
387+
| Int "==Int" Int [function, functional, left, smtlib(=), latex({#1}\mathrel{{=}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.eq), klabel(_==Int_)]
388+
| Int "=/=Int" Int [function, functional, left, smtlib(distinct), latex({#1}\mathrel{{=}{/}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.ne)]
389+
| Int "dividesInt" Int [function]
390+
endmodule
391+
392+
module INT-SYMBOLIC [symbolic, kore]
393+
imports INT-COMMON
394+
imports ML-SYNTAX
395+
396+
/**
397+
* Definability conditions for _/Int_ and _%Int_
398+
*/
399+
400+
rule #Ceil(I1:Int /Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]
401+
rule #Ceil(I1:Int %Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]
402+
endmodule
403+
404+
module INT
405+
imports INT-COMMON
406+
imports INT-SYMBOLIC
407+
imports K-EQUAL
408+
384409
rule bitRangeInt(I::Int, IDX::Int, LEN::Int) => (I >>Int IDX) modInt (1 <<Int LEN)
385410

386411
rule signExtendBitRangeInt(I::Int, IDX::Int, LEN::Int) => (bitRangeInt(I, IDX, LEN) +Int (1 <<Int (LEN -Int 1))) modInt (1 <<Int LEN) -Int (1 <<Int (LEN -Int 1))
@@ -396,14 +421,6 @@ module INT
396421
rule minInt(I1:Int, I2:Int) => I1 requires I1 <=Int I2
397422
rule minInt(I1:Int, I2:Int) => I2 requires I1 >=Int I2
398423

399-
syntax Bool ::= Int "<=Int" Int [function, functional, left, smtlib(<=), latex({#1}\mathrel{\leq_{\scriptstyle\it Int}}{#2}), hook(INT.le)]
400-
| Int "<Int" Int [function, functional, left, smtlib(<), latex({#1}\mathrel{<_{\scriptstyle\it Int}}{#2}), hook(INT.lt)]
401-
| Int ">=Int" Int [function, functional, left, smtlib(>=), latex({#1}\mathrel{\geq_{\scriptstyle\it Int}}{#2}), hook(INT.ge)]
402-
| Int ">Int" Int [function, functional, left, smtlib(>), latex({#1}\mathrel{>_{\scriptstyle\it Int}}{#2}), hook(INT.gt)]
403-
| Int "==Int" Int [function, functional, left, smtlib(=), latex({#1}\mathrel{{=}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.eq), klabel(_==Int_)]
404-
| Int "=/=Int" Int [function, functional, left, smtlib(distinct), latex({#1}\mathrel{{=}{/}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.ne)]
405-
| Int "dividesInt" Int [function]
406-
407424
rule I1:Int ==Int I2:Int => I1 ==K I2
408425
rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)
409426
rule (I1:Int dividesInt I2:Int) => (I2 %Int I1) ==Int 0

‎k-distribution/include/builtin/kast.k‎

Lines changed: 20 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -63,30 +63,35 @@ module KSEQ
6363
endmodule
6464
6565
66+
module ML-SYNTAX
67+
imports BASIC-K
68+
69+
syntax #KVariable
70+
71+
syntax K ::= "#True" [klabel(#True), symbol, poly(0)]
72+
| "#False" [klabel(#False), symbol, poly(0)]
73+
| "#Not" "(" K ")" [klabel(#Not), symbol, mlOp, poly(0, 1)]
74+
| "#Ceil" "(" K ")" [klabel(#Ceil), symbol, mlOp, poly(1; 0)]
75+
| "#Floor" "(" K ")" [klabel(#Floor), symbol, mlOp, poly(1; 0)]
76+
> "{" K "#Equals" K "}" [klabel(#Equals), symbol, mlOp, format(%1%i%n%2%d%n%3%i%n%4%d%n%5), poly(1, 2; 0)]
77+
> K "#And" K [klabel(#And), symbol, assoc, left, comm, unit(#True), mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
78+
> K "#Or" K [klabel(#Or), symbol, assoc, left, comm, unit(#False), mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
79+
> K "#Implies" K [klabel(#Implies), symbol, mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
80+
> "#Exists" #KVariable "." K [klabel(#Exists), symbol, mlOp, poly(0, 2)]
81+
| "#Forall" #KVariable "." K [klabel(#Forall), symbol, mlOp, poly(0, 2)]
82+
endmodule
83+
6684
// To be used when parsing/pretty-printing symbolic configurations
6785
module KSEQ-SYMBOLIC
6886
imports KSEQ
87+
imports ML-SYNTAX
88+
6989
syntax #KVariable ::= r"(?<![A-Za-z0-9_\\$!\\?])(\\!|\\?)?([A-Z][A-Za-z0-9'_]*|_)" [token, prec(1), autoReject]
7090
| #UpperId [token, autoReject]
7191
syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?])(\\$)([A-Z][A-Za-z0-9'_]*)" [token, autoReject]
7292
syntax KBott ::= #KVariable
7393
syntax KBott ::= KConfigVar
7494
syntax KLabel ::= #KVariable
75-
76-
syntax KBott ::= "#True" [klabel(#True), symbol, poly(0)]
77-
syntax KBott ::= "#False" [klabel(#False), symbol, poly(0)]
78-
syntax KBott ::= "#Not" "(" K ")" [klabel(#Not), symbol, mlOp, poly(0, 1), mlUnary]
79-
| "#Ceil" "(" K ")" [klabel(#Ceil), symbol, mlOp, poly(0; 1), mlUnary]
80-
| "#Floor" "(" K ")" [klabel(#Floor), symbol, mlOp, poly(0; 1), mlUnary]
81-
syntax K ::= "{" K "#Equals" K "}" [klabel(#Equals), symbol, mlOp, format(%1%i%n%2%d%n%3%i%n%4%d%n%5), poly(0; 1, 2), mlEquals]
82-
> K "#And" K [klabel(#And), symbol, assoc, left, comm, unit(#True), mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
83-
> K "#Or" K [klabel(#Or), symbol, assoc, left, comm, unit(#False), mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
84-
> K "#Implies" K [klabel(#Implies), symbol, mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d), mlImplies]
85-
syntax KBott ::= "#Exists" #KVariable "." K [klabel(#Exists), symbol, mlOp, poly(0, 2), mlQuantifier]
86-
| "#Forall" #KVariable "." K [klabel(#Forall), symbol, mlOp, poly(0, 2), mlQuantifier]
87-
88-
syntax priority mlUnary > mlEquals
89-
syntax priority mlImplies > mlQuantifier
9095
endmodule
9196
9297
module KCELLS

‎k-distribution/tests/regression-new/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ SUBDIRS=issue-2273 \
1515
is-variable \
1616
no-dup-rules \
1717
imp-haskell \
18+
imp-llvm \
1819
equals-pattern \
1920
or-llvm \
2021
or-ocaml \

‎k-distribution/tests/regression-new/equals-formatting/eq.k‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,14 @@
33
requires "kast.k"
44

55
module EQ-SYNTAX
6-
imports KSEQ-SYMBOLIC
7-
imports INT
8-
9-
syntax Pgm ::= KBott
6+
imports INT-SYNTAX
107

118
syntax Pgm ::= init ( Int )
129
endmodule
1310

1411
module EQ
1512
imports EQ-SYNTAX
13+
imports ML-SYNTAX
1614

1715
configuration <k color="green"> $PGM:Pgm </k>
1816

‎k-distribution/tests/regression-new/imp-llvm/Makefile‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
DEF=imp
2+
EXT=imp
3+
TESTDIR=.
4+
KOMPILE_BACKEND=llvm
5+
export KOMPILE_BACKEND
6+
7+
include ../../../include/ktest.mak

‎k-distribution/tests/regression-new/imp-llvm/collatz.imp‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// This program tests the Collatz conjecture for all numbers up to m
2+
// and accumulates the total number of steps in s.
3+
4+
int m, n, q, r, s;
5+
m = 10;
6+
while (!(m<=2)) {
7+
n = m;
8+
m = m + -1;
9+
while (!(n<=1)) {
10+
s = s + 1;
11+
q = n/2;
12+
r = q+q + 1;
13+
if (r<=n) {
14+
n = n+n+n + 1; // n becomes 3*n+1 if odd
15+
} else {n=q;} // or n/2 if even
16+
}
17+
}
18+
19+
// s should be 66 when m is 10

‎k-distribution/tests/regression-new/imp-llvm/collatz.imp.out‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
<T>
2+
<k>
3+
.
4+
</k>
5+
<state>
6+
m |-> 2
7+
n |-> 1
8+
q |-> 1
9+
r |-> 3
10+
s |-> 66
11+
</state>
12+
</T>

‎k-distribution/tests/regression-new/imp-llvm/imp.k‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
// Copyright (c) 2014-2019 K Team. All Rights Reserved.
2+
3+
module IMP-SYNTAX
4+
imports BOOL-SYNTAX
5+
imports INT-SYNTAX
6+
imports ID
7+
8+
syntax AExp ::= Int | Id
9+
| "-" Int [format(%1%2)]
10+
| AExp "/" AExp [left, strict, color(pink)]
11+
> AExp "+" AExp [left, strict, color(pink)]
12+
| "(" AExp ")" [bracket]
13+
syntax BExp ::= Bool
14+
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)]
15+
| "!" BExp [strict, color(pink)]
16+
> BExp "&&" BExp [left, strict(1), color(pink)]
17+
| "(" BExp ")" [bracket]
18+
syntax Block ::= "{" "}"
19+
| "{" Stmt "}" [format(%1%i%n%2%d%n%3)]
20+
syntax Stmt ::= Block
21+
| Id "=" AExp ";" [strict(2), color(pink), format(%1 %2 %3%4)]
22+
| "if" "(" BExp ")"
23+
Block "else" Block [strict(1), colors(yellow, white, white, yellow), format(%1 %2%3%4 %5 %6 %7)]
24+
| "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)]
25+
> Stmt Stmt [left, format(%1%n%2)]
26+
27+
syntax Pgm ::= "int" Ids ";" Stmt [format(%1 %2%3%n%4), colors(yellow,pink)]
28+
syntax Ids ::= List{Id,","} [format(%1%2 %3)]
29+
endmodule
30+
31+
module IMP
32+
imports IMP-SYNTAX
33+
imports BOOL
34+
imports INT
35+
imports MAP
36+
37+
syntax KResult ::= Int | Bool
38+
39+
configuration <T color="yellow">
40+
<k color="green"> $PGM:Pgm </k>
41+
<state color="red"> .Map </state>
42+
</T>
43+
44+
rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
45+
46+
rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
47+
rule I1 + I2 => I1 +Int I2
48+
rule - I1 => 0 -Int I1
49+
50+
rule I1 <= I2 => I1 <=Int I2
51+
rule ! T => notBool T
52+
rule true && B => B
53+
rule false && _ => false
54+
55+
rule {} => . [structural]
56+
rule {S} => S [structural]
57+
58+
rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
59+
60+
rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
61+
62+
rule if (true) S else _ => S
63+
rule if (false) _ else S => S
64+
65+
rule while (B) S => if (B) {S while (B) S} else {} [structural]
66+
67+
rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
68+
requires notBool (X in keys(Rho))
69+
rule int .Ids; S => S [structural]
70+
endmodule

‎k-distribution/tests/regression-new/imp-llvm/primes.imp‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// This program counts in s all the prime numbers up to m.
2+
3+
int i, m, n, q, r, s, t, x, y, z;
4+
m = 10; n = 2;
5+
while (n <= m) {
6+
// checking primality of n and writing t to 1 or 0
7+
i = 2; q = n/i; t = 1;
8+
while (i<=q && 1<=t) {
9+
x = i;
10+
y = q;
11+
// fast multiplication (base 2) algorithm
12+
z = 0;
13+
while (!(x <= 0)) {
14+
q = x/2;
15+
r = q+q + 1;
16+
if (r <= x) { z = z+y; } else {}
17+
x = q;
18+
y = y+y;
19+
} // end fast multiplication
20+
if (n <= z) { t = 0; } else { i = i + 1; q = n/i; }
21+
} // end checking primality
22+
if (1 <= t) { s = s + 1; } else {}
23+
n = n + 1;
24+
}
25+
26+
// s should be 4 when m = 10.

‎k-distribution/tests/regression-new/imp-llvm/primes.imp.out‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
<T>
2+
<k>
3+
.
4+
</k>
5+
<state>
6+
i |-> 2
7+
m |-> 10
8+
n |-> 11
9+
q |-> 0
10+
r |-> 1
11+
s |-> 4
12+
t |-> 0
13+
x |-> 0
14+
y |-> 20
15+
z |-> 10
16+
</state>
17+
</T>

0 commit comments

Comments
 (0)