public class SMTObjTranslator extends 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 String |
ANY_SORT |
private static String |
ARR_FUNCTION_NAME |
static String |
BINT_SORT |
private Sort |
boolSort |
private List<SMTTerm> |
castAssertions
Assertions regarding Any2Object, Any2BInt, Object2Any, etc.
|
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 String |
CLASS_INVARIANT |
private TypeHierarchy |
concreteHierarchy
The concrete java type hierarchy obtained by contracting all abstract
types from the java type hierarchy.
|
private static String |
CREATED_FIELD_NAME |
static String |
ELEMENTOF |
private SMTFunction |
elementOfFunction
The elementOf predicate.
|
private static String |
EMPTY_CONSTANT |
private SMTTerm |
emptyConstant
The empty constant.
|
private Set<Sort> |
extendedJavaSorts
The java sorts that we encountered in the proof obligation and all their
supersorts.
|
static String |
FIELD_SORT |
private Sort |
fieldSort |
private Map<String,Sort> |
fieldSorts
Stores the sort of each field.
|
private List<String> |
functionDefinitionOrder
Stores the order in which the function definitions should be written in
the SMT file.
|
private Map<String,SMTFunction> |
functions
The functions that we declare are stored here.
|
private 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 String |
HEAP_SORT |
private Sort |
heapSort |
private Sort |
integerSort |
private Set<Sort> |
javaSorts
The java sorts that we have encountered in the proof obligation.
|
static String |
LENGTH |
static String |
LOCSET_SORT |
private Sort |
locsetSort |
private static String |
NULL_CONSTANT |
private SMTTerm |
nullConstant
The null constant.
|
static String |
OBJECT_SORT |
private Sort |
objectSort |
private Map<Operator,SMTTermMultOp.Op> |
opTable
Mapps some basic KeY operators to their equivalent built in operators.
|
private Set<SMTTerm> |
overflowGuards
Overflow guards for ground terms.
|
private List<SMTTermVariable> |
quantifiedVariables
List of current quantified variables.
|
private ModelExtractor |
query
The query that will extract the counterexample from the z3 solver.
|
private static String |
SELECT |
private SMTFunction |
selectFunction
The select function.
|
private static String |
SELF |
private static String |
SEQ_EMPTY |
static String |
SEQ_GET |
static String |
SEQ_LEN |
private static String |
SEQ_OUTSIDE |
static 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 Map<SMTSort,SMTTermNumber> |
sortNumbers
Type bits for the SMTSorts that are subtypes of any.
|
private Map<String,SMTSort> |
sorts
The SMT sorts used in this translation.
|
private TypeHierarchy |
thierarchy
The java type hierarchy.
|
private Map<String,SMTTerm> |
typeAssertions
Assertions for specifying the java type hierarchy.
|
private KeYJavaType |
typeOfClassUnderTest
Info regarding the selected proof.
|
private Map<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 String |
WELL_FORMED_NAME |
private List<SMTTerm> |
wellFormedAssertions
Assertions regarding the wellformed function.
|
private SMTFunction |
wellformedFunction
The wellformed predicate.
|
Constructor and Description |
---|
SMTObjTranslator(SMTSettings settings,
Services services,
KeYJavaType typeOfClassUnderTest) |
Modifier and Type | Method and Description |
---|---|
private SMTTerm |
addAssertionForField(String fieldName)
Create assertion which states that a field is of the correct type.
|
private void |
addCastAssertions(SMTSort source,
SMTSort target,
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(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(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 String |
getCastFunctionName(SMTSort source,
SMTSort target)
Returns the name of a cast function determined by the specified source
and target sorts.
|
private String |
getCastFunctionName(Sort castTarget) |
private SMTFunction |
getExactInstanceFunction(Sort s)
Creates the exactInstance predicate for a sort s.
|
static String |
getExactInstanceName(String sortName) |
Collection<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(String sortName) |
static String |
getTypePredicateName(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(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.
|
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 String |
varName(char c) |
public static final String CLASS_INVARIANT
public static final String LENGTH
private static final String WELL_FORMED_NAME
public static final String BINT_SORT
public static final String HEAP_SORT
public static final String FIELD_SORT
public static final String LOCSET_SORT
public static final String OBJECT_SORT
public static final String ANY_SORT
public static final String SEQ_SORT
private static final String NULL_CONSTANT
private static final String EMPTY_CONSTANT
public static final String ELEMENTOF
private static final String SELECT
private static final String CREATED_FIELD_NAME
private static final String ARR_FUNCTION_NAME
private static final String SEQ_EMPTY
private static final String SEQ_OUTSIDE
public static final String SEQ_GET
public static final String SEQ_LEN
private static final String SELF
private Map<Operator,SMTTermMultOp.Op> opTable
private int varNr
private SMTSettings settings
private Services services
private final KeYJavaType typeOfClassUnderTest
private List<SMTTerm> castAssertions
private List<SMTTerm> wellFormedAssertions
private SMTFunction selectFunction
private SMTFunction wellformedFunction
private Map<String,SMTSort> sorts
private Map<SMTSort,SMTTermNumber> sortNumbers
private Map<String,Sort> fieldSorts
private Map<String,SMTFunction> typePredicates
private Map<String,SMTTerm> typeAssertions
private List<SMTTerm> functionTypeAssertions
private Set<Sort> javaSorts
private Set<Sort> extendedJavaSorts
private Map<String,SMTFunction> functions
private List<String> functionDefinitionOrder
private SMTTerm nullConstant
private SMTTerm emptyConstant
private List<SMTTermVariable> quantifiedVariables
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 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(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 String getCastFunctionName(SMTSort source, SMTSort target)
source
- target
- private SMTFunction createCastFunction(SMTSort source, SMTSort target)
source
- target
- private void addCastAssertions(SMTSort source, SMTSort target, 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(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 String varName(char c)
private void addTypeAssertion(SMTFunction f, SMTFunction tp)
f
- tp
- private SMTFunction getTypePredicate(String sortName)
sortName
- private boolean appearsInPO(Sort s)
s
- private void addTypePredicate(Sort s)
s
- private void forceAddTypePredicate(Sort s)
private SMTFunction translateConstant(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 SMTFunction getExactInstanceFunction(Sort s) throws IllegalFormulaException
s
- IllegalFormulaException
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 Collection<Throwable> getExceptionsOfTacletTranslation()
SMTTranslator
getExceptionsOfTacletTranslation
in interface SMTTranslator