public class OracleGenerator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
AND |
private java.util.Set<Term> |
constants |
private static java.lang.String |
EQUALS |
private java.util.Set<java.lang.String> |
falsePredicates |
private java.util.Map<Sort,OracleMethod> |
invariants |
private java.util.List<OracleVariable> |
methodArgs |
private java.util.HashMap<Operator,java.lang.String> |
ops |
private static java.lang.String |
OR |
private java.util.Set<OracleMethod> |
oracleMethods |
static java.lang.String |
PRE_STRING |
private java.util.Set<java.lang.String> |
prestateTerms |
private java.util.List<OracleVariable> |
quantifiedVariables |
private ReflectionClassCreator |
rflCreator |
private Services |
services |
private java.util.Set<java.lang.String> |
truePredicates |
private boolean |
useRFL |
private static int |
varNum |
Constructor and Description |
---|
OracleGenerator(Services services,
ReflectionClassCreator rflCreator,
boolean useRFL) |
Modifier and Type | Method and Description |
---|---|
private static OracleTerm |
and(OracleTerm left,
OracleTerm right) |
private OracleMethod |
createDummyInvariant(Sort s) |
private OracleMethod |
createDummyOracleMethod(ProgramMethod pm) |
private java.lang.String |
createExistsBody(QuantifiableVariable qv,
java.lang.String setName,
OracleTerm cond) |
private java.lang.String |
createForallBody(QuantifiableVariable qv,
java.lang.String setName,
OracleUnaryTerm neg) |
private OracleMethod |
createIfThenElseMethod(Term term,
boolean initialSelect) |
private OracleMethod |
createInvariantMethod(Sort s,
boolean initialSelect) |
private java.lang.String |
createLocationString(OracleTerm heapTerm,
OracleTerm objTerm,
java.lang.String fieldName,
Sort objSort,
Sort fieldSort,
boolean initialSelect) |
private OracleMethod |
createQuantifierMethod(Term term,
boolean initialSelect) |
private Sort |
createSetSort(java.lang.String inner) |
private static OracleTerm |
eq(OracleTerm left,
OracleTerm right) |
private void |
findConstants(java.util.Set<Term> constants,
Term term) |
static java.lang.String |
generateMethodName() |
OracleTerm |
generateOracle(Term term,
boolean initialSelect) |
OracleMethod |
generateOracleMethod(Term term) |
java.util.Set<Term> |
getConstants() |
private java.util.Set<Term> |
getConstants(Term t) |
java.util.List<OracleVariable> |
getMethodArgs() |
private java.util.List<OracleVariable> |
getMethodArgs(Term t) |
OracleLocationSet |
getOracleLocationSet(Term modifierset) |
java.util.Set<OracleMethod> |
getOracleMethods() |
java.util.Set<java.lang.String> |
getPrestateTerms() |
private java.lang.String |
getSetName(Sort s) |
private java.lang.String |
getSortInvName(Sort s) |
private void |
initFalse() |
private void |
initOps() |
private void |
initTrue() |
private boolean |
isFalseConstant(Operator o) |
private boolean |
isPreHeap(OracleTerm heapTerm) |
private boolean |
isRelevantConstant(Term c) |
private boolean |
isTrueConstant(Operator o) |
private static OracleTerm |
neg(OracleTerm t) |
private static OracleTerm |
or(OracleTerm left,
OracleTerm right) |
private OracleTerm |
translateFunction(Term term,
boolean initialSelect) |
private OracleTerm |
translateQuery(Term term,
boolean initialSelect,
Operator op) |
private OracleTerm |
translateSelect(Term term,
boolean initialSelect) |
private static final java.lang.String OR
private static final java.lang.String AND
private static final java.lang.String EQUALS
private Services services
private static int varNum
private java.util.HashMap<Operator,java.lang.String> ops
private java.util.Set<OracleMethod> oracleMethods
private java.util.List<OracleVariable> quantifiedVariables
private java.util.Set<java.lang.String> truePredicates
private java.util.Set<java.lang.String> falsePredicates
private java.util.Set<java.lang.String> prestateTerms
private java.util.Map<Sort,OracleMethod> invariants
private java.util.List<OracleVariable> methodArgs
private java.util.Set<Term> constants
private ReflectionClassCreator rflCreator
private boolean useRFL
public static final java.lang.String PRE_STRING
public OracleGenerator(Services services, ReflectionClassCreator rflCreator, boolean useRFL)
private void initTrue()
private void initFalse()
private void initOps()
public OracleMethod generateOracleMethod(Term term)
public OracleLocationSet getOracleLocationSet(Term modifierset)
public java.util.List<OracleVariable> getMethodArgs()
public java.util.Set<OracleMethod> getOracleMethods()
private boolean isRelevantConstant(Term c)
public java.util.Set<Term> getConstants()
private java.util.List<OracleVariable> getMethodArgs(Term t)
private Sort createSetSort(java.lang.String inner)
public OracleTerm generateOracle(Term term, boolean initialSelect)
private OracleTerm translateFunction(Term term, boolean initialSelect)
private OracleTerm translateQuery(Term term, boolean initialSelect, Operator op)
private OracleMethod createDummyOracleMethod(ProgramMethod pm)
private OracleTerm translateSelect(Term term, boolean initialSelect)
private java.lang.String createLocationString(OracleTerm heapTerm, OracleTerm objTerm, java.lang.String fieldName, Sort objSort, Sort fieldSort, boolean initialSelect)
private boolean isPreHeap(OracleTerm heapTerm)
private boolean isTrueConstant(Operator o)
private boolean isFalseConstant(Operator o)
public static java.lang.String generateMethodName()
private java.lang.String getSortInvName(Sort s)
private OracleMethod createDummyInvariant(Sort s)
private OracleMethod createInvariantMethod(Sort s, boolean initialSelect)
private OracleMethod createIfThenElseMethod(Term term, boolean initialSelect)
public java.util.Set<java.lang.String> getPrestateTerms()
private java.lang.String getSetName(Sort s)
private OracleMethod createQuantifierMethod(Term term, boolean initialSelect)
private java.lang.String createForallBody(QuantifiableVariable qv, java.lang.String setName, OracleUnaryTerm neg)
private java.lang.String createExistsBody(QuantifiableVariable qv, java.lang.String setName, OracleTerm cond)
private static OracleTerm neg(OracleTerm t)
private static OracleTerm eq(OracleTerm left, OracleTerm right)
private static OracleTerm and(OracleTerm left, OracleTerm right)
private static OracleTerm or(OracleTerm left, OracleTerm right)