Skip to content

Commit 2afee47

Browse files
drognanarlexicalscope
authored andcommitted
Makes symbols static
Conflicts: svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/partition/trace/symb/tree/GoalTree.java svm-partition-trace-symb/src/test/java/com/lexicalscope/svm/partition/trace/symb/tree/TestGoalTree.java
1 parent f423d01 commit 2afee47

File tree

22 files changed

+40
-106
lines changed

22 files changed

+40
-106
lines changed

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/EqStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class EqStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value == 0) {
16-
return new TrueSymbol();
16+
return TrueSymbol.TT;
1717
}
18-
return new FalseSymbol();
18+
return FalseSymbol.FF;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/GeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class GeStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value >= 0) {
16-
return new TrueSymbol();
16+
return TrueSymbol.TT;
1717
}
18-
return new FalseSymbol();
18+
return FalseSymbol.FF;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/GtStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class GtStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value > 0) {
16-
return new TrueSymbol();
16+
return TrueSymbol.TT;
1717
}
18-
return new FalseSymbol();
18+
return FalseSymbol.FF;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpEqStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ public final class ICmpEqStrategy implements BinarySBranchOp {
2222

2323
private BoolSymbol pConditionSymbol(final int value1, final int value2) {
2424
if (value1 == value2) {
25-
return new TrueSymbol();
25+
return TrueSymbol.TT;
2626
}
27-
return new FalseSymbol();
27+
return FalseSymbol.FF;
2828
}
2929
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpGeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ public final class ICmpGeStrategy implements BinarySBranchOp {
1717

1818
@Override public BoolSymbol conditionSymbol(final Integer value1, final Integer value2) {
1919
if (value1 >= value2) {
20-
return new TrueSymbol();
20+
return TrueSymbol.TT;
2121
}
22-
return new FalseSymbol();
22+
return FalseSymbol.FF;
2323
}
2424
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpGtStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ public final class ICmpGtStrategy implements BinarySBranchOp {
1717

1818
@Override public BoolSymbol conditionSymbol(final Integer value1, final Integer value2) {
1919
if (value1 > value2) {
20-
return new TrueSymbol();
20+
return TrueSymbol.TT;
2121
}
22-
return new FalseSymbol();
22+
return FalseSymbol.FF;
2323
}
2424
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpLeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ public final class ICmpLeStrategy implements BinarySBranchOp {
1717

1818
@Override public BoolSymbol conditionSymbol(final Integer value1, final Integer value2) {
1919
if (value1 <= value2) {
20-
return new TrueSymbol();
20+
return TrueSymbol.TT;
2121
}
22-
return new FalseSymbol();
22+
return FalseSymbol.FF;
2323
}
2424
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpLtStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ public final class ICmpLtStrategy implements BinarySBranchOp {
1717

1818
@Override public BoolSymbol conditionSymbol(final Integer value1, final Integer value2) {
1919
if (value1 < value2) {
20-
return new TrueSymbol();
20+
return TrueSymbol.TT;
2121
}
22-
return new FalseSymbol();
22+
return FalseSymbol.FF;
2323
}
2424
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/ICmpNeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ public final class ICmpNeStrategy implements BinarySBranchOp {
2121

2222
private BoolSymbol pConditionSymbol(final int value1, final int value2) {
2323
if (value1 != value2) {
24-
return new TrueSymbol();
24+
return TrueSymbol.TT;
2525
}
26-
return new FalseSymbol();
26+
return FalseSymbol.FF;
2727
}
2828
}

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/LeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class LeStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value <= 0) {
16-
return new TrueSymbol();
16+
return TrueSymbol.TT;
1717
}
18-
return new FalseSymbol();
18+
return FalseSymbol.FF;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/LtStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class LtStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value < 0) {
16-
return new TrueSymbol();
16+
return TrueSymbol.TT;
1717
}
18-
return new FalseSymbol();
18+
return FalseSymbol.FF;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/predicates/NeStrategy.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ public final class NeStrategy implements UnarySBranchOp {
1313

1414
@Override public BoolSymbol conditionSymbol(final Integer value) {
1515
if(value == 0) {
16-
return new FalseSymbol();
16+
return FalseSymbol.FF;
1717
}
18-
return new TrueSymbol();
18+
return TrueSymbol.TT;
1919
}
2020

2121
@Override public String toString() {

svm-jinstruction-symb/src/main/java/com/lexicalscope/svm/z3/FeasibilityChecker.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ public FeasibilityChecker() {
4242
throw new RuntimeException("could not enable warning messages", e);
4343
}
4444
//Log.open("test.log");
45-
satisfiableCache.put(new TrueSymbol(), true);
46-
satisfiableCache.put(new FalseSymbol(), false);
45+
satisfiableCache.put(TrueSymbol.TT, true);
46+
satisfiableCache.put(FalseSymbol.FF, false);
4747

4848
final HashMap<String, String> cfg = new HashMap<String, String>();
4949
cfg.put("model", "true");

svm-jinstruction-symb/src/test/java/com/lexicalscope/svm/j/instruction/symbolic/ops/array/TestArrayTheory.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ public class TestArrayTheory {
2323
private final FeasibilityChecker feasbilityChecker = new FeasibilityChecker();
2424

2525
private final StateBuilder state = new StateBuilder();
26-
private final BoolSymbol pc = new TrueSymbol();
26+
private final BoolSymbol pc = TrueSymbol.TT;
2727

2828
@Test public void storeAndSelectAtSymbolicIndex() throws Exception {
2929
final ITerminalSymbol indexSymbol = state.intSymbol();

svm-jsymbols/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/pc/PcBuilder.java

+2-2
Original file line numberDiff line numberDiff line change
@@ -57,10 +57,10 @@ public static BoolSymbol or(final BoolSymbol left, final BoolSymbol right) {
5757
}
5858

5959
public static BoolSymbol truth() {
60-
return new TrueSymbol();
60+
return TrueSymbol.TT;
6161
}
6262

6363
public static BoolSymbol falsity() {
64-
return new FalseSymbol();
64+
return FalseSymbol.FF;
6565
}
6666
}

svm-jsymbols/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/symbols/FalseSymbol.java

+5-9
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@
22

33

44
public class FalseSymbol implements BoolSymbol {
5+
public static FalseSymbol FF = new FalseSymbol();
6+
7+
private FalseSymbol() { }
8+
59
@Override public boolean isTT() {
610
return false;
711
}
@@ -27,14 +31,6 @@ public class FalseSymbol implements BoolSymbol {
2731
}
2832

2933
@Override public BoolSymbol not() {
30-
return new TrueSymbol();
31-
}
32-
33-
@Override public int hashCode() {
34-
return FalseSymbol.class.hashCode();
35-
}
36-
37-
@Override public boolean equals(final Object obj) {
38-
return obj != null && obj.getClass().equals(this.getClass());
34+
return TrueSymbol.TT;
3935
}
4036
}

svm-jsymbols/src/main/java/com/lexicalscope/svm/j/instruction/symbolic/symbols/TrueSymbol.java

+5-9
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@
22

33

44
public final class TrueSymbol implements BoolSymbol {
5+
public static TrueSymbol TT = new TrueSymbol();
6+
7+
private TrueSymbol() {}
8+
59
@Override public boolean isTT() {
610
return true;
711
}
@@ -23,18 +27,10 @@ public final class TrueSymbol implements BoolSymbol {
2327
}
2428

2529
@Override public BoolSymbol not() {
26-
return new FalseSymbol();
30+
return FalseSymbol.FF;
2731
}
2832

2933
@Override public String toString() {
3034
return "TT";
3135
}
32-
33-
@Override public int hashCode() {
34-
return TrueSymbol.class.hashCode();
35-
}
36-
37-
@Override public boolean equals(final Object obj) {
38-
return obj != null && obj.getClass().equals(this.getClass());
39-
}
4036
}

svm-jvm-symb/src/main/java/com/lexicalscope/svm/vm/symb/SymbVmFactory.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ public static JvmBuilder symbolicVmBuilder(
3131
.useNatives(SymbolicNativeMethods.natives())
3232
.instructionFactory(instructionFactory)
3333
.heapFactory(heapFactory)
34-
.meta(PC, new TrueSymbol())
34+
.meta(PC, TrueSymbol.TT)
3535
.meta(TERMINATION, false)
3636
.meta(SC, 0));
3737
return vmBuilder;

svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/partition/trace/symb/tree/AbstractGoalMap.java

-21
This file was deleted.

svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/partition/trace/symb/tree/GoalMap.java

-23
This file was deleted.

svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/partition/trace/symb/tree/GoalMapFactory.java

-6
This file was deleted.

svm-partition-trace-symb/src/main/java/com/lexicalscope/svm/partition/trace/symb/tree/InputSubset.java

-8
This file was deleted.

0 commit comments

Comments
 (0)