Skip to content

Commit 8205f8b

Browse files
llalexandru00llalexandru00
committed
fixed maps, added keys, improved invariants checking
1 parent fe8e717 commit 8205f8b

26 files changed

+1067
-1125
lines changed

‎bin/alk.jar

15.3 KB
Binary file not shown.

‎input/test.alk

+7-57
Original file line numberDiff line numberDiff line change
@@ -1,79 +1,29 @@
1-
symbolic $a : array<int>;
2-
3-
@Trusted
4-
findMin(a : array<int>, out b : int) modifies x : int uses y : int
5-
requires true
1+
findMin(a : array<int>) : int
62
ensures forall j : int :: 0 <= j && j < a.size() ==> result <= a[j]
7-
ensures exists j : int :: 0 <= j && j < a.size() ==> a[j] == result
3+
ensures exists j : int :: 0 <= j && j < a.size() ==> result == a[j]
84
{
95
i = 0;
106
minim = a[0];
117

128
while (i < a.size())
9+
invariant i <= a.size()
1310
invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j]
1411
modifies i, minim
1512
{
1613
if (a[i] < minim)
1714
{
1815
minim = a[i];
1916
}
20-
i++; (2) (3)
21-
...
17+
i++;
2218
}
23-
if (...)
24-
{
25-
...
26-
return x; (4)
27-
}
28-
29-
return minim; // result = minim; goto finish; (1)
30-
}
3119

32-
swap(out a, out b)
33-
{
34-
...
20+
return minim;
3521
}
3622

37-
a = 2; // <==> -i a |-> 2
38-
assume ...; // <==> -pc ...
39-
40-
// main:
23+
symbolic $a : array<int>;
4124
a = $a;
42-
x = findMin(a);
43-
assert ...;
44-
45-
46-
// interpretori
47-
// concret (fara optiune)
48-
// simbolic (-s)
49-
50-
51-
Executie: (env, store, interpreter, stack, pool ...)
52-
53-
ExecutionPool
54-
55-
executie ->
56-
57-
58-
execution pool:
59-
executia1 -> true
60-
executia2 -> false
61-
executia3 -> true
62-
63-
25+
findMin(a);
6426

65-
// 0) imbogatit gramatica cu requires, ensures, tipuri de date pentru parametrii
6627

67-
// 1) extragere a functiilor -> List<AST>
6828

69-
// 2) analiza funtiilor ->
70-
// 1) havoc input, output, modifies, uses
71-
// 2) assume r
72-
// 3) execute s -> mai multe executii simbolice pe mai multe threaduri
73-
// 4) assert e
7429

75-
// * 3) folosirea functiilor la interpretare ->
76-
// 1) evaluare argumente si initializare parametrii de intrare
77-
// 2) assert r
78-
// 3) havoc output, modifies
79-
// 4) assume e

‎input/test5.alk

+13-14
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,17 @@
1-
a = [1, 2, 3, 4];
2-
i = 0;
3-
minim = a[0];
4-
5-
while (i < a.size())
6-
{
7-
if (a[i] < minim)
8-
{
9-
minim = a[i];
10-
}
11-
i++;
12-
}
13-
14-
print(minim);
1+
a = { "a" |-> 5 };
152

3+
{} x = a.keys()
164

5+
// map-uri (keys)
6+
// invariantii trebuie procesati intr-o singura executie (nu o executie pentru fiecare invariant)
177

8+
// apel conditional la Z3 (-pr)
9+
// dataflow -> cautare secventiala si minim in tablou
10+
// conversia structurilor si a map-urilor in Z3
1811

12+
// redenumit keyword-urile assert, assume, requires, ensures, symbolic, modifies -> @
13+
// operatorul : pentru apartenenta la un tip de date:
14+
// @requires a : array<int> && x : int; -> din gramatica
15+
// @ensures result : int; -> din gramatica
16+
// type assertions
17+
// @Trusted

‎input/test7.alk

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
findMin(a : array<int>) : int
1+
dfs(a : array<int>) : int
22
ensures forall j : int :: 0 <= j && j < a.size() ==> result <= a[j]
33
ensures exists j : int :: 0 <= j && j < a.size() ==> result == a[j]
44
{

‎output.log

+25-113
Original file line numberDiff line numberDiff line change
@@ -1,114 +1,26 @@
1-
=======================CFG========================
2-
3-
"input"
4-
"a=[1,2,3,4];"
5-
"i=0;"
6-
"minim=a[0];"
7-
"while (i<a.size())"
8-
"if (a[i]<minim)"
9-
"print(minim);"
10-
"minim=a[i];"
11-
"i++;"
12-
"output"
13-
"input" "a=[1,2,3,4];"
14-
"a=[1,2,3,4];" "i=0;"
15-
"i=0;" "minim=a[0];"
16-
"minim=a[0];" "while (i<a.size())"
17-
"while (i<a.size())" "if (a[i]<minim)" true-edge
18-
"while (i<a.size())" "print(minim);" false-edge
19-
"if (a[i]<minim)" "minim=a[i];" true-edge
20-
"if (a[i]<minim)" "i++;" false-edge
21-
"print(minim);" "output"
22-
"minim=a[i];" "i++;"
23-
"i++;" "while (i<a.size())"
24-
25-
26-
27-
=====================Dataflow=====================
28-
29-
Exception in thread "Thread-2" util.exception.SMTUnimplementedException: Unimplemented SMT solver for: ast.VirtualAST
30-
at smt.SMTVisitor.visit(SMTVisitor.java:479)
31-
at smt.SMTVisitor.visit(SMTVisitor.java:33)
32-
at ast.VirtualAST.accept(VirtualAST.java:28)
33-
at smt.SMTVisitor.visit(SMTVisitor.java:283)
34-
at smt.SMTVisitor.visit(SMTVisitor.java:33)
35-
at ast.expr.RelationalAST.accept(RelationalAST.java:46)
36-
at smt.AlkSMTContext.process(AlkSMTContext.java:155)
37-
at util.pc.PathCondition.add(PathCondition.java:76)
38-
at util.pc.PathCondition.add(PathCondition.java:66)
39-
at util.pc.PathCondition.<init>(PathCondition.java:59)
40-
at dataflow.domain.ExecutionPath.<init>(ProgramContext.java:220)
41-
at dataflow.domain.ProgramContext.<init>(ProgramContext.java:40)
42-
at dataflow.wcet.SeqWCETLattice.getLUB(SeqWCETLattice.java:24)
43-
at dataflow.wcet.SeqWCETLattice.getLUB(SeqWCETLattice.java:9)
44-
at dataflow.worklist.WorklistFlow.execute(WorklistFlow.java:42)
45-
at dataflow.Dataflow.run(Dataflow.java:27)
46-
minim=a[i]; ->
47-
48-
i++; ->
49-
50-
output ->
51-
52-
minim=a[0]; ->
53-
{
54-
Environment:
55-
a |-> [1, 2, 3, 4]
56-
i |-> 0
57-
Path Condition:
58-
true
59-
}
60-
61-
input ->
62-
{
63-
Environment:
64-
65-
Path Condition:
66-
true
67-
}
68-
69-
i=0; ->
70-
{
71-
Environment:
72-
a |-> [1, 2, 3, 4]
73-
Path Condition:
74-
true
75-
}
76-
77-
a=[1,2,3,4]; ->
78-
{
79-
Environment:
80-
81-
Path Condition:
82-
true
83-
}
84-
85-
print(minim); ->
86-
87-
if (a[i]<minim) ->
88-
89-
while (i<a.size()) ->
90-
{
91-
Environment:
92-
a |-> [1, 2, 3, 4]
93-
minim |-> 1
94-
i |-> 0
95-
Path Condition:
96-
true
97-
}
98-
99-
===================Loop mapping===================
100-
101-
line 5 i<a.size() -> l_0
102-
103-
====================Recurrence====================
104-
105-
Loop 0:
106-
a:
107-
a_l0(0) = [1, 2, 3, 4] when true
108-
109-
minim:
110-
minim_l0(0) = 1 when true
111-
112-
i:
113-
i_l0(0) = 0 when true
1+
Can't use return outside function scope.
2+
a |-> $a_0
3+
[result] |-> $minim_0
4+
minim |-> $minim_0
5+
i |-> $i_0
6+
j |-> $j_1
7+
8+
Note that the execution was symbolic.
9+
Path condition: ($i_0<=$a_0.size()) && forall $j_1 : int :: ((0<=$j_1)&&($j_1<$i_0)) ==> ($minim_0<=$a_0[$j_1]) && !($i_0<$a_0.size()) ($j_0 : int, $i_0 : int, $j_1 : int, $minim_0 : int, $a_0 : array<int>)
10+
11+
Can't use return outside function scope.
12+
a |-> $a_0
13+
[result] |-> $minim_0
14+
minim |-> $minim_0
15+
i |-> $i_0
16+
j |-> $j_1
17+
18+
Note that the execution was symbolic.
19+
Path condition: ($i_0<=$a_0.size()) && forall $j_1 : int :: ((0<=$j_1)&&($j_1<$i_0)) ==> ($minim_0<=$a_0[$j_1]) && !($i_0<$a_0.size()) ($j_0 : int, $i_0 : int, $j_1 : int, $minim_0 : int, $a_0 : array<int>)
20+
21+
Successfully verified: findMin
22+
a |-> $a
23+
24+
Note that the execution was symbolic.
25+
Path condition: forall $j_4 : int :: ((0<=$j_4)&&($j_4<$a.size())) ==> ($[result]_0<=$a[$j_4]) && exists $j_5 : int :: ((0<=$j_5)&&($j_5<$a.size())) ==> ($[result]_0==$a[$j_5]) ($[result]_0 : int, $j_4 : int, $a : array<int>, $j_5 : int)
11426

‎src/main/java/ast/enums/BuiltInMethod.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@
22

33
public enum BuiltInMethod
44
{
5-
AT, DELETE, END, FIRST, INSERT, POPBACK, POPFRONT, PUSHBACK, PUSHFRONT, REMOVE, REMOVEALLEQTO, REMOVEAT,
5+
AT, DELETE, END, FIRST, INSERT, KEYS, POPBACK, POPFRONT, PUSHBACK, PUSHFRONT, REMOVE, REMOVEALLEQTO, REMOVEAT,
66
SIZE, SPLIT, TOPBACK, TOPFRONT, UPDATE
77
}

‎src/main/java/ast/expr/FactorPointMethodAST.java

+9-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,15 @@ public DataTypeAST getDataType(DataTypeProvider dtp)
3838
if (target instanceof IterableDataTypeAST)
3939
return ((IterableDataTypeAST) target).getTypeAst();
4040
else
41-
throw new AlkException("Invalid use of at method on " + target);
41+
throw new AlkException("Invalid use of " + attr.getMethod() + " method on " + target);
42+
}
43+
case KEYS:
44+
{
45+
DataTypeAST target = ((ExpressionAST) getChild(0)).getDataType(dtp);
46+
if (target instanceof MapDataTypeAST)
47+
return new SetDataTypeAST(null);
48+
else
49+
throw new AlkException("Invalid use of keys method on " + target);
4250
}
4351
default: throw new InternalException("Unidentified builtin method in order to detect data type.");
4452
}

‎src/main/java/ast/type/MapDataTypeAST.java

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
package ast.type;
2+
3+
import com.microsoft.z3.Context;
4+
import com.microsoft.z3.Expr;
5+
import com.microsoft.z3.Sort;
6+
import execution.parser.exceptions.NotImplementedException;
7+
import org.antlr.v4.runtime.ParserRuleContext;
8+
9+
public class MapDataTypeAST
10+
extends DataTypeAST
11+
{
12+
public MapDataTypeAST(ParserRuleContext ctx)
13+
{
14+
super(ctx);
15+
}
16+
17+
@Override
18+
public String toString()
19+
{
20+
return "map<" + getChild(0).toString() +">";
21+
}
22+
23+
@Override
24+
public Expr<?> makeExpr(Context ctx, String id)
25+
{
26+
throw new NotImplementedException("Map data type retrieval not implemented!");
27+
}
28+
29+
@Override
30+
public Sort getSort(Context ctx)
31+
{
32+
throw new NotImplementedException("Map data type retrieval not implemented!");
33+
}
34+
}

‎src/main/java/execution/parser/constants/Constants.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
public class Constants
44
{
5-
public static final String VERSION = "3.1";
5+
public static final String VERSION = "3.2";
66
public static int MAX_DECIMALS = 10;
77
public static int MAX_ARRAY = 1000000000;
88
public final static boolean DEBUG = false;

‎src/main/java/execution/parser/exceptions/AlkException.java

+2
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,8 @@ public class AlkException extends InternalException
229229

230230
public final static String ERR_FIRST = "This type of value is not valid for the first function.";
231231

232+
public final static String ERR_KEYS = "This type of value is not valid for the keys method.";
233+
232234
public final static String ERR_INSERT = "This type of value is not valid for the insert function.";
233235
public final static String ERR_INSERT_TOOBIG = "The insert function does not permit such large numbers as a position.";
234236

‎src/main/java/execution/state/expression/BaseMapWithCompsState.java

+14-2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ public class BaseMapWithCompsState
1414
private AlkMap mapping = new AlkMap();
1515
private int step = 0;
1616
private Location key;
17+
private boolean checkKey = true;
1718

1819
public BaseMapWithCompsState(AST tree, ExecutionPayload executionPayload) {
1920
super(tree, executionPayload);
@@ -28,19 +29,29 @@ public ExecutionState makeStep()
2829
return null;
2930
}
3031

31-
return request(tree.getChild(step++));
32+
if (checkKey)
33+
{
34+
return request(tree.getChild(step).getChild(0));
35+
}
36+
else
37+
{
38+
return request(tree.getChild(step).getChild(1));
39+
}
3240
}
3341

3442
@Override
3543
public void assign(ExecutionResult result)
3644
{
37-
if (step % 2 == 1)
45+
if (checkKey)
3846
{
3947
key = generator.generate(result.getValue().toRValue());
48+
checkKey = false;
4049
}
4150
else
4251
{
4352
mapping.put(key, generator.generate(result.getValue().toRValue()));
53+
checkKey = true;
54+
step++;
4455
}
4556
}
4657

@@ -50,6 +61,7 @@ public ExecutionState clone(SplitMapper sm) {
5061
copy.mapping = (AlkMap) this.mapping.weakClone(sm.getLocationMapper());
5162
copy.step = this.step;
5263
copy.key = key != null ? sm.getLocationMapper().get(key) : null;
64+
copy.checkKey = checkKey;
5365
return super.decorate(copy, sm);
5466
}
5567
}

0 commit comments

Comments
 (0)