public class SMTObjTranslator extends java.lang.Object implements SMTTranslator
Modifier and Type | Class and Description |
---|---|
class |
SMTObjTranslator.ConstantCounter
Class for counting constants of different types appearing in the proof
obligation.
|
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
ANY_SORT |
private static java.lang.String |
ARR_FUNCTION_NAME |
static java.lang.String |
BINT_SORT |
private Sort |
boolSort |
private java.util.List<SMTTerm> |
castAssertions
Assertions regarding Any2Object, Any2BInt, Object2Any, etc. functions.
|
private SMTObjTranslator.ConstantCounter |
cc
The constant counter counts the number of heap and field constants in
order to determine the size of their sorts.
|
static java.lang.String |
CLASS_INVARIANT |
private TypeHierarchy |
concreteHierarchy
The concrete java type hierarchy obtained by contracting all abstract
types from the java type hierarchy.
|
private static java.lang.String |
CREATED_FIELD_NAME |
static java.lang.String |
ELEMENTOF |
private SMTFunction |
elementOfFunction
The elementOf predicate.
|
private static java.lang.String |
EMPTY_CONSTANT |
private SMTTerm |
emptyConstant
The empty constant.
|
private java.util.Set<Sort> |
extendedJavaSorts
The java sorts that we encountered in the proof obligation and all their
supersorts.
|
static java.lang.String |
FIELD_SORT |
private Sort |
fieldSort |
private java.util.Map<java.lang.String,Sort> |
fieldSorts
Stores the sort of each field.
|
private java.util.List<java.lang.String> |
functionDefinitionOrder
Stores the order in which the function definitions should be written in
the SMT file.
|
private java.util.Map<java.lang.String,SMTFunction> |
functions
The functions that we declare are stored here.
|
private java.util.List<SMTTerm> |
functionTypeAssertions
Assertions regarding the return type of functions.
|
private static boolean |
guardOverflow
If true, guards for preventing integer overflows will be added.
|
static java.lang.String |
HEAP_SORT |
private Sort |
heapSort |
private Sort |
integerSort |
private java.util.Set<Sort> |
javaSorts
The java sorts that we have encountered in the proof obligation.
|
static java.lang.String |
LENGTH |
static java.lang.String |
LOCSET_SORT |
private Sort |
locsetSort |
private static java.lang.String |
NULL_CONSTANT |
private SMTTerm |
nullConstant
The null constant.
|
static java.lang.String |
OBJECT_SORT |
private Sort |
objectSort |
private java.util.Map<Operator,SMTTermMultOp.Op> |
opTable
Mapps some basic KeY operators to their equivalent built in operators.
|
private java.util.Set<SMTTerm> |
overflowGuards
Overflow guards for ground terms.
|
private java.util.List<SMTTermVariable> |
quantifiedVariables
List of current quantified variables.
|
private ModelExtractor |
query
The query that will extract the counterexample from the z3 solver.
|
private static java.lang.String |
SELECT |
private SMTFunction |
selectFunction
The select function. select : Heap x Object x Field -> Any
|
private static java.lang.String |
SELF |
private static java.lang.String |
SEQ_EMPTY |
static java.lang.String |
SEQ_GET |
static java.lang.String |
SEQ_LEN |
private static java.lang.String |
SEQ_OUTSIDE |
static java.lang.String |
SEQ_SORT |
private Sort |
seqSort |
private Services |
services
KeY services provide a lot of useful stuff.
|
private SMTSettings |
settings
The SMT translation settings.
|
private java.util.Map<SMTSort,SMTTermNumber> |
sortNumbers
Type bits for the SMTSorts that are subtypes of any.
|
private java.util.Map<java.lang.String,SMTSort> |
sorts
The SMT sorts used in this translation.
|
private TypeHierarchy |
thierarchy
The java type hierarchy.
|
private java.util.Map<java.lang.String,SMTTerm> |
typeAssertions
Assertions for specifying the java type hierarchy.
|
private KeYJavaType |
typeOfClassUnderTest
Info regarding the selected proof.
|
private java.util.Map<java.lang.String,SMTFunction> |
typePredicates
Type predicates used to specify the java type hierarchy.
|
private ProblemTypeInformation |
types
Types information needed by the counterexample formatter.
|
private int |
varNr |
private static java.lang.String |
WELL_FORMED_NAME |
private java.util.List<SMTTerm> |
wellFormedAssertions
Assertions regarding the wellformed function.
|
private SMTFunction |
wellformedFunction
The wellformed predicate. wellformed : Heap -> Bool
|
Constructor and Description |
---|
SMTObjTranslator(SMTSettings settings,
Services services,
KeYJavaType typeOfClassUnderTest) |
Modifier and Type | Method and Description |
---|---|
private SMTTerm |
addAssertionForField(java.lang.String fieldName)
Create assertion which states that a field is of the correct type.
|
private void |
addCastAssertions(SMTSort source,
SMTSort target,
java.lang.String id)
Adds the necessary assertions for a cast function
|
private void |
addCastFunctionAssertions(Sort castTarget)
Adds the necessary assertions for the cast function for the castTarget
sort.
|
private void |
addSingleSort(java.util.Set<Sort> sorts,
Sort s) |
private void |
addTypeAssertion(SMTFunction f,
SMTFunction tp)
Generates an assertion which states that the function f is of type
specified by the type predicate tp.
|
private void |
addTypeConstarints(Sort s)
Generates the type assertions for the java reference type s.
|
private void |
addTypePredicate(Sort s)
Creates a type predicate for the sort s if acceptable.
|
private boolean |
appearsInPO(Sort s) |
private SMTTerm |
call(SMTFunction function,
ImmutableArray<Term> subs)
Creates an SMTTermCall using the given function and arguments.
|
private SMTTerm |
castTermIfNecessary(SMTTerm term,
SMTSort target)
Casts a term to the specified sort, if the term is not already of that
sort.
|
private void |
createArrFunction()
Creates the arr function.
|
private SMTFunction |
createCastFunction(SMTSort source,
SMTSort target)
Creates a function which casts a term from the source sort tot the target
sort.
|
private SMTFunction |
createClassInvariantFunction()
Creates the class invariant function.
|
private void |
createCreatedConstant()
Create the created field constant.
|
private SMTFunction |
createElementOfFunction()
Creates the elementOf function.
|
private SMTTerm |
createEmptyConstant()
Creates the empty constant.
|
private SMTFunction |
createExactInstanceDefinition(Sort sort)
Creates the exactInstance function assertion(definition for final
classes) for sort s.
|
private SMTFunction |
createLengthFunction()
Creates the length function.
|
private SMTTerm |
createNullConstant()
Creates the null constant.
|
private SMTFunction |
createSelectFunction()
Creates the select function.
|
private SMTFunction |
createSelfObject() |
private void |
createSeqConstantsAndAssertions()
Creates the necessary sequence functions and assertions.
|
private void |
createSpecialFunctions()
Creates some special constant functions, which are used in every
translation.
|
private SMTFunction |
createWellFormedFunction()
Creates the wellformed function.
|
private void |
findSorts(java.util.Set<Sort> sorts,
Term term)
Recursively finds all sorts in a term
|
private void |
forceAddTypePredicate(Sort s) |
private void |
generateFieldFunctionDefinitions()
Creates an SMT constant for each named field pointing to a distinct
value.
|
private void |
generateLengthAssertions()
Creates assertion which states that the length of each object is greater
than or equal to 0.
|
private void |
generateTypeConstraints()
Generates the necessary assertions for specifying the type hierarchy.
|
private void |
generateWellFormedAssertions()
Creates the wellformed function definition.
|
private SMTFunction |
getCastFunction(SMTSort source,
SMTSort target)
Return a function which casts a term from the source sort to the target
sort.
|
private SMTFunction |
getCastFunction(Sort castTarget)
Creates a reference type cast function for the castTarget type.
|
private java.lang.String |
getCastFunctionName(SMTSort source,
SMTSort target)
Returns the name of a cast function determined by the specified source
and target sorts.
|
private java.lang.String |
getCastFunctionName(Sort castTarget) |
private SMTFunction |
getExactInstanceFunction(Sort s)
Creates the exactInstance predicate for a sort s.
|
static java.lang.String |
getExactInstanceName(java.lang.String sortName) |
java.util.Collection<java.lang.Throwable> |
getExceptionsOfTacletTranslation()
Returns all exceptions that have occurred while translating the taclets.
|
private SMTFunction |
getIsFunction(SMTSort sort)
Creates a function for checking if the given sort is the actual sort of
an Any value.
|
ModelExtractor |
getQuery() |
private SMTFunction |
getTypePredicate(java.lang.String sortName) |
static java.lang.String |
getTypePredicateName(java.lang.String id) |
ProblemTypeInformation |
getTypes() |
private void |
initOpTable()
Fills the operator table.
|
private void |
initSMTSorts()
Create the needed SMT sorts.
|
private void |
initSorts()
Get special KeY sorts that we need.
|
private boolean |
isFalseConstant(Operator o,
Services s) |
private boolean |
isFinal(Sort s) |
private boolean |
isInterface(Sort s) |
private boolean |
isTrueConstant(Operator o,
Services s) |
private SMTTerm |
translateCall(Function fun,
ImmutableArray<Term> subs)
Translates a function call of function f with argument subs.
|
private SMTFunction |
translateConstant(java.lang.String id,
Sort s)
Creates an SMT constant with the specified id and sort.
|
SMTFile |
translateProblem(Term problem)
Translates a KeY problem into a SMTFile.
|
java.lang.StringBuffer |
translateProblem(Term problem,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
private SMTSort |
translateSort(Sort s)
Translates a KeY sort to an SMT sort.
|
SMTTerm |
translateTerm(Term term)
Translates a KeY term to an SMT term.
|
private SMTTermVariable |
translateVariable(QuantifiableVariable q)
Translates a quantified variable.
|
private java.lang.String |
varName(char c) |
public static final java.lang.String CLASS_INVARIANT
public static final java.lang.String LENGTH
private static final java.lang.String WELL_FORMED_NAME
public static final java.lang.String BINT_SORT
public static final java.lang.String HEAP_SORT
public static final java.lang.String FIELD_SORT
public static final java.lang.String LOCSET_SORT
public static final java.lang.String OBJECT_SORT
public static final java.lang.String ANY_SORT
public static final java.lang.String SEQ_SORT
private static final java.lang.String NULL_CONSTANT
private static final java.lang.String EMPTY_CONSTANT
public static final java.lang.String ELEMENTOF
private static final java.lang.String SELECT
private static final java.lang.String CREATED_FIELD_NAME
private static final java.lang.String ARR_FUNCTION_NAME
private static final java.lang.String SEQ_EMPTY
private static final java.lang.String SEQ_OUTSIDE
public static final java.lang.String SEQ_GET
public static final java.lang.String SEQ_LEN
private static final java.lang.String SELF
private java.util.Map<Operator,SMTTermMultOp.Op> opTable
private int varNr
private SMTSettings settings
private Services services
private final KeYJavaType typeOfClassUnderTest
private java.util.List<SMTTerm> castAssertions
private java.util.List<SMTTerm> wellFormedAssertions
private SMTFunction selectFunction
private SMTFunction wellformedFunction
private java.util.Map<java.lang.String,SMTSort> sorts
private java.util.Map<SMTSort,SMTTermNumber> sortNumbers
private java.util.Map<java.lang.String,Sort> fieldSorts
private java.util.Map<java.lang.String,SMTFunction> typePredicates
private java.util.Map<java.lang.String,SMTTerm> typeAssertions
private java.util.List<SMTTerm> functionTypeAssertions
private java.util.Set<Sort> javaSorts
private java.util.Set<Sort> extendedJavaSorts
private java.util.Map<java.lang.String,SMTFunction> functions
private java.util.List<java.lang.String> functionDefinitionOrder
private SMTTerm nullConstant
private SMTTerm emptyConstant
private java.util.List<SMTTermVariable> quantifiedVariables
private java.util.Set<SMTTerm> overflowGuards
private TypeHierarchy thierarchy
private TypeHierarchy concreteHierarchy
private ProblemTypeInformation types
private ModelExtractor query
private Sort integerSort
private Sort heapSort
private Sort fieldSort
private Sort locsetSort
private Sort boolSort
private Sort seqSort
private Sort objectSort
private SMTFunction elementOfFunction
private SMTObjTranslator.ConstantCounter cc
private static boolean guardOverflow
public SMTObjTranslator(SMTSettings settings, Services services, KeYJavaType typeOfClassUnderTest)
private void createSpecialFunctions()
public ProblemTypeInformation getTypes()
private void createArrFunction()
private SMTFunction createSelfObject()
private SMTFunction createSelectFunction()
private SMTFunction createElementOfFunction()
private SMTFunction createLengthFunction()
private SMTFunction createWellFormedFunction()
private void initOpTable()
private void initSorts()
private void initSMTSorts()
public java.lang.StringBuffer translateProblem(Term problem, Services services, SMTSettings settings) throws IllegalFormulaException
SMTTranslator
translate(Term t, Services services)
is that assumptions
will be added.translateProblem
in interface SMTTranslator
problem
- the problem to be translated.IllegalFormulaException
public ModelExtractor getQuery()
private SMTTerm createNullConstant()
private void createSeqConstantsAndAssertions()
private SMTTerm createEmptyConstant()
private void generateLengthAssertions()
private void generateFieldFunctionDefinitions()
private void generateWellFormedAssertions() throws IllegalFormulaException
IllegalFormulaException
private void createCreatedConstant()
private SMTTerm addAssertionForField(java.lang.String fieldName) throws IllegalFormulaException
fieldName
- IllegalFormulaException
private SMTTerm castTermIfNecessary(SMTTerm term, SMTSort target)
term
- the term to be castedtarget
- the sort to which the term must be castedprivate SMTFunction getCastFunction(SMTSort source, SMTSort target)
source
- target
- private java.lang.String getCastFunctionName(SMTSort source, SMTSort target)
source
- target
- private SMTFunction createCastFunction(SMTSort source, SMTSort target)
source
- target
- private void addCastAssertions(SMTSort source, SMTSort target, java.lang.String id)
source
- source sort of the cast functiontarget
- target sort of the cast functionid
- key where the cast function can be found in the function tableprivate void findSorts(java.util.Set<Sort> sorts, Term term)
sorts
- list of accumulated sortsterm
- the term where we look for the sortspublic SMTFile translateProblem(Term problem) throws IllegalFormulaException
problem
- The KeY proof obligation.IllegalFormulaException
public SMTTerm translateTerm(Term term) throws IllegalFormulaException
term
- the KeY term.IllegalFormulaException
private SMTTermVariable translateVariable(QuantifiableVariable q) throws IllegalFormulaException
q
- IllegalFormulaException
private SMTSort translateSort(Sort s) throws IllegalFormulaException
s
- IllegalFormulaException
private void generateTypeConstraints() throws IllegalFormulaException
IllegalFormulaException
private void addTypeConstarints(Sort s) throws IllegalFormulaException
s
- IllegalFormulaException
private boolean isFinal(Sort s)
private java.lang.String varName(char c)
private void addTypeAssertion(SMTFunction f, SMTFunction tp)
f
- tp
- private SMTFunction getTypePredicate(java.lang.String sortName)
sortName
- public static java.lang.String getTypePredicateName(java.lang.String id)
private boolean appearsInPO(Sort s)
s
- private void addTypePredicate(Sort s)
s
- private void forceAddTypePredicate(Sort s)
private SMTFunction translateConstant(java.lang.String id, Sort s) throws IllegalFormulaException
id
- s
- IllegalFormulaException
private SMTTerm translateCall(Function fun, ImmutableArray<Term> subs) throws IllegalFormulaException
fun
- subs
- IllegalFormulaException
private SMTFunction createClassInvariantFunction()
private SMTFunction getCastFunction(Sort castTarget) throws IllegalFormulaException
castTarget
- IllegalFormulaException
private void addCastFunctionAssertions(Sort castTarget)
castTarget
- private java.lang.String getCastFunctionName(Sort castTarget)
private SMTFunction getExactInstanceFunction(Sort s) throws IllegalFormulaException
s
- IllegalFormulaException
public static java.lang.String getExactInstanceName(java.lang.String sortName)
private boolean isInterface(Sort s)
s
- private SMTFunction createExactInstanceDefinition(Sort sort)
sort
- private SMTFunction getIsFunction(SMTSort sort)
sort
- private SMTTerm call(SMTFunction function, ImmutableArray<Term> subs) throws IllegalFormulaException
function
- subs
- IllegalFormulaException
public java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
SMTTranslator
getExceptionsOfTacletTranslation
in interface SMTTranslator