Skip to content

Commit 67f96cc

Browse files
committed
Removed all debug printing
1 parent 4891439 commit 67f96cc

File tree

14 files changed

+30
-96
lines changed

14 files changed

+30
-96
lines changed

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -21,45 +21,32 @@ public static void main(String[] args) {
2121
if (ee.foundError()) {
2222
System.out.println(ee.getFullMessage());
2323
System.exit(ee.getErrorStatus());
24-
} else {
25-
System.out.println("Analysis complete!");
2624
}
2725
}
2826

2927
public static ErrorEmitter launchTest(String file) {
3028
ErrorEmitter ee = launch(file);
31-
if (ee.foundError()) {
32-
System.out.println(ee.getFullMessage());
33-
// System.exit(ee.getErrorStatus());
34-
} else {
35-
System.out.println("Analysis complete!");
36-
}
3729
return ee;
3830
}
3931

4032
public static ErrorEmitter launch(String file) {
4133
Launcher launcher = new Launcher();
42-
System.out.println("File path in launch before spoon:" + file);
4334
launcher.addInputResource(file);
4435
launcher.getEnvironment().setNoClasspath(true);
4536
// optional
4637
// launcher.getEnvironment().setSourceClasspath(
4738
// "lib1.jar:lib2.jar".split(":"));
4839
launcher.getEnvironment().setComplianceLevel(8);
4940

50-
System.out.println("before run");
5141
launcher.run();
5242

53-
System.out.println("after run");
54-
5543
final Factory factory = launcher.getFactory();
5644
final ProcessingManager processingManager = new QueueProcessingManager(factory);
5745

5846
ErrorEmitter ee = new ErrorEmitter();
5947
final RefinementProcessor processor = new RefinementProcessor(factory, ee);
6048
processingManager.addProcessor(processor);
6149

62-
System.out.println("before process");
6350
try {
6451
// To only search the last package - less time spent
6552
CtPackage v = factory.Package().getAll().stream().reduce((first, second) -> second).orElse(null);

liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,6 @@ public <T> void visitCtClass(CtClass<T> ctClass) {
3535

3636
ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int"))
3737
.forEach(fld -> {
38-
System.out.println("generated field ghost in class " + ctClass.getQualifiedName() + " for field "
39-
+ fld.getSimpleName());
4038
CtTypeReference<?> fld_type = fld.getType();
4139
CtAnnotation<?> gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
4240
gen_ann.addValue("value", fld_type.getSimpleName() + " " + fld.getSimpleName());

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ public class ExternalRefinementTypeChecker extends TypeChecker {
2626

2727
public ExternalRefinementTypeChecker(Context context, Factory fac, ErrorEmitter errorEmitter) {
2828
super(context, fac, errorEmitter);
29-
System.out.println("ExternalRefinementTypeChecker");
3029
}
3130

3231
@Override
@@ -94,7 +93,6 @@ protected void getGhostFunction(String value, CtElement element) {
9493
String d = a[a.length - 1];
9594
GhostFunction gh = new GhostFunction(f, factory, prefix, d);
9695
context.addGhostFunction(gh);
97-
System.out.println(gh.toString());
9896
}
9997

10098
} catch (ParsingException e) {
@@ -113,7 +111,6 @@ protected Optional<GhostFunction> createStateGhost(int order, CtElement element)
113111
List<String> params = Arrays.asList(klass);
114112
GhostFunction gh = new GhostFunction(String.format("%s_state%d", klass.toLowerCase(), order), params, ret,
115113
factory, prefix, klass);
116-
System.out.println(gh.toString());
117114
return Optional.of(gh);
118115
}
119116
return Optional.empty();

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,13 @@ public MethodsFirstChecker(Context c, Factory fac, ErrorEmitter errorEmitter) {
2323
super(c, fac, errorEmitter);
2424
mfc = new MethodsFunctionsChecker(this);
2525
visitedClasses = new ArrayList<>();
26-
System.out.println("In Methids First Checker");
2726
}
2827

2928
@Override
3029
public <T> void visitCtClass(CtClass<T> ctClass) {
3130
if (errorEmitter.foundError())
3231
return;
3332

34-
System.out.println("CTCLASS:" + ctClass.getSimpleName());
3533
context.reinitializeContext();
3634
if (visitedClasses.contains(ctClass.getQualifiedName()))
3735
return;

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@
44
import java.util.Arrays;
55
import java.util.List;
66
import java.util.Optional;
7+
8+
import org.apache.commons.lang3.NotImplementedException;
9+
710
import liquidjava.errors.ErrorEmitter;
811
import liquidjava.processor.context.*;
912
import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
@@ -53,7 +56,6 @@ public RefinementTypeChecker(Context context, Factory factory, ErrorEmitter erro
5356
super(context, factory, errorEmitter);
5457
otc = new OperationsChecker(this);
5558
mfc = new MethodsFunctionsChecker(this);
56-
System.out.println("In RefinementTypeChecker");
5759
}
5860

5961
// --------------------- Visitors -----------------------------------
@@ -221,7 +223,6 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignement) {
221223
checkAssignment(name, varDecl.getType(), ex, assignement.getAssignment(), assignement, varDecl);
222224

223225
} else if (ex instanceof CtFieldWrite) {
224-
System.out.println("Got field write: " + assignement);
225226
CtFieldWrite<?> fw = ((CtFieldWrite<?>) ex);
226227
CtFieldReference<?> cr = fw.getVariable();
227228
CtField<?> f = fw.getVariable().getDeclaration();
@@ -268,7 +269,8 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
268269
} else if (lit.getType().getQualifiedName().contentEquals("java.lang.String")) {
269270
// Only taking care of strings inside refinements
270271
} else {
271-
System.out.println(String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName()));
272+
throw new NotImplementedException(
273+
String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName()));
272274
}
273275
}
274276

@@ -386,7 +388,6 @@ public <R> void visitCtInvocation(CtInvocation<R> invocation) {
386388

387389
super.visitCtInvocation(invocation);
388390
mfc.getInvocationRefinements(invocation);
389-
System.out.println();
390391
}
391392

392393
@Override
@@ -503,7 +504,6 @@ public <T> void visitCtNewClass(CtNewClass<T> newClass) {
503504
}
504505

505506
super.visitCtNewClass(newClass);
506-
System.out.println("new class");
507507
}
508508

509509
// ############################### Inner Visitors

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -113,8 +113,7 @@ public void handleStateSetsFromAnnotation(CtElement element) {
113113
private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
114114
Optional<GhostFunction> og = createStateGhost(set, element);
115115
if (!og.isPresent()) {
116-
System.out.println("Error in creation of GhostFunction");
117-
assert false;
116+
throw new RuntimeException("Error in creation of GhostFunction");
118117
}
119118
GhostFunction g = og.get();
120119
context.addGhostFunction(g);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -56,12 +56,10 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, Stri
5656
return;
5757
}
5858

59-
// System.out.println(premises.toString() + "\n"+et.toString());
6059
try {
6160
smtChecking(premises, et);
6261
} catch (Exception e) {
6362
// To emit the message we use the constraints before the alias and state change
64-
System.out.println();
6563
printError(e, premisesBeforeChange, expectedType, element, map);
6664
}
6765
}
@@ -97,7 +95,8 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
9795
// printError(premises, expectedType, element, map, e.getMessage());
9896
}
9997

100-
System.out.println("premise: " + premises.toString() + "\nexpectation: " + et.toString());
98+
// System.out.println("premise: " + premises.toString() + "\nexpectation: " +
99+
// et.toString());
101100
return smtChecks(premises, et, p);
102101
}
103102

@@ -136,21 +135,21 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
136135
if (firstSi != null && lastSi != null) {
137136
cSMT = firstSi.clone();
138137
lastSi.setNext(new VCImplication(expectedType));
139-
printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType);
138+
// printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType);
140139
}
141140

142141
return cSMT; // firstSi != null ? firstSi : new VCImplication(new Predicate());
143142
}
144143

145144
private void addMap(RefinedVariable var, HashMap<String, PlacementInCode> map) {
146145
map.put(var.getName(), var.getPlacementInCode());
147-
// System.out.println();
148146
// if(var instanceof VariableInstance) {
149147
// VariableInstance vi = (VariableInstance) var;
150148
// if(vi.getParent().isPresent())
151149
// map.put(vi.getName(), vi.getParent().get().getName());
152150
// else if(instancePattern.matcher(var.getName()).matches()){
153-
// String result = var.getName().replaceAll("(_[0-9]+)$", "").replaceAll("^#", "");
151+
// String result = var.getName().replaceAll("(_[0-9]+)$", "").replaceAll("^#",
152+
// "");
154153
// map.put(var.getName(), result);
155154
// }
156155
// }else if(thisPattern.matcher(var.getName()).matches())
@@ -306,7 +305,6 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
306305
totalS = ci.toString().substring(targetL + 1);
307306
}
308307
s = "Method invocation " + totalS + " in:";
309-
System.out.println();
310308
}
311309

312310
Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@
33
import java.util.Arrays;
44
import java.util.List;
55
import java.util.Optional;
6+
7+
import org.apache.commons.lang3.NotImplementedException;
8+
69
import liquidjava.processor.context.RefinedFunction;
710
import liquidjava.processor.context.RefinedVariable;
811
import liquidjava.processor.context.Variable;
@@ -87,7 +90,7 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws Pars
8790
} else if (types.contains(type)) {
8891
operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper));
8992
} else {
90-
System.out.println("Literal type not implemented");
93+
throw new NotImplementedException("Literal type not implemented");
9194
}
9295
// TODO ADD TYPES
9396
}
@@ -128,7 +131,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
128131
}
129132
}
130133
} catch (ParentNotInitializedException e) {
131-
System.out.println("Parent not initialized");
134+
throw new RuntimeException("Parent not initialized");
132135
}
133136
}
134137

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
7676
Predicate argRef = arg.getRefinement().substituteVariable(arg.getName(), newName);
7777
Predicate superArgRef = superArg.getRefinement().substituteVariable(superArg.getName(), newName);
7878

79-
System.out.println(arg.getName() + " has ref " + argRef);
8079
if (argRef.isBooleanTrue()) {
81-
System.out.println(arg.getName() + " has ref boolean true");
8280
arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName()));
8381
} else {
8482
boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
@@ -100,7 +98,8 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct
10098
else {
10199
String name = String.format(tc.freshFormat, tc.getContext().getCounter());
102100
tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method);
103-
// functionRef might be stronger than superRef -> check (superRef <: functionRef)
101+
// functionRef might be stronger than superRef -> check (superRef <:
102+
// functionRef)
104103
functionRef = functionRef.substituteVariable(tc.WILD_VAR, name);
105104
superRef = superRef.substituteVariable(tc.WILD_VAR, name);
106105
for (String m : super2function.keySet())
@@ -152,16 +151,17 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
152151
tc.checkStateSMT(superConst, subConst, method,
153152
"FROM State from Superclass must be subtype of FROM State from Subclass");
154153
// boolean correct = tc.checkStateSMT(superConst, subConst, method);
155-
// if(!correct) ErrorPrinter.printError(method, subState.getFrom(), superState.getFrom());
156-
System.out.println("Came to checkStates hierarchy");
154+
// if(!correct) ErrorPrinter.printError(method, subState.getFrom(),
155+
// superState.getFrom());
157156

158157
superConst = matchVariableNames(tc.THIS, thisName, superState.getTo());
159158
subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction, subState.getTo());
160159
// toSub <: toSup <==> ToSub is sub type and toSup is expectedType
161160
tc.checkStateSMT(subConst, superConst, method,
162161
"TO State from Subclass must be subtype of TO State from Superclass");
163162
// boolean correct = tc.checkStateSMT(subConst, superConst, method);
164-
// if(!correct) ErrorPrinter.printError(method, subState.getTo(), superState.getTo());
163+
// if(!correct) ErrorPrinter.printError(method, subState.getTo(),
164+
// superState.getTo());
165165
}
166166
}
167167
}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -290,7 +290,6 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
290290
String stateChangeRefinementFrom = "true";
291291

292292
// extracting target from assignment
293-
System.out.println("Target for field writw: " + fw.getTarget());
294293

295294
// only works for things in form of this.field_name = 1
296295
// does not work thor thins like `void method(){otherMethod();}`

0 commit comments

Comments
 (0)