Skip to content

Commit 4a3bcbe

Browse files
andreiarusoaieandreiarusoaie
committed
symbolic execution: first experiments
1. Marked two rules for if with [symbolic-rule] 2. Added the directory "symbolic" with 3 examples. Two of them work, the third needs extra investigation.
1 parent 5fbdaa6 commit 4a3bcbe

File tree

4 files changed

+244
-0
lines changed

4 files changed

+244
-0
lines changed

‎semantics/statements.k‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,9 +117,11 @@ context 'If(HOLE,,_,,_)
117117
118118
rule [IfTrue]:
119119
'If(true::bool,, S:K,, _) => S
120+
[symbolic-rule]
120121

121122
rule [IfFalse]:
122123
'If(false::bool,, _,, S:K) => S
124+
[symbolic-rule]
123125
124126
rule [IfThenDesugar]:
125127
'If(E:K,,S1:K) => 'If(E:K,, S1:K,, .K)

‎symbolic/main.java‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/*
2+
$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
3+
4+
time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"test\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/main.java -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
5+
6+
Expected output (unreached at the moment): 11 solutions, none of them containing error message.
7+
*/
8+
import java.util.*;
9+
10+
class LList {
11+
int a[] = new int[10];
12+
int size, capacity;
13+
14+
LList () { size = 0; capacity = 10; }
15+
16+
void insert (int x) {
17+
if (size < capacity) {
18+
a[size] = x;
19+
++size;
20+
}
21+
}
22+
23+
void delete(int x) {
24+
int i = 0;
25+
while (i < size-1 && a[i] != x) {
26+
i = i + 1;
27+
}
28+
if (a[i] == x) {
29+
while (i < size - 1) {
30+
a[i] = a[i+1];
31+
i = i + 1;
32+
}
33+
size = size - 1;
34+
}
35+
}
36+
37+
int getAt(int i) {
38+
if (i < size) {
39+
return a[i];
40+
}
41+
return -1;
42+
}
43+
44+
boolean eqTo(LList l) {
45+
if (size != l.size) {
46+
return false;
47+
}
48+
int i = 0;
49+
while (i < size - 1 && a[i] == l.getAt(i)) {
50+
i = i + 1;
51+
}
52+
if (a[i] == l.getAt(i)) {
53+
return true;
54+
}
55+
return false;
56+
}
57+
58+
LList copy() {
59+
LList t = new LList();
60+
int i = 0;
61+
t.size = size;
62+
while(i < size) {
63+
t.a[i] = a[i];
64+
i = i + 1;
65+
}
66+
return t;
67+
}
68+
}
69+
70+
class OrderedList extends LList {
71+
72+
OrderedList() {
73+
super();
74+
}
75+
76+
void insert(int x) {
77+
if (size < capacity) {
78+
int i = 0;
79+
while(i < size && a[i] <= x) { i = i + 1; }
80+
++size;
81+
int k = size - 1;
82+
while(k > i) { a[k] = a[k-1]; k = k - 1; }
83+
a[i] = x;
84+
}
85+
}
86+
87+
OrderedList copy() {
88+
OrderedList t = new OrderedList();
89+
int i = 0;
90+
t.size = size;
91+
while(i < size) { t.a[i] = a[i]; i = i + 1; }
92+
return t;
93+
}
94+
}
95+
96+
public class main {
97+
public static void main(String[] args) {
98+
int i = 0;
99+
LList l1 = new OrderedList();
100+
Scanner scanner = new Scanner(System.in);
101+
while (i < 2) {
102+
l1.insert(scanner.nextInt());
103+
i = i+1;
104+
}
105+
int x = scanner.nextInt();
106+
107+
LList l2 = l1.copy();
108+
l1.insert(x);
109+
l1.delete(x);
110+
if (l2.eqTo(l1) == false) {
111+
System.out.println("error");
112+
}
113+
}
114+
}

‎symbolic/max3.java‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/*
2+
$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
3+
4+
time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"max3\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/max3.java -cIN="ListItem(3) ListItem(#symInt(x)) ListItem(8)" -cPC=true --search
5+
6+
Expected output: 3 solutions
7+
*/
8+
import java.util.*;
9+
10+
public class max3 {
11+
12+
public static void main(String[] args) {
13+
System.out.print("Insert 3 numbers: ");
14+
Scanner scanner = new Scanner(System.in);
15+
int a = scanner.nextInt();
16+
int b = scanner.nextInt();
17+
int c = scanner.nextInt();
18+
int max;
19+
if (a > b) {
20+
if (a > c) {
21+
max = a;
22+
} else {
23+
max = c;
24+
}
25+
} else {
26+
if (b > c) {
27+
max = b;
28+
} else {
29+
max = c;
30+
}
31+
}
32+
System.out.println("max = " + max);
33+
System.out.println("Done!");
34+
}
35+
}
36+
37+
// (for input 6 12 8)
38+
39+
// Insert 3 numbers: max = 12
40+
// Done!

‎symbolic/test.java‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
/*
2+
$KOMPILE_CMD -v java --symbolic-rules "symbolic-rule" --backend symbolic
3+
4+
time timeout 300 krun --debug-info --color extended --directory="/home/andrei.arusoaie/work/java-semantics/tools/../semantics" --main-module=JAVA -cMainClass="ListItem(\"test\")" -cModelCheck="false" --output=pretty --parser="kj-parse-aggreg.sh" ../symbolic/test.java -cIN="ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))" -cPC="true" --search
5+
6+
Expected output: 4 solutions, one of them containing error message.
7+
*/
8+
import java.util.*;
9+
10+
class List {
11+
int a[] = new int[10];
12+
int size, capacity;
13+
14+
List () { size = 0; capacity = 10; }
15+
16+
void insert (int x) {
17+
if (size < capacity) {
18+
a[size] = x;
19+
++size;
20+
}
21+
}
22+
23+
void delete(int x) {
24+
int i = 0;
25+
while (i < size-1 && a[i] != x) {
26+
i = i + 1;
27+
}
28+
if (a[i] == x) {
29+
while (i < size - 1) {
30+
a[i] = a[i+1];
31+
i = i + 1;
32+
}
33+
size = size - 1;
34+
}
35+
}
36+
37+
int getAt(int i) {
38+
if (i < size) {
39+
return a[i];
40+
}
41+
return -1;
42+
}
43+
44+
boolean eqTo(List l) {
45+
if (size != l.size) {
46+
return false;
47+
}
48+
int i = 0;
49+
while (i < size - 1 && a[i] == l.getAt(i)) {
50+
i = i + 1;
51+
}
52+
if (a[i] == l.getAt(i)) {
53+
return true;
54+
}
55+
return false;
56+
}
57+
58+
List copy() {
59+
List t = new List();
60+
int i = 0;
61+
t.size = size;
62+
while(i < size) {
63+
t.a[i] = a[i];
64+
i = i + 1;
65+
}
66+
return t;
67+
}
68+
}
69+
70+
public class test {
71+
public static void main(String[] args) {
72+
int i = 0;
73+
List l1 = new List();
74+
Scanner scanner = new Scanner(System.in);
75+
while (i < 2) {
76+
l1.insert(scanner.nextInt());
77+
i = i+1;
78+
}
79+
int x = scanner.nextInt();
80+
81+
List l2 = l1.copy();
82+
l1.insert(x);
83+
l1.delete(x);
84+
if (l2.eqTo(l1) == false) {
85+
System.out.println("error");
86+
}
87+
}
88+
}

0 commit comments

Comments
 (0)