Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Carson Smith - GSoC Submission PR #54

Open
wants to merge 16 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion eclipse/run-JPF-symbc.launch
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">
<listEntry value="1"/>
</listAttribute>
<booleanAttribute key="org.eclipse.debug.core.appendEnvironmentVariables" value="false"/>
<mapAttribute key="org.eclipse.debug.core.environmentVariables">
<mapEntry key="LD_LIBRARY_PATH" value="/Users/corinapasareanu/workspace-isstac/jpf-symbc"/>
</mapAttribute>
Expand All @@ -25,4 +26,5 @@
<stringAttribute key="org.eclipse.jdt.launching.PROGRAM_ARGUMENTS" value="&quot;${resource_loc}&quot;"/>
<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="jpf-symbc"/>
<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx1024m -ea"/>
</launchConfiguration>
<stringAttribute key="org.eclipse.jdt.launching.WORKING_DIRECTORY" value="${workspace_loc:jpf-symbc/lib}"/>
</launchConfiguration>
9 changes: 9 additions & 0 deletions src/main/gov/nasa/jpf/symbc/arrays/ArrayConstraint.java
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
package gov.nasa.jpf.symbc.arrays;

import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.Comparator;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;

Expand Down Expand Up @@ -58,5 +59,13 @@ public ArrayConstraint not() {
}
}
}

//Carson Smith
public boolean accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
boolean result = visitor.visit(this);
visitor.postVisit(this);
return result;
}
}

1 change: 1 addition & 0 deletions src/main/gov/nasa/jpf/symbc/arrays/ArrayExpression.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
package gov.nasa.jpf.symbc.arrays;

import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.Expression;
import gov.nasa.jpf.symbc.numeric.IntegerConstant;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
Expand Down
9 changes: 9 additions & 0 deletions src/main/gov/nasa/jpf/symbc/arrays/RealArrayConstraint.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
package gov.nasa.jpf.symbc.arrays;

import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.Comparator;
import gov.nasa.jpf.symbc.numeric.RealExpression;

Expand Down Expand Up @@ -51,5 +52,13 @@ public RealArrayConstraint not() {
}
}
}

//Carson Smith
public boolean accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
boolean result = visitor.visit(this);
visitor.postVisit(this);
return result;
}
}

8 changes: 6 additions & 2 deletions src/main/gov/nasa/jpf/symbc/concolic/FunctionExpression.java
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,8 @@
package gov.nasa.jpf.symbc.concolic;
// support for arbitrary external functions

import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.Expression;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
import gov.nasa.jpf.symbc.numeric.PathCondition;
Expand Down Expand Up @@ -203,6 +204,9 @@ public int compareTo(Expression expr) {
}
}


@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
throw new RuntimeException("FunctionExpression - This isn't a supported expression type for the visitor system.");
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@


import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.Expression;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
import gov.nasa.jpf.symbc.string.StringExpression;
Expand Down Expand Up @@ -111,4 +112,9 @@ public int compareTo(Expression expr) {
return getClass().getCanonicalName().compareTo(expr.getClass().getCanonicalName());
}
}

@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
throw new RuntimeException("This isn't a supported expression type for the visitor system.");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@


import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor2;
import gov.nasa.jpf.symbc.numeric.RealExpression;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
import gov.nasa.jpf.symbc.numeric.Expression;
Expand Down Expand Up @@ -115,4 +116,9 @@ public int compareTo(Expression expr) {
return getClass().getCanonicalName().compareTo(expr.getClass().getCanonicalName());
}
}

@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
throw new RuntimeException("This isn't a supported expression type for the visitor system.");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@

package gov.nasa.jpf.symbc.numeric;

import java.util.Map;
import java.util.Map;

public class BinaryLinearIntegerExpression extends LinearIntegerExpression
{
Expand All @@ -58,6 +58,15 @@ public void accept(ConstraintExpressionVisitor visitor) {
left.accept(visitor);
right.accept(visitor);
visitor.postVisit(this);
}

//Carson Smith
@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
Object result = visitor.visit(this);
visitor.postVisit(this);
return result;
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,13 @@ public int compareTo(Expression expr) {
} else {
return getClass().getCanonicalName().compareTo(expr.getClass().getCanonicalName());
}
}

@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
Object result = visitor.visit(this);
visitor.postVisit(this);
return result;
}

}
8 changes: 8 additions & 0 deletions src/main/gov/nasa/jpf/symbc/numeric/BinaryRealExpression.java
Original file line number Diff line number Diff line change
Expand Up @@ -121,5 +121,13 @@ public int compareTo(Expression expr) {
} else {
return getClass().getCanonicalName().compareTo(expr.getClass().getCanonicalName());
}
}

@Override
public Object accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
Object result = visitor.visit(this);
visitor.postVisit(this);
return result;
}
}
13 changes: 12 additions & 1 deletion src/main/gov/nasa/jpf/symbc/numeric/Constraint.java
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@

import java.util.Map;

import gov.nasa.jpf.symbc.numeric.visitors.CollectVariableVisitor;
import gov.nasa.jpf.symbc.numeric.visitors.ProblemGeneralVisitor;

public abstract class Constraint implements Comparable<Constraint> {
private final Expression left;

Expand Down Expand Up @@ -168,13 +171,21 @@ public Constraint last() {
return c;
}

//JacoGeldenhuys
//JacoGeldenhuys - For use with GREEN
public void accept(ConstraintExpressionVisitor visitor) {
visitor.preVisit(this);
left.accept(visitor);
right.accept(visitor);
visitor.postVisit(this);
}

// Carson Smith - For use with GSoC changes.
public boolean accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
boolean result = visitor.visit(this);
visitor.postVisit(this);
return result;
}

public String prefix_notation() {
//return left.toString() + comp.toString() + right.toString()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +237,4 @@ public void postVisit(StringSymbolic expr) {
public void postVisit(SymbolicStringBuilder expr) {
}



}
107 changes: 107 additions & 0 deletions src/main/gov/nasa/jpf/symbc/numeric/ConstraintExpressionVisitor2.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
/*
* Copyright (C) 2014, United States Government, as represented by the
* Administrator of the National Aeronautics and Space Administration.
* All rights reserved.
*
* Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
* Version 2.0 (the "License"); you may not use this file except
* in compliance with the License. You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0.
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/

package gov.nasa.jpf.symbc.numeric;

import gov.nasa.jpf.symbc.arrays.ArrayConstraint;
import gov.nasa.jpf.symbc.arrays.RealArrayConstraint;

/**
* An extension of the previous visitor system created for GREEN solver integration
* set up for a more robust purpose of handling the functionality previously done by
* PCParser. All it changes about the previous system is the creation of literal
* visit() methods that return values explicitly upon being called. The calling of
* accept() has been moved to these visit methods for simplicity purposes.
*
* Not all methods have been moved over. As of now, only the methods needed to be moved
* have been moved since many of the preVisit() and postVisit() methods visit constraints
* or expressions that don't need visit() functionality to accomplish my initial goal.
*
* @author Carson Smith
*/
public abstract class ConstraintExpressionVisitor2 extends ConstraintExpressionVisitor {

/*--- CONSTRAINT VISITOR ROUTINES ---*/

public boolean visit(Constraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(LinearIntegerConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(NonLinearIntegerConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(RealConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(MixedConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(LogicalORLinearIntegerConstraints constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(ArrayConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public boolean visit(RealArrayConstraint constraint) {
throw new RuntimeException("Method needs to be Overloaded.");
}

/*--- EXPRESSION VISITOR ROUTINES ---*/

public Object visit(SymbolicInteger expr) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Double visit(RealConstant expr) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Object visit(SymbolicReal expr) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Object visit(MathRealExpression expr) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Object visit(BinaryLinearIntegerExpression expression) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Object visit(BinaryNonLinearIntegerExpression expression) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Object visit(BinaryRealExpression expression) {
throw new RuntimeException("Method needs to be Overloaded.");
}

public Long visit(IntegerConstant integerConstant) {
throw new RuntimeException("Method needs to be Overloaded.");
}

}
4 changes: 4 additions & 0 deletions src/main/gov/nasa/jpf/symbc/numeric/Expression.java
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@


import java.util.Map;

import gov.nasa.jpf.symbc.numeric.visitors.ProblemGeneralVisitor;

import java.util.LinkedList;


Expand All @@ -47,6 +50,7 @@ public abstract class Expression implements Comparable<Expression> {
public abstract String stringPC();
public abstract void getVarsVals(Map<String,Object> varsVals);
public abstract void accept(ConstraintExpressionVisitor visitor);
// public abstract Object accept(ConstraintExpressionVisitor2 visitor);
public String prefix_notation() {throw new RuntimeException("error printing");}

}
12 changes: 11 additions & 1 deletion src/main/gov/nasa/jpf/symbc/numeric/IntegerConstant.java
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,9 @@

package gov.nasa.jpf.symbc.numeric;

import java.util.Map;
import java.util.Map;

import gov.nasa.jpf.symbc.numeric.visitors.ProblemGeneralVisitor;

import static gov.nasa.jpf.symbc.numeric.Operator.*;

Expand Down Expand Up @@ -307,6 +309,14 @@ public void getVarsVals(Map<String,Object> varsVals) {}
public void accept(ConstraintExpressionVisitor visitor) {
visitor.preVisit(this);
visitor.postVisit(this);
}

//Carson Smith
public Object accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
Object result = visitor.visit(this);
visitor.postVisit(this);
return result;
}

@Override
Expand Down
3 changes: 2 additions & 1 deletion src/main/gov/nasa/jpf/symbc/numeric/IntegerExpression.java
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,8 @@ public char solutionChar() {
throw new RuntimeException( "## Error: Expression Solution request Error: " + this);
}


public abstract Object accept(ConstraintExpressionVisitor2 visitor);

//protected void finalize() throws Throwable {
// System.out.println("Finalized LIExp -> " + this);
//}
Expand Down
11 changes: 10 additions & 1 deletion src/main/gov/nasa/jpf/symbc/numeric/LinearIntegerConstraint.java
Original file line number Diff line number Diff line change
Expand Up @@ -61,5 +61,14 @@ public IntegerExpression getRight() {
@Override
public LinearIntegerConstraint not() {
return new LinearIntegerConstraint(getLeft(), getComparator().not(), getRight());
}
}

//Carson Smith
@Override
public boolean accept(ConstraintExpressionVisitor2 visitor) {
visitor.preVisit(this);
boolean result = visitor.visit(this);
visitor.postVisit(this);
return result;
}
}
Loading