public class Model
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private java.util.Map<java.lang.String,java.lang.String> |
constants
Maps constant names to constant values.
|
private boolean |
empty
marks an empty model
|
private java.util.List<Heap> |
heaps
List of heaps.
|
private java.util.List<LocationSet> |
locsets
List of location sets.
|
private java.util.Map<java.lang.String,java.lang.String> |
reversedConstants
Maps constant values to constant names.
|
private java.util.List<Sequence> |
sequences
List of sequences.
|
private ProblemTypeInformation |
types
Type information from the SMT specification.
|
Constructor and Description |
---|
Model()
creates an empty SMT model
|
Modifier and Type | Method and Description |
---|---|
void |
addAliases()
For all values it adds the names of the constants which have the same
values.
|
void |
addConstant(java.lang.String key,
java.lang.String value)
Adds a constant to the model.
|
void |
addHeap(Heap e)
Adds a heap to the model.
|
void |
addLocationSet(LocationSet e)
Adds a location set to the model.
|
void |
addSequence(Sequence s)
Adds a sequence set to the model.
|
private java.util.Map<java.lang.Integer,java.lang.String> |
extractArrayValuesFor(ObjectVal o)
extracts all array values for the specified object
|
private java.util.Map<java.lang.String,java.lang.String> |
extractFieldValuesFor(ObjectVal o)
extracts all field values for the specified object
|
private java.util.Map<java.lang.String,java.lang.String> |
extractFunctionValuesFor(ObjectVal o)
extracts all function values for the specified object
|
private void |
fillReversedTable()
Fills the reversed constants table.
|
ObjectVal |
findObject(java.lang.String ref)
finds the object the ref parameter is referring to
|
private java.lang.String |
formatAny(java.lang.String val,
SMTSort s)
Transforms a binary value of an any to a human readable form: #sn, where
s is the first letter of the actual sort name and n is the decimal value
of corresponding to the any value after the removal of the three type
bits and the fill up bits.
|
private java.lang.String |
getAliasedName(java.lang.String original)
returns an alias for the given name
|
java.util.Map<java.lang.String,java.lang.String> |
getConstants()
returns map from constant names to constant values
|
java.util.List<Heap> |
getHeaps() |
java.util.List<LocationSet> |
getLocsets() |
java.util.Set<ObjectVal> |
getNecessaryPrestateObjects(java.lang.String location)
returns set of necessary prestate objects
|
ObjectVal |
getObject(java.lang.String name,
Heap heap)
returns the object of the given name found in the heap
|
java.util.Set<ObjectVal> |
getReachableObjects(java.lang.String name,
Heap heap)
returns all objects reachable from the specified one in the fiven heap
|
java.util.List<Sequence> |
getSequences() |
ProblemTypeInformation |
getTypes() |
boolean |
isEmpty()
returns true if the model is empty
|
java.util.Set<ObjectVal> |
pointsTo(java.lang.String name,
Heap heap)
set of objects the specified object points to
|
java.lang.String |
processAnyValue(java.lang.String val)
Transforms a binary value of an any to a human readable form: #sn, where
s is the first letter of the actual sort name and n is the decimal value
of corresponding to the any value after the removal of the three type
bits and the fill up bits.
|
void |
processArrayValues()
Transforms the values of array fields of objects from binary/hexidecimal
to human readable form.
|
void |
processConstantsAndFieldValues()
Transforms the values of constants and object fields from
binary/hexadecimal to a human readable from.
|
java.lang.String |
processConstantValue(java.lang.String val,
SMTSort s)
Transforms a constant value from binary/hexadecimal form to a human
redable form.
|
private void |
processLocSetNames()
Rewrites the values of location sets from binary/hexadecimal to a human
readable form.
|
private java.lang.String |
processObjectID(java.lang.String objectID)
Transforms an Object id from binary form to #on, where n is a decimal
number.
|
void |
processObjectNames()
Rewrite the object names from binary/hexadecimal to a human readable
form.
|
private java.lang.String |
processSeqID(java.lang.String sequenceID)
Transforms a sequence id from binary form to #sn, where n is a decimal
number.
|
void |
processSequenceNames()
Rewrite the sequence names from binary/hexadecimal to a human readable
form.
|
void |
processSeqValues()
Transforms values of sequences from binary/hexadecimal to human readable
form
|
static java.lang.String |
removePipes(java.lang.String s)
removes the pipe character at the start and end from the given string
|
void |
removeUnnecessaryObjects()
cleans up maps from unused/unnecessary objects
|
void |
setEmpty(boolean empty)
marks the model as empty or full
|
void |
setTypes(ProblemTypeInformation types) |
java.lang.String |
toString()
returns a string representation of this SMT model
|
private boolean empty
private java.util.Map<java.lang.String,java.lang.String> constants
private java.util.Map<java.lang.String,java.lang.String> reversedConstants
private java.util.List<Heap> heaps
private java.util.List<LocationSet> locsets
private java.util.List<Sequence> sequences
private ProblemTypeInformation types
public boolean isEmpty()
public void setEmpty(boolean empty)
empty
- indicates model statusprivate java.lang.String processObjectID(java.lang.String objectID)
objectID
- object id in binary formprivate java.lang.String processSeqID(java.lang.String sequenceID)
sequenceID
- sequence id in binary formpublic java.util.Map<java.lang.String,java.lang.String> getConstants()
private void processLocSetNames()
public void processObjectNames()
public void processSequenceNames()
public java.util.List<Heap> getHeaps()
public java.util.List<Sequence> getSequences()
public java.util.List<LocationSet> getLocsets()
public ProblemTypeInformation getTypes()
public void setTypes(ProblemTypeInformation types)
types
- the types to setprivate void fillReversedTable()
public void addConstant(java.lang.String key, java.lang.String value)
key
- the constant namevalue
- the constant valuepublic void addHeap(Heap e)
e
- The heap to be addedpublic void addLocationSet(LocationSet e)
e
- The location set to be added.public void addSequence(Sequence s)
s
- The sequence to be added.private java.lang.String formatAny(java.lang.String val, SMTSort s)
val
- original any values
- actual sort of the any sortpublic java.lang.String processConstantValue(java.lang.String val, SMTSort s)
val
- binary/hexadecimal value of constants
- sort of constantpublic java.lang.String processAnyValue(java.lang.String val)
val
- the original any value in binary/hexadecimalpublic void processArrayValues()
public void processSeqValues()
private java.lang.String getAliasedName(java.lang.String original)
original
- the name for which an alias is createdpublic void addAliases()
private java.util.Map<java.lang.String,java.lang.String> extractFunctionValuesFor(ObjectVal o)
o
- the ObjectValprivate java.util.Map<java.lang.Integer,java.lang.String> extractArrayValuesFor(ObjectVal o)
o
- the ObjectValprivate java.util.Map<java.lang.String,java.lang.String> extractFieldValuesFor(ObjectVal o)
o
- the ObjectValpublic java.util.Set<ObjectVal> getNecessaryPrestateObjects(java.lang.String location)
location
- public ObjectVal findObject(java.lang.String ref)
ref
- the reference to the objectpublic void removeUnnecessaryObjects()
public java.util.Set<ObjectVal> getReachableObjects(java.lang.String name, Heap heap)
name
- the name of the object from where to lookheap
- the heappublic java.util.Set<ObjectVal> pointsTo(java.lang.String name, Heap heap)
name
- the source objectheap
- the heappublic ObjectVal getObject(java.lang.String name, Heap heap)
name
- the object to look upheap
- the heappublic static java.lang.String removePipes(java.lang.String s)
s
- the String to processpublic void processConstantsAndFieldValues()
public java.lang.String toString()
toString
in class java.lang.Object