Skip to content

Commit 37f208b

Browse files
llalexandru00llalexandru00
committed
various dataflow fixes
1 parent 8205f8b commit 37f208b

13 files changed

Lines changed: 177 additions & 65 deletions

File tree

‎.idea/codeStyles/Project.xml‎

Lines changed: 31 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎bin/alk.jar‎

219 KB
Binary file not shown.

‎input/test.alk‎

Lines changed: 48 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,55 @@
1-
findMin(a : array<int>) : int
2-
ensures forall j : int :: 0 <= j && j < a.size() ==> result <= a[j]
3-
ensures exists j : int :: 0 <= j && j < a.size() ==> result == a[j]
1+
/*
2+
3+
symbolic $n : int;
4+
5+
sum = 0;
6+
n = $n;
7+
8+
i = 1;
9+
while (i <= n)
10+
// invariant sum == i * (i - 1) / 2 && i <= n + 1
411
{
5-
i = 0;
6-
minim = a[0];
7-
8-
while (i < a.size())
9-
invariant i <= a.size()
10-
invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j]
11-
modifies i, minim
12-
{
13-
if (a[i] < minim)
14-
{
15-
minim = a[i];
16-
}
17-
i++;
18-
}
19-
20-
return minim;
12+
sum = sum + i;
13+
i++;
2114
}
2215

23-
symbolic $a : array<int>;
24-
a = $a;
25-
findMin(a);
16+
// sum |->
17+
// i |->
18+
*/
19+
20+
symbolic $n : int;
21+
symbolic $i : int, $sum : int;
22+
23+
sum = 0;
24+
i = 1;
25+
n = $n;
26+
27+
// proof obligation 1: the invariant holds in the initial state of while
28+
assert sum == i * (i - 1) / 2 && i <= n + 1;
29+
30+
// general: am ajuns la un while cu annotation de invariant
31+
assert invariant; // in configuratia curenta
32+
33+
// proof obligation 2: check the loop invariant
34+
havoc i, sum;
35+
// asignam la variabilele care urmeaza sa fie modificate in while valori simbolice
36+
37+
38+
// dupa executia buclei while
39+
havoc i, sum;
40+
41+
42+
assume invariant && !(conditia);
43+
// continue executia
2644

45+
// \forall 0 <= t < w. $i(t) = $i(t - 1) + 1;
2746

2847

48+
// a |-> $a_l0(t)
49+
// a |-> $a_l1(t)
2950

51+
havoc a, b, c;
52+
=============
53+
a = fresh("a", type(a));
54+
b = fresh("b", type(b));
55+
c = fresh("c", type(c));

‎input/test7.alk‎

Lines changed: 11 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,18 @@
1-
dfs(a : array<int>) : int
2-
ensures forall j : int :: 0 <= j && j < a.size() ==> result <= a[j]
3-
ensures exists j : int :: 0 <= j && j < a.size() ==> result == a[j]
4-
{
5-
i = 0;
6-
minim = a[0];
1+
a = [1, 2, 3, 4, 5];
2+
i = 0;
3+
minim = a[0];
74

8-
while (i < a.size())
9-
invariant i <= a.size()
10-
invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j]
11-
modifies i, minim
5+
while (i < a.size())
6+
// invariant i <= a.size()
7+
// invariant forall j : int :: 0 <= j && j < i ==> minim <= a[j]
8+
// modifies i, minim
9+
{
10+
if (a[i] < minim)
1211
{
13-
if (a[i] < minim)
14-
{
15-
minim = a[i];
16-
}
17-
i++;
12+
minim = a[i];
1813
}
19-
20-
return minim;
14+
i++;
2115
}
2216

23-
symbolic $a : array<int>;
24-
a = $a;
25-
x = findMin(a);
26-
2717

2818

‎src/main/java/dataflow/domain/ProgramContext.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ public static ProgramContext getInitialContext()
4545
{
4646
ProgramContext ctx = new ProgramContext();
4747
StoreImpl store = new StoreImpl();
48-
ctx.addExecutionPath(new ExecutionPath(store, new EnvironmentImpl(store), new PathCondition()));
48+
ctx.addExecutionPath(new ExecutionPath(store, new EnvironmentImpl(store), new PathCondition(false)));
4949
return ctx;
5050
}
5151

@@ -230,13 +230,13 @@ public void run(AST tree, EdgeData data)
230230
{
231231
if (data.getCondition())
232232
{
233-
this.pc.add(SymbolicValue.toSymbolic(value), false);
233+
this.pc.add(SymbolicValue.toSymbolic(value));
234234
}
235235
else
236236
{
237237
SymbolicValue symVal = SymbolicValue.toSymbolic(value);
238238
AST negatedAst = UnaryAST.createUnary(Operator.NOT, symVal.toAST());
239-
this.pc.add(new SymbolicValue(negatedAst), false);
239+
this.pc.add(new SymbolicValue(negatedAst));
240240
}
241241
}
242242
}

‎src/main/java/execution/Execution.java‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ public Execution(Configuration config,
9292
this.registerEnv(global);
9393
funcManager = new FuncManager();
9494
interpreterManager = manager;
95-
conditionPath = new PathCondition();
95+
conditionPath = new PathCondition(config.hasProver());
9696
annoHelper = new AnnoHelper();
9797
}
9898

@@ -123,7 +123,7 @@ private boolean initialize()
123123

124124
if (config.getConditionPath() != null)
125125
{
126-
conditionPath = PathCondition.parse(config.getConditionPath());
126+
conditionPath = PathCondition.parse(config.getConditionPath(), config.hasProver());
127127
}
128128

129129
return true;
@@ -193,6 +193,7 @@ private void execute()
193193
}
194194
}
195195

196+
// EXECUTIA ALGORITMULUI ALK
196197
stack.run();
197198

198199
// if the metadata flag is set, print the global environment
@@ -258,6 +259,10 @@ public void run()
258259
output.hasError = true;
259260
config.getErrorManager().handleError(e);
260261
}
262+
catch (Throwable e)
263+
{
264+
output.hasError = true;
265+
}
261266
finally
262267
{
263268
config.getIOManager().flush();

‎src/main/java/execution/Symbolic.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ public static void verifyFunction(AlkFunction function, Execution exec)
2727

2828
StoreImpl store = new StoreImpl();
2929
Environment env = new EnvironmentImpl(store);
30-
PathCondition pc = new PathCondition();
30+
PathCondition pc = new PathCondition(exec.getConfig().hasProver());
3131

3232
for (int i = 0; i < function.getParams().size(); i++)
3333
{

‎src/main/java/execution/utils/Stepper.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ public static Storable run(AST root,
3030
exec.setStore(store);
3131
exec.setGlobal(env);
3232
exec.setFuncManager(funcManager);
33-
exec.setPathCondition(pathCondition == null ? new PathCondition() : pathCondition);
33+
exec.setPathCondition(pathCondition == null ? new PathCondition(config.hasProver()) : pathCondition);
3434

3535
SymbolicExecutionPayload payload = new SymbolicExecutionPayload(exec, exec.getGlobal());
3636
ExecutionState state = exec.getInterpreterManager().interpret(root, payload);
@@ -53,7 +53,7 @@ public static List<ExecutionOutput> runBatch(AST root,
5353
exec.setStore(store);
5454
exec.setGlobal(env);
5555
exec.setFuncManager(funcManager);
56-
exec.setPathCondition(pathCondition == null ? new PathCondition() : pathCondition);
56+
exec.setPathCondition(pathCondition == null ? new PathCondition(config.hasProver()) : pathCondition);
5757

5858
SymbolicExecutionPayload payload = new SymbolicExecutionPayload(exec, exec.getGlobal());
5959
ExecutionState state = exec.getInterpreterManager().interpret(root, payload);

‎src/main/java/io/AlkConsole.java‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,9 +82,13 @@ public AlkConsole(String[] args)
8282
options.addOption(trace);
8383

8484
Option exhaustive = new Option("e", "exhaustive", false, "trigger exhaustive mode");
85-
trace.setRequired(false);
85+
exhaustive.setRequired(false);
8686
options.addOption(exhaustive);
8787

88+
Option prover = new Option("pr", "prover", false, "define the prover to be used");
89+
prover.setRequired(false);
90+
options.addOption(prover);
91+
8892
CommandLineParser cmdparser = new DefaultParser();
8993

9094
try
@@ -210,6 +214,18 @@ public String getConditionPath()
210214
return cmd.getOptionValue("pathcondition");
211215
}
212216

217+
@Override
218+
public boolean hasProver()
219+
{
220+
return cmd.hasOption("prover");
221+
}
222+
223+
@Override
224+
public String getProver()
225+
{
226+
return cmd.getOptionValue("prover");
227+
}
228+
213229
public IOManager getEndpoint()
214230
{
215231
return this;

‎src/main/java/util/Configuration.java‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ public class Configuration
4141

4242
private String conditionPath;
4343

44+
private String prover;
45+
4446
/** The debugMode flag, used to print the stach trace in case of one exception*/
4547
private boolean debugMode;
4648

@@ -120,6 +122,18 @@ public String getConditionPath()
120122
return conditionPath;
121123
}
122124

125+
@Override
126+
public boolean hasProver()
127+
{
128+
return prover != null;
129+
}
130+
131+
@Override
132+
public String getProver()
133+
{
134+
return prover;
135+
}
136+
123137
/**
124138
* Used for identifying the metadata flag based on the internal members
125139
*
@@ -179,6 +193,7 @@ public void importOptions(OptionProvider op)
179193
this.help = op.hasHelp();
180194
this.staticVerif = op.hasStaticVerif();
181195
this.conditionPath = op.getConditionPath();
196+
this.prover = op.hasProver() ? op.getProver() : null;
182197
}
183198

184199
/**

0 commit comments

Comments
 (0)