Skip to content

Commit 3b3cb30

Browse files
drognanarlexicalscope
drognanar
authored and
lexicalscope
committedJun 8, 2015
Updates the symbolic methods
Moves all methods to the symbolic instructions package. By this the methods can access symbolic state. Improves the selectState method. Because the states are split based on their choice PC no longer needs to be updated. Improves performance of the newSymbol method. Caches the symbols so that they do not need to be constructed per vm instance. Makes all random selection methods use the `pushValues` method. Conflicts: svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/SymbolicNativeMethods.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_countParameters.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_getPassedParameter.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_newSymbol.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_passParameter.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_randomChoice.java svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_selectState.java svm-jnatives/src/main/java/com/lexicalscope/svm/j/natives/DefaultNativeMethods.java
1 parent 3641ebc commit 3b3cb30

File tree

7 files changed

+149
-10
lines changed

7 files changed

+149
-10
lines changed
 

‎svm-jinstruction-symb/pom.xml

+6
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,12 @@
3636
<artifactId>svm-jinstruction</artifactId>
3737
<version>${project.version}</version>
3838
</dependency>
39+
<dependency>
40+
<!-- this shouldn't be here, the stuff that needs it should be split out -->
41+
<groupId>com.lexicalscope.symb</groupId>
42+
<artifactId>svm-partition-trace</artifactId>
43+
<version>${project.version}</version>
44+
</dependency>
3945
<dependency>
4046
<groupId>com.lexicalscope.symb</groupId>
4147
<artifactId>svm-jsymbols</artifactId>

‎svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/SymbolicNativeMethods.java

+4-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,10 @@ public static NativeMethods natives() {
1212
symbolicNatives.addAll(DefaultNativeMethods.nativeMethodList());
1313
symbolicNatives.add(new Symbolic_newArray("newCharArraySymbol", "()[C"));
1414
symbolicNatives.add(new Symbolic_Java_lang_system_arraycopy());
15-
15+
symbolicNatives.add(new Symbolic_selectState());
16+
symbolicNatives.add(new Symbolic_randomChoice());
17+
symbolicNatives.add(new Symbolic_newSymbol("newIntSymbol", "()I"));
18+
symbolicNatives.add(new Symbolic_newSymbol("newBooleanSymbol", "()Z"));
1619
return DefaultNativeMethods.natives(symbolicNatives);
1720
}
1821
}

‎svm-jnatives/src/main/java/com/lexicalscope/svm/j/natives/Symbolic_newSymbol.java ‎svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_newSymbol.java

+27-5
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,31 @@
1-
package com.lexicalscope.svm.j.natives;
1+
package com.lexicalscope.svm.j.instruction.symbolic.ops.natives;
22

33
import static com.lexicalscope.svm.j.instruction.concrete.object.SymbolCounterMetaKey.SC;
44
import static com.lexicalscope.svm.j.statementBuilder.StatementBuilder.statements;
55

66
import com.lexicalscope.svm.j.instruction.factory.InstructionSource;
7+
import com.lexicalscope.svm.j.instruction.symbolic.symbols.ISymbol;
78
import com.lexicalscope.svm.j.instruction.symbolic.symbols.ITerminalSymbol;
9+
import com.lexicalscope.svm.j.natives.AbstractNativeMethodDef;
810
import com.lexicalscope.svm.vm.j.InstructionQuery;
911
import com.lexicalscope.svm.vm.j.JState;
1012
import com.lexicalscope.svm.vm.j.MethodBody;
1113
import com.lexicalscope.svm.vm.j.Vop;
1214

15+
import java.util.ArrayList;
16+
1317
/**
1418
* Class that allows dynamic creation of int symbols in execution.
1519
*/
1620
public class Symbolic_newSymbol extends AbstractNativeMethodDef {
21+
public static final int INITIAL_CAPACITY = 128;
22+
private static ArrayList<ISymbol> symbols = new ArrayList<>(INITIAL_CAPACITY);
23+
{
24+
for (int i = 0; i < INITIAL_CAPACITY; i++) {
25+
symbols.add(i, new ITerminalSymbol(String.format("s%d", i)));
26+
}
27+
}
28+
1729
public Symbolic_newSymbol(final String methodName, final String signature) {
1830
super("com/lexicalscope/svm/j/instruction/symbolic/symbols/SymbolFactory", methodName, signature);
1931
}
@@ -31,15 +43,25 @@ public MethodBody instructions(final InstructionSource instructions) {
3143
private class GetSymbolOp implements Vop {
3244
@Override
3345
public void eval(final JState ctx) {
34-
final int counter = ctx.getMeta(SC);
35-
final ITerminalSymbol symbol = new ITerminalSymbol(String.format("%s%d", "symbol", counter));
36-
ctx.setMeta(SC, counter + 1);
37-
ctx.push(symbol);
46+
ctx.push(getNewSymbol(ctx));
3847
}
3948

4049
@Override
4150
public <T> T query(final InstructionQuery<T> instructionQuery) {
4251
return instructionQuery.nativ3();
4352
}
4453
}
54+
55+
public static ISymbol getNewSymbol(JState ctx) {
56+
int counter = ctx.getMeta(SC);
57+
ISymbol symbol;
58+
if (counter < symbols.size()) {
59+
symbol = symbols.get(counter);
60+
} else {
61+
symbol = new ITerminalSymbol(counter);
62+
symbols.add(symbol);
63+
}
64+
ctx.setMeta(SC, counter + 1);
65+
return symbol;
66+
}
4567
}

‎svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_randomChoice.java

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
package com.lexicalscope.svm.j.instruction.symbolic.ops.natives;
2+
3+
import com.lexicalscope.svm.j.instruction.factory.InstructionSource;
4+
import com.lexicalscope.svm.j.natives.AbstractNativeMethodDef;
5+
import com.lexicalscope.svm.vm.j.InstructionQuery;
6+
import com.lexicalscope.svm.vm.j.JState;
7+
import com.lexicalscope.svm.vm.j.MethodBody;
8+
import com.lexicalscope.svm.vm.j.Vop;
9+
10+
import static com.lexicalscope.svm.j.statementBuilder.StatementBuilder.statements;
11+
12+
public class Symbolic_randomChoice extends AbstractNativeMethodDef {
13+
public Symbolic_randomChoice() {
14+
super("com/lexicalscope/svm/j/instruction/symbolic/symbols/SymbolFactory", "randomChoice", "()Z");
15+
}
16+
17+
@Override
18+
public MethodBody instructions(InstructionSource instructions) {
19+
return statements(instructions)
20+
.maxStack(1)
21+
.maxLocals(1)
22+
.linearOp(new RandomChoiceOp())
23+
.return1(name()).build();
24+
}
25+
26+
private class RandomChoiceOp implements Vop {
27+
@Override
28+
public void eval(JState ctx) {
29+
Object[] values = new Object[] {0, 1};
30+
Symbolic_selectState.pushValues(ctx, values);
31+
}
32+
33+
@Override
34+
public <T> T query(InstructionQuery<T> instructionQuery) {
35+
return instructionQuery.nativ3();
36+
}
37+
}
38+
}

‎svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/ops/natives/Symbolic_selectState.java

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
package com.lexicalscope.svm.j.instruction.symbolic.ops.natives;
2+
3+
import static com.lexicalscope.svm.j.statementBuilder.StatementBuilder.statements;
4+
import static com.lexicalscope.svm.partition.trace.TraceMetaKey.TRACE;
5+
6+
import com.lexicalscope.svm.j.instruction.factory.InstructionSource;
7+
import com.lexicalscope.svm.j.natives.AbstractNativeMethodDef;
8+
import com.lexicalscope.svm.partition.trace.HashTrace;
9+
import com.lexicalscope.svm.partition.trace.Trace;
10+
import com.lexicalscope.svm.vm.j.InstructionQuery;
11+
import com.lexicalscope.svm.vm.j.JState;
12+
import com.lexicalscope.svm.vm.j.MethodBody;
13+
import com.lexicalscope.svm.vm.j.Vop;
14+
import com.lexicalscope.svm.vm.j.klass.SMethodDescriptor;
15+
16+
/**
17+
* Method which chooses a number randomly between 0 and (count - 1) creating n choices.
18+
*/
19+
public class Symbolic_selectState extends AbstractNativeMethodDef {
20+
public Symbolic_selectState() {
21+
super("com/lexicalscope/svm/j/instruction/symbolic/symbols/SymbolFactory", "selectState", "(I)I");
22+
}
23+
24+
@Override
25+
public MethodBody instructions(InstructionSource instructions) {
26+
return statements(instructions)
27+
.maxStack(1)
28+
.maxLocals(1)
29+
.linearOp(new SelectStateOp())
30+
.return1(name()).build();
31+
}
32+
33+
public static void pushValues(JState ctx, Object[] values) {
34+
SMethodDescriptor context = (SMethodDescriptor) ctx.currentFrame().context();
35+
Trace trace = ctx.getMeta(TRACE);
36+
trace = trace.extend(context, HashTrace.CallReturn.CALL, 0);
37+
ctx.setMeta(TRACE, trace);
38+
39+
JState[] forks = new JState[values.length];
40+
for (int i = 0; i < values.length; i++) {
41+
forks[i] = ctx.snapshot();
42+
forks[i].push(values[i]);
43+
44+
Trace forkTrace = trace.extend(context, HashTrace.CallReturn.RETURN, 0, i);
45+
forks[i].setMeta(TRACE, forkTrace);
46+
}
47+
48+
ctx.forkDisjoined(forks);
49+
}
50+
51+
private class SelectStateOp implements Vop {
52+
@Override
53+
public void eval(JState ctx) {
54+
int count = (int) ctx.pop();
55+
assert count > 0: "Cannot select one from 0 states.";
56+
Object[] values = new Object[count];
57+
for (int i = 0; i < count; i++) {
58+
values[i] = i;
59+
}
60+
61+
pushValues(ctx, values);
62+
}
63+
64+
@Override
65+
public <T> T query(InstructionQuery<T> instructionQuery) {
66+
return instructionQuery.nativ3();
67+
}
68+
}
69+
}

‎svm-jnatives/src/main/java/com/lexicalscope/svm/j/natives/DefaultNativeMethods.java

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

33
import static com.lexicalscope.svm.j.statementBuilder.StatementBuilder.statements;
44

5-
import java.util.ArrayList;
65
import java.util.Arrays;
76
import java.util.HashMap;
87
import java.util.List;
@@ -65,9 +64,7 @@ public static List<NativeMethodDef> nativeMethodList() {
6564
new Sun_misc_unsafe_arrayIndexScale(),
6665
new Sun_misc_unsafe_addressSize(),
6766
new Sun_reflect_reflection_getCallerClass(),
68-
new Java_security_accessController_doPrivileged(),
69-
new Symbolic_newSymbol("newIntSymbol", "()I"),
70-
new Symbolic_newSymbol("newBooleanSymbol", "()Z")
67+
new Java_security_accessController_doPrivileged()
7168
);
7269
}
7370

‎svm-partition-trace-symb/src/test/java/com/lexicalscope/svm/partition/trace/symb/search/FakeVmState.java

+4
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,10 @@ public FakeVmState(final String string) {
9494

9595
}
9696

97+
@Override public void forkDisjoined(JState[] states) {
98+
99+
}
100+
97101
@Override public JState[] fork() {
98102
return null;
99103
}

0 commit comments

Comments
 (0)
Please sign in to comment.