PptTopLevel

A PptMap is a collection of PptTopLevel objects.
A PptTopLevel contains PptSlice objects, one for each set of variables at the program point. For instance, if a PptTopLevel has variables a, b, and c, then it has three PptSlice1 objects (one for a; one for b; and one for c), three PptSlice2 objects (one for a,b; one for a,c; and one for b,c), and one PptSlice3 object (for a,b,c).
A PptSlice object contains invariants. When a sample (a tuple of variable values) is fed to a PptTopLevel, it in turn feeds it to all the slices, which feed it to all the invariants, which act on it appropriately.

See Also:: Serialized Form

Nested Class Summary
`class`	`PptTopLevel.CondIterator` Iterator for all of the conditional ppts.
`static class`	`PptTopLevel.PptFlags` Ppt attributes (specified in decl records)
`static class`	`PptTopLevel.PptType` Possible types of program points.
`static interface`	`PptTopLevel.SimplifyInclusionTester` Interface used by mark_implied_via_simplify to determine what invariants should be considered during the logical redundancy tests.
`static class`	`PptTopLevel.Stats` Stores various statistics about a ppt.
`static class`	`PptTopLevel.ViewsIteratorIterator` An iterator whose elements are themselves iterators that return invariants.

Nested classes/interfaces inherited from class Ppt
`Ppt.NameComparator`

Field Summary
`int`	`bb_length` Length of basic block (bytes)
`List<PptRelation>`	`children` All children relations in the variable/ppt hierarchy.
`PptCombined`	`combined_ppt` Combined ppt that should be processed when this ppt is encountered.
`boolean`	`combined_ppts_init` True if this basic block has been combined with other basic blocks to form combined program points.
`boolean`	`combined_subsumed` True if this ppt is subsumed by combined_ppt.
`PptTopLevel`	`combined_subsumed_by` The ppt whose combined ppt includes this one.
`DynamicConstants`	`constants` List of constant variables.
`static Logger`	`debug` Main debug tracer.
`static SimpleLog`	`debug_varinfo`
`static Logger`	`debugAddImplications` Debug tracer for addImplications.
`static Logger`	`debugConditional` Debug tracer for adding and processing conditional ppts.
`static Logger`	`debugEqualTo` Debug tracer for equalTo checks.
`static Logger`	`debugFlow` Debug tracer for data flow.
`static Logger`	`debugInstantiate` Debug tracer for instantiated slices.
`static Logger`	`debugMerge` Debug tracer for up-merging equality sets.
`static Logger`	`debugNISStats` Debug tracer for NIS suppression statistics
`static Logger`	`debugTimeMerge` Debug tracer for timing merges.
`static boolean`	`dkconfig_pairwise_implications` Boolean.
`static boolean`	`dkconfig_remove_merged_invs` Remove invariants at lower program points when a matching invariant is created at a higher program point.
`PptSliceEquality`	`equality_view` Holds Equality invariants.
`static boolean`	`first_pass_with_sample` Boolean.
`EnumSet<PptTopLevel.PptFlags>`	`flags` Attributes of this ppt
`String`	`function_id` Identifier of the function (for basic blocks)
`static Comparator<Invariant>`	`icfp`
`boolean`	`in_merge`
`int`	`instantiated_inv_cnt` Number of invariants after equality set processing for the last sample.
`int`	`instantiated_slice_cnt` Number of slices after equality set processing for the last sample.
`boolean`	`invariants_merged` Flag that indicates whether or not invariants have been merged from all of this ppts children to form the invariants here.
`boolean`	`invariants_removed` Flag that indicates whether or not invariants that are duplicated at the parent have been removed..
`PptSlice0`	`joiner_view`
`ValueTuple`	`last_values` The last set of values for this program point.
`String`	`name`
`int`	`num_declvars`
`int`	`num_orig_vars`
`int`	`num_static_constant_vars`
`int`	`num_tracevars`
`List<FileIO.ParentRelation>`	`parent_relations` List of parent relations in the variable/ppt hierarchy as specified in the declaration record.
`List<PptRelation>`	`parents` All parent relations in the variable/ppt hierarchy.
`PptName`	`ppt_name`
`List<String>`	`ppt_successors` List of successor program point names.
`List<PptTopLevel>`	`predecessors` List of predecesor program points.
`Set<Invariant>`	`redundant_invs` Redundant invariants, except for Equality invariants.
`Set<VarInfo>`	`redundant_invs_equality` The canonical VarInfo for the equality.
`ArrayList<PptSplitter>`	`splitters` List of all of the splitters for this ppt.
`PptTopLevel.PptType`	`type` Type of this program point

Fields inherited from class Ppt
`emptyInvList, var_infos`

Constructor Summary
`PptTopLevel(String name, PptTopLevel.PptType type, List<FileIO.ParentRelation> parents, EnumSet<PptTopLevel.PptFlags> flags, List<String> ppt_successors, String function_id, int bb_length, VarInfo[] var_infos)`
`PptTopLevel(String name, VarInfo[] var_infos)`

Method Summary
`Set<Invariant>`	`add_bottom_up(ValueTuple vt, int count)` Add the sample to the equality sets, dynamic constants and invariants at this program point.
`void`	`addConditions(Splitter[] splits)`
`void`	`addImplications()` Given conditional program points (and invariants detected over them), create implications.
`void`	`addSlice(PptSlice slice)` Add a single slice to the views variable
`void`	`addViews(Vector<PptSlice> slices_vector)` Add the specified slices to this ppt
`boolean`	`all_predecessors_goto(PptTopLevel ppt)` Returns true if all prececessor basic blocks eventually end up at the specified program point.
`int`	`all_predecessors_goto(PptTopLevel ppt, Set<PptTopLevel> visited_set)` Returns true if all predecessor basic blocks eventually end up at the specified progrm point.
`boolean`	`all_successors_goto(PptTopLevel ppt)` Returns true if all successor basic blocks eventually end up at the specified progrm point.
`int`	`all_successors_goto(PptTopLevel ppt, Set<PptTopLevel> visited_set)` Returns true if all successor basic blocks eventually end up at the specified progrm point.
`int`	`bb_offset()` If this is a basic block, returns the offset in the DLL
`static int[]`	`build_permute(VarInfo[] vis1, VarInfo[] vis2)` Builds a permutation from vis1 to vis2.
`boolean`	`check_implied_canonical(DiscardInfo di, VarInfo v1, VarInfo v2, Invariant proto)`
`DiscardInfo`	`check_implied_canonical(Invariant imp_inv, VarInfo v, Invariant proto)` If the proto invariant is true over the leader of the specified variable returns DiscardInfo indicating that the proto invariant implies imp_inv.
`DiscardInfo`	`check_implied_canonical(Invariant imp_inv, VarInfo v1, VarInfo v2, Invariant proto)` If the prototype invariant is true over the leader of each specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`boolean`	`check_implied(DiscardInfo di, VarInfo v1, VarInfo v2, Invariant proto)`
`DiscardInfo`	`check_implied(Invariant imp_inv, VarInfo v, Invariant proto)` If the prototype invariant is true over the specified variable returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`DiscardInfo`	`check_implied(Invariant imp_inv, VarInfo v1, VarInfo v2, Invariant proto)` If the prototype invariant is true over the specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`void`	`clean_for_merge()` Cleans up the ppt so that its invariants can be merged from other ppts.
`PptTopLevel.CondIterator`	`cond_iterator()` returns an iterator over all of the splitters at this ppt
`boolean`	`connected(PptTopLevel ppt)` Returns true if there is a connection (using successors) from this ppt to ppt
`boolean`	`connected(PptTopLevel ppt, Set<PptTopLevel> visited_set)` Returns true if all successor basic blocks eventually end up at the specified progrm point.
`int`	`const_inv_cnt()` Returns the number of invariants that contain one or more constants.
`int`	`const_slice_cnt()` Returns the number of slices that contain one or more constants.
`void`	`create_derived_variables()` Create all the derived variables.
`PptSlice`	`create_equality_inv(VarInfo v1, VarInfo v2, int samples)` Create an equality invariant over the specified variables.
`void`	`debug_invs(Logger log)` Debug print to the specified logger information about each invariant at this ppt
`void`	`debug_print_slice_info(Logger log, String descr, List<PptSlice> slices)` Debug print slice/inv count information to the specified logger
`void`	`debug_print_tree(Logger l, int indent, PptRelation parent_rel)` Debug method to print children (in the partial order) recursively.
`void`	`debug_unary_info(Logger log)` Debug print to the specified logger information about each variable in this ppt.
`String`	`debugSlices()` Debug method to display all slices.
`String`	`equality_sets_txt()` Returns a string version of all of the equality sets for this ppt.
`List<Invariant>`	`find_assignment_inv(VarInfo v)` Searches for all of the invariants that that provide an exact value for v.
`PptTopLevel`	`find_combined_ppt_leader()` Finds the ppt whose combined ppt subsumes this one.
`Invariant`	`find_inv_by_class(VarInfo[] vis, Class<? extends Invariant> cls)` Returns the invariant in the slice specified by vis that matches the specified class.
`PptSlice`	`findSlice_unordered(VarInfo[] vis)` Find a pptSlice without an assumed ordering.
`PptSlice2`	`findSlice_unordered(VarInfo v1, VarInfo v2)` Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
`PptSlice3`	`findSlice_unordered(VarInfo v1, VarInfo v2, VarInfo v3)` Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
`PptSlice1`	`findSlice(VarInfo v)` Returns the unary slice over v.
`PptSlice`	`findSlice(VarInfo[] vis)` Find a pptSlice with an assumed ordering.
`PptSlice2`	`findSlice(VarInfo v1, VarInfo v2)` Returns the binary slice over v1 and v2.
`PptSlice3`	`findSlice(VarInfo v1, VarInfo v2, VarInfo v3)` Returns the ternary slice over v1, v2, and v3.
`void`	`get_missingOutOfBounds(PptTopLevel ppt, ValueTuple vt)` Gets any missing out of bounds variables from the specified ppt and applies them to the matching variable in this ppt if the variable is MISSING_NONSENSICAL.
`PptSlice`	`get_or_instantiate_slice(VarInfo vi)` Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo[] vis)` Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo v1, VarInfo v2)` Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo v1, VarInfo v2, VarInfo v3)` Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_temp_slice(VarInfo v)` Looks up the slice for v1.
`PptSlice`	`get_temp_slice(VarInfo v1, VarInfo v2)` Looks up the slice for v1 and v2.
`List<Invariant>`	`getInvariants()` Return a List of all the invariants for the program point.
`Set<VarInfo>`	`getParamVars()` Returns variables in this Ppt that are parameters.
`boolean`	`has_parent(VarInfo v)` Returns whether or not the specified variable in this ppt has any parents.
`boolean`	`has_splitters()` Returns whether or not this ppt has any splitters.
`void`	`incSampleNumber()` Increments the number of samples processed by the program point by 1
`void`	`instantiate_views_and_invariants()` This function creates all the views (and thus candidate invariants), but does not check those invariants.
`List<Invariant>`	`inv_add(List<Invariant> inv_list, ValueTuple vt, int count)` Adds a sample to each invariant in the list.
`Map<Class<? extends Invariant>,PptTopLevel.Cnt>`	`invariant_cnt_by_class()` Returns how many invariants there are of each invariant class.
`int`	`invariant_cnt()` Returns the number of true invariants at this ppt.
`Iterator<Invariant>`	`invariants_iterator()` Iterate over all of the invariants at this ppt (but not any implications).
`Vector<Invariant>`	`invariants_vector()` Vector version of getInvariants()
`boolean`	`is_basic_block()` Is this a basic block ppt
`boolean`	`is_class()` Is this a ppt that represents a class?
`boolean`	`is_combined_exit()` Is this a combined exit point?
`boolean`	`is_constant(VarInfo v)` Returns whether or not the specified variable is dynamically constant.
`boolean`	`is_empty(VarInfo varr)` Returns true if varr is empty.
`boolean`	`is_enter()` is this an enter ppt
`boolean`	`is_equal(VarInfo v1, VarInfo v2)` Returns whether or not the specified variables are equal (ie, an equality invariant exists between them)
`boolean`	`is_exit()` Is this is an exit ppt (combined or specific)?
`boolean`	`is_less_equal(VarInfo v1, int v1_shift, VarInfo v2, int v2_shift)` Returns true if (v1+v1_shift) <= (v2+v2_shift) is known to be true.
`boolean`	`is_missing(VarInfo v)` Returns whether or not the specified variable has been missing for all samples seen so far.
`boolean`	`is_nonzero(VarInfo v)` Returns whether or not v1 is always non-zero
`boolean`	`is_object()` Is this a ppt that represents an object?
`boolean`	`is_prev_constant(VarInfo v)` Returns whether or not the specified variable is currently dynamically constant, or was a dynamic constant at the beginning of constant processing.
`boolean`	`is_prev_missing(VarInfo v)` returns whether the specified variable is currently missing OR was missing at the beginning of constants processing.
`boolean`	`is_slice_ok(VarInfo var1)` Returns whether or not the specified unary slice should be created.
`boolean`	`is_slice_ok(VarInfo[] vis, int arity)` Returns whether or not the specified slice should be created.
`boolean`	`is_slice_ok(VarInfo var1, VarInfo var2)` Returns whether or not the specified binary slice should be created.
`boolean`	`is_slice_ok(VarInfo v1, VarInfo v2, VarInfo v3)` Returns whether or not the specified ternary slice should be created by checking the variables' qualifications.
`boolean`	`is_subexit()` Is this a numbered (specific) exit point?
`boolean`	`is_subsequence(VarInfo v1, VarInfo v2)` Returns true if v1 is known to be a subsequence of v2.
`boolean`	`is_subset(VarInfo v1, VarInfo v2)` Returns whether or not v1 is a subset of v2.
`void`	`mark_implied_via_simplify(PptMap all_ppts)` Use the Simplify theorem prover to flag invariants that are logically implied by others.
`void`	`merge_conditionals()` Merges the conditionals from the children of this ppt to this ppt.
`void`	`merge_invs_multiple_children()` Merges the invariants from multiple children.
`void`	`merge_invs_one_child()` Merges one child.
`void`	`mergeInvs()` Recursively merge invariants from children to create an invariant list at this ppt.
`String`	`name()`
`int`	`num_array_vars()`
`int`	`num_samples()` The number of samples processed by this program point so far.
`int`	`num_samples(VarInfo vi1)` Return the number of samples where vi1 is present (not missing)
`int`	`num_samples(VarInfo vi1, VarInfo vi2)` Return the number of samples where vi1 and vi2 are both present (not missing)
`int`	`num_samples(VarInfo vi1, VarInfo vi2, VarInfo vi3)` Return the number of samples where vi1, vi2, and vi3 are all present (not missing)
`int`	`num_values(VarInfo vi1)` The number of distinct values that have been seen.
`int`	`num_values(VarInfo vi1, VarInfo vi2)` An upper bound on the number of distinct pairs of values that have been seen.
`int`	`num_values(VarInfo vi1, VarInfo vi2, VarInfo vi3)` An upper bound on the number of distinct values over vi1, vi2, and vi3 that have been seen.
`int`	`numViews()`
`VarInfo[]`	`parent_vis(PptRelation rel, PptSlice slice)` Creates a list of parent variables (i.e., variables at the parent program point) that matches slice.
`void`	`postProcessEquality()` Two things: a) convert Equality invariants into normal IntEqual type for filtering, printing, etc. b) Pivot uninteresting parameter VarInfos so that each equality set contains only the interesting one.
`static void`	`print_equality_stats(Logger log, PptMap all_ppts)` Print statistics concerning equality sets over the entire set of ppts to the specified logger.
`void`	`processOmissions(boolean[] omitTypes)` remove invariants that are marked for ommission in omitTypes
`void`	`remove_child_invs(PptRelation rel)` Removes any invariant in this ppt which has a matching invariant in the parent (as specified in the relation).
`void`	`remove_equality_invariants()` Remove the equality invariants added during equality post processing.
`void`	`remove_implications()` Remove all of the implications from this program point.
`void`	`remove_invs(List<Invariant> rm_list)` Remove a list of invariants
`void`	`removeSlice(PptSlice slice)` Remove a slice from this PptTopLevel.
`void`	`repCheck()` Check the rep invariants of this.
`void`	`simplify_variable_names()` Simplify the names of variables before printing them.
`int`	`slice_cnt()` Returns the number of slices at this ppt.
`String`	`toString()` Returns the full name of the ppt
`void`	`trimToSize()` Trim the collections used here, in hopes of saving space.
`Iterator<VarInfo>`	`var_info_iterator()` Iterate through each variable at this ppt
`String`	`var_names()`
`Iterator<PptSlice>`	`views_iterator()` For some clients, this method may be more efficient than getInvariants.
`boolean`	`vis_order_ok(VarInfo[] vis)` Determines whether the order of the variables in vis is a valid permutation (i.e., their varinfo_index's are ordered).
`static boolean`	`worthDerivingFrom(VarInfo vi)`

Methods inherited from class Ppt
`containsVar, find_var_by_name, indexOf, varNames, varNames`

Methods inherited from class Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`

Field Detail

dkconfig_pairwise_implications

public static boolean dkconfig_pairwise_implications

Boolean. If true, create implications for all pairwise combinations of conditions, and all pairwise combinations of exit points. If false, create implications for only the first two conditions, and create implications only if there are exactly two exit points.

dkconfig_remove_merged_invs

public static boolean dkconfig_remove_merged_invs

Remove invariants at lower program points when a matching invariant is created at a higher program point. For experimental purposes only.

first_pass_with_sample

public static boolean first_pass_with_sample

Boolean. Needed by the NIS.falsified method when keeping stats to figure out how many falsified invariants are antecedents. Only the first pass of processing with the sample is counted toward the stats.

flags

public EnumSet<PptTopLevel.PptFlags> flags

Attributes of this ppt

type

public PptTopLevel.PptType type

Type of this program point

instantiated_inv_cnt

public int instantiated_inv_cnt

Number of invariants after equality set processing for the last sample.

instantiated_slice_cnt

public int instantiated_slice_cnt

Number of slices after equality set processing for the last sample.

debug

public static final Logger debug

Main debug tracer.

debugInstantiate

public static final Logger debugInstantiate

Debug tracer for instantiated slices.

debugTimeMerge

public static final Logger debugTimeMerge

Debug tracer for timing merges.

debugEqualTo

public static final Logger debugEqualTo

Debug tracer for equalTo checks.

debugAddImplications

public static final Logger debugAddImplications

Debug tracer for addImplications.

debugConditional

public static final Logger debugConditional

Debug tracer for adding and processing conditional ppts.

debugFlow

public static final Logger debugFlow

Debug tracer for data flow.

debugMerge

public static final Logger debugMerge

Debug tracer for up-merging equality sets.

debugNISStats

public static final Logger debugNISStats

Debug tracer for NIS suppression statistics

debug_varinfo

public static final SimpleLog debug_varinfo

name

public final String name

ppt_name

public final PptName ppt_name

constants

public DynamicConstants constants

List of constant variables. Null unless dkconfig_use_dynamic_constant_optimization is set.

num_declvars

public int num_declvars

num_tracevars

public int num_tracevars

num_orig_vars

public int num_orig_vars

num_static_constant_vars

public int num_static_constant_vars

splitters

public ArrayList<PptSplitter> splitters

List of all of the splitters for this ppt.

children

public List<PptRelation> children

All children relations in the variable/ppt hierarchy.

parents

public List<PptRelation> parents

All parent relations in the variable/ppt hierarchy.

parent_relations

public List<FileIO.ParentRelation> parent_relations

List of parent relations in the variable/ppt hierarchy as specified in the declaration record. These are used to build the detailed parents/children lists of PptRelation above

ppt_successors

public List<String> ppt_successors

List of successor program point names. Later changed into a list of successor PptTopLevel. Can be null (not an empty list) if there are no successors, as for an exit program point.

predecessors

public List<PptTopLevel> predecessors

List of predecesor program points. Computed from ppt_successors. This field is only properly set and used when creating combined program points.

function_id

public String function_id

Identifier of the function (for basic blocks)

bb_length

public int bb_length

Length of basic block (bytes)

combined_ppts_init

public boolean combined_ppts_init

True if this basic block has been combined with other basic blocks to form combined program points.

combined_ppt

public PptCombined combined_ppt

Combined ppt that should be processed when this ppt is encountered. Only non-null for basic block ppts.

combined_subsumed

public boolean combined_subsumed

True if this ppt is subsumed by combined_ppt. A different ppt is the trigger to the combined_ppt (ie, the ppt whose data is used to initiate the processing of a sample for the combined ppt

combined_subsumed_by

public PptTopLevel combined_subsumed_by

The ppt whose combined ppt includes this one. Only non-null for basic block ppts.

last_values

public ValueTuple last_values

The last set of values for this program point. Only for basic block ppts.

invariants_merged

public boolean invariants_merged

Flag that indicates whether or not invariants have been merged from all of this ppts children to form the invariants here. Necessary because a ppt can have multiple parents and otherwise we'd needlessly merge multiple times

in_merge

public boolean in_merge

invariants_removed

public boolean invariants_removed

Flag that indicates whether or not invariants that are duplicated at the parent have been removed..

joiner_view

public PptSlice0 joiner_view

equality_view

public PptSliceEquality equality_view

Holds Equality invariants. Never null after invariants are instantiated.

redundant_invs

public Set<Invariant> redundant_invs

Redundant invariants, except for Equality invariants.

redundant_invs_equality

public Set<VarInfo> redundant_invs_equality

The canonical VarInfo for the equality.

icfp

public static final Comparator<Invariant> icfp

Constructor Detail

PptTopLevel

public PptTopLevel(String name,
                   PptTopLevel.PptType type,
                   List<FileIO.ParentRelation> parents,
                   EnumSet<PptTopLevel.PptFlags> flags,
                   List<String> ppt_successors,
                   String function_id,
                   int bb_length,
                   VarInfo[] var_infos)

PptTopLevel

public PptTopLevel(String name,
                   VarInfo[] var_infos)

Method Detail

name

public String name()

Specified by:: name in class Ppt

cond_iterator

public PptTopLevel.CondIterator cond_iterator()

returns an iterator over all of the splitters at this ppt

has_splitters

public boolean has_splitters()

Returns whether or not this ppt has any splitters.

num_array_vars

public int num_array_vars()

var_info_iterator

public Iterator<VarInfo> var_info_iterator()

Iterate through each variable at this ppt

toString

public String toString()

Returns the full name of the ppt

Overrides:: toString in class Object

trimToSize

public void trimToSize()

Trim the collections used here, in hopes of saving space.

Overrides:: trimToSize in class Ppt

num_samples

public int num_samples()

The number of samples processed by this program point so far.

num_samples

public int num_samples(VarInfo vi1)

Return the number of samples where vi1 is present (not missing)

num_samples

public int num_samples(VarInfo vi1,
                       VarInfo vi2)

Return the number of samples where vi1 and vi2 are both present (not missing)

num_samples

public int num_samples(VarInfo vi1,
                       VarInfo vi2,
                       VarInfo vi3)

Return the number of samples where vi1, vi2, and vi3 are all present (not missing)

num_values

public int num_values(VarInfo vi1)

The number of distinct values that have been seen.

num_values

public int num_values(VarInfo vi1,
                      VarInfo vi2)

An upper bound on the number of distinct pairs of values that have been seen. Note that there can't be more pairs of values than there are samples. This matters when there are very few samples due to one of the variables being missing.

num_values

public int num_values(VarInfo vi1,
                      VarInfo vi2,
                      VarInfo vi3)

An upper bound on the number of distinct values over vi1, vi2, and vi3 that have been seen. Note that there can't be more pairs of values than there are samples. This matters when there are very few samples due to one of the variables being missing.

numViews

public int numViews()

worthDerivingFrom

public static boolean worthDerivingFrom(VarInfo vi)

add_bottom_up

public Set<Invariant> add_bottom_up(ValueTuple vt,
                                    int count)

Add the sample to the equality sets, dynamic constants and invariants at this program point. This version is specific to the bottom up processing mechanism. This routine also instantiates slices/invariants on the first call for the ppt.

Parameters:: vt - the set of values for this to see; count - the number of samples that vt represents
Returns:: the set of all invariants weakened or falsified by this sample

inv_add

public List<Invariant> inv_add(List<Invariant> inv_list,
                               ValueTuple vt,
                               int count)

Adds a sample to each invariant in the list. Returns the list of weakened invariants. This should only be called when the sample has already been added to the slice containing each invariant. Otherwise the statistics kept in the slice will be incorrect.

get_missingOutOfBounds

public void get_missingOutOfBounds(PptTopLevel ppt,
                                   ValueTuple vt)

Gets any missing out of bounds variables from the specified ppt and applies them to the matching variable in this ppt if the variable is MISSING_NONSENSICAL. The goal is to set the missing_array_bounds flag only if it was missing in ppt on THIS sample. This could fail if missing_array_bounds was set on a previous sample and the MISSING_NONSENSICAL flag is set for a different reason on this sample. This could happen with an array in an object. This implementation is also not particularly efficient and the variables must match exactly. Missing out of bounds really needs to be implemented as a separate flag in the missing bits. That would clear up all of this mess.

is_constant

public boolean is_constant(VarInfo v)

Returns whether or not the specified variable is dynamically constant.

is_prev_constant

public boolean is_prev_constant(VarInfo v)

Returns whether or not the specified variable is currently dynamically constant, or was a dynamic constant at the beginning of constant processing.

is_missing

public boolean is_missing(VarInfo v)

Returns whether or not the specified variable has been missing for all samples seen so far.

is_prev_missing

public boolean is_prev_missing(VarInfo v)

returns whether the specified variable is currently missing OR was missing at the beginning of constants processing.

invariant_cnt

public int invariant_cnt()

Returns the number of true invariants at this ppt.

const_slice_cnt

public int const_slice_cnt()

Returns the number of slices that contain one or more constants.

const_inv_cnt

public int const_inv_cnt()

Returns the number of invariants that contain one or more constants.

debug_invs

public void debug_invs(Logger log)

Debug print to the specified logger information about each invariant at this ppt

debug_unary_info

public void debug_unary_info(Logger log)

Debug print to the specified logger information about each variable in this ppt. Currently only prints integer and float information using the bound invariants

invariant_cnt_by_class

public Map<Class<? extends Invariant>,PptTopLevel.Cnt> invariant_cnt_by_class()

Returns how many invariants there are of each invariant class. The map is from the invariant class to an integer cnt of the number of that class.

slice_cnt

public int slice_cnt()

Returns the number of slices at this ppt.

create_derived_variables

public void create_derived_variables()

Create all the derived variables.

addViews

public void addViews(Vector<PptSlice> slices_vector)

Add the specified slices to this ppt

addSlice

public void addSlice(PptSlice slice)

Add a single slice to the views variable

removeSlice

public void removeSlice(PptSlice slice)

Remove a slice from this PptTopLevel.

remove_invs

public void remove_invs(List<Invariant> rm_list)

Remove a list of invariants

findSlice

public PptSlice1 findSlice(VarInfo v)

Returns the unary slice over v. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).

findSlice

public PptSlice2 findSlice(VarInfo v1,
                           VarInfo v2)

Returns the binary slice over v1 and v2. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).

findSlice_unordered

public PptSlice2 findSlice_unordered(VarInfo v1,
                                     VarInfo v2)

Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.

findSlice

public PptSlice3 findSlice(VarInfo v1,
                           VarInfo v2,
                           VarInfo v3)

Returns the ternary slice over v1, v2, and v3. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).

findSlice_unordered

public PptSlice3 findSlice_unordered(VarInfo v1,
                                     VarInfo v2,
                                     VarInfo v3)

Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.

findSlice_unordered

public PptSlice findSlice_unordered(VarInfo[] vis)

Find a pptSlice without an assumed ordering.

findSlice

public PptSlice findSlice(VarInfo[] vis)

Find a pptSlice with an assumed ordering.

find_inv_by_class

public Invariant find_inv_by_class(VarInfo[] vis,
                                   Class<? extends Invariant> cls)

Returns the invariant in the slice specified by vis that matches the specified class. If the slice or the invariant does not exist, returns null.

find_assignment_inv

public List<Invariant> find_assignment_inv(VarInfo v)

Searches for all of the invariants that that provide an exact value for v. Intuitively those are invariants of the form 'v = equation'. For example: 'v = 63' or 'v = x * y' The implementation is a little iffy -- each invariant over v is examined and it matches iff it is exact and its daikon format starts with 'v ='.

Returns:: list of matching invariants or null if no matching invariants are found

get_temp_slice

public PptSlice get_temp_slice(VarInfo v)

Looks up the slice for v1. If the slice does not exist, one is created (but not added into the list of slices for this ppt).

get_temp_slice

public PptSlice get_temp_slice(VarInfo v1,
                               VarInfo v2)

Looks up the slice for v1 and v2. They do not have to be in order. If the slice does not exist, one is created (but not added into the list of slices for this ppt).

check_implied

public DiscardInfo check_implied(Invariant imp_inv,
                                 VarInfo v,
                                 Invariant proto)

If the prototype invariant is true over the specified variable returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.

check_implied_canonical

public DiscardInfo check_implied_canonical(Invariant imp_inv,
                                           VarInfo v,
                                           Invariant proto)

If the proto invariant is true over the leader of the specified variable returns DiscardInfo indicating that the proto invariant implies imp_inv. Otherwise returns null.

check_implied

public DiscardInfo check_implied(Invariant imp_inv,
                                 VarInfo v1,
                                 VarInfo v2,
                                 Invariant proto)

If the prototype invariant is true over the specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.

check_implied

public boolean check_implied(DiscardInfo di,
                             VarInfo v1,
                             VarInfo v2,
                             Invariant proto)

check_implied_canonical

public DiscardInfo check_implied_canonical(Invariant imp_inv,
                                           VarInfo v1,
                                           VarInfo v2,
                                           Invariant proto)

If the prototype invariant is true over the leader of each specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.

check_implied_canonical

public boolean check_implied_canonical(DiscardInfo di,
                                       VarInfo v1,
                                       VarInfo v2,
                                       Invariant proto)

is_subset

public boolean is_subset(VarInfo v1,
                         VarInfo v2)

Returns whether or not v1 is a subset of v2.

is_nonzero

public boolean is_nonzero(VarInfo v)

Returns whether or not v1 is always non-zero

is_equal

public boolean is_equal(VarInfo v1,
                        VarInfo v2)

Returns whether or not the specified variables are equal (ie, an equality invariant exists between them)

is_less_equal

public boolean is_less_equal(VarInfo v1,
                             int v1_shift,
                             VarInfo v2,
                             int v2_shift)

Returns true if (v1+v1_shift) <= (v2+v2_shift) is known to be true. Returns false otherwise. Integers only.

is_subsequence

public boolean is_subsequence(VarInfo v1,
                              VarInfo v2)

Returns true if v1 is known to be a subsequence of v2. This is true if the subsequence invariant exists or if it it suppressed

is_empty

public boolean is_empty(VarInfo varr)

Returns true if varr is empty. Supports ints, doubles, and strings.

instantiate_views_and_invariants

public void instantiate_views_and_invariants()

This function creates all the views (and thus candidate invariants), but does not check those invariants. We create NO views over static constant variables, but everything else is fair game. We don't create views over variables which have a higher (controlling) view. This function does NOT cause invariants over the new views to be checked (but it does create invariants).

is_slice_ok

public boolean is_slice_ok(VarInfo[] vis,
                           int arity)

Returns whether or not the specified slice should be created.

is_slice_ok

public boolean is_slice_ok(VarInfo var1)

Returns whether or not the specified unary slice should be created. The slice should not be created if the variable does not meet qualifications for the unary slice.

See Also:: is_var_ok_unary(VarInfo)

is_slice_ok

public boolean is_slice_ok(VarInfo var1,
                           VarInfo var2)

Returns whether or not the specified binary slice should be created. The slice should not be created if any of the following are true: - One of the variables does not meet qualifications for the binary slice - Variables are not compatible - Both variables are constant.

See Also:: is_var_ok_binary(VarInfo)

is_slice_ok

public boolean is_slice_ok(VarInfo v1,
                           VarInfo v2,
                           VarInfo v3)

Returns whether or not the specified ternary slice should be created by checking the variables' qualifications. In addition, The slice should not be created if any of the following are true: - One of the variables does not meet qualifications for the ternary slice - All of the vars are constants - Any var is not (integral or float) - Each var is the same and its equality set has only two variables - Two of the vars are the same and its equality has only one variable (this last one is currently disabled as x = func(x,y) might still be interesting even if x is the same.

See Also:: is_var_ok_ternary(VarInfo)

vis_order_ok

public boolean vis_order_ok(VarInfo[] vis)

Determines whether the order of the variables in vis is a valid permutation (i.e., their varinfo_index's are ordered). Null elements are ignored (and an all-null list is ok)

get_or_instantiate_slice

public PptSlice get_or_instantiate_slice(VarInfo[] vis)

Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the caller that the slice be either filled with one or more invariants, or else removed from the views collection.

When the arity of the slice is known, call one of the overloaded definitions of get_or_instantiate_slice that takes (one or more) VarInfo arguments; they are more efficient.

Parameters:: vis - array of VarInfo objects; is not used internally (so the same value can be passed in repeatedly). Can be unsorted.

get_or_instantiate_slice

public PptSlice get_or_instantiate_slice(VarInfo vi)

get_or_instantiate_slice

public PptSlice get_or_instantiate_slice(VarInfo v1,
                                         VarInfo v2)

get_or_instantiate_slice

public PptSlice get_or_instantiate_slice(VarInfo v1,
                                         VarInfo v2,
                                         VarInfo v3)

addConditions

public void addConditions(Splitter[] splits)

addImplications

public void addImplications()

Given conditional program points (and invariants detected over them), create implications. Configuration variable "pairwise_implications" controls whether all or only the first two conditional program points are considered.

postProcessEquality

public void postProcessEquality()

Two things: a) convert Equality invariants into normal IntEqual type for filtering, printing, etc. b) Pivot uninteresting parameter VarInfos so that each equality set contains only the interesting one.

mark_implied_via_simplify

public void mark_implied_via_simplify(PptMap all_ppts)

Use the Simplify theorem prover to flag invariants that are logically implied by others. Considers only invariants that pass isWorthPrinting.

getParamVars

public Set<VarInfo> getParamVars()

Returns variables in this Ppt that are parameters.

getInvariants

public List<Invariant> getInvariants()

Return a List of all the invariants for the program point. Also consider using views_iterator() instead. You can't modify the result of this.

invariants_vector

public Vector<Invariant> invariants_vector()

Vector version of getInvariants()

views_iterator

public Iterator<PptSlice> views_iterator()

For some clients, this method may be more efficient than getInvariants.

invariants_iterator

public Iterator<Invariant> invariants_iterator()

Iterate over all of the invariants at this ppt (but not any implications).

simplify_variable_names

public void simplify_variable_names()

Simplify the names of variables before printing them. For example, "orig(a[post(i)])" might change into "orig(a[i+1])". We might want to switch off this behavior, depending on various heuristics. We'll have to try it and see which output we like best. In any case, we have to do this for ESC output, since ESC doesn't have anything like post().

processOmissions

public void processOmissions(boolean[] omitTypes)

remove invariants that are marked for ommission in omitTypes

repCheck

public void repCheck()

Check the rep invariants of this. Throw an Error if not okay.

debugSlices

public String debugSlices()

Debug method to display all slices.

debug_print_tree

public void debug_print_tree(Logger l,
                             int indent,
                             PptRelation parent_rel)

Debug method to print children (in the partial order) recursively.

equality_sets_txt

public String equality_sets_txt()

Returns a string version of all of the equality sets for this ppt. The string is of the form [a,b], [c,d] where a,b and c,d are each in an equality set. Should be used only for debugging.

has_parent

public boolean has_parent(VarInfo v)

Returns whether or not the specified variable in this ppt has any parents.

mergeInvs

public void mergeInvs()

Recursively merge invariants from children to create an invariant list at this ppt. First, equality sets are created for this ppt. These are the intersection of the equality sets from each child. Then create unary, binary, and ternary slices for each combination of equality sets and build the invariants for each slice.

merge_invs_multiple_children

public void merge_invs_multiple_children()

Merges the invariants from multiple children. NI suppression is handled by first creating all of the suppressed invariants in each of the children, performing the merge, and then removing them.

merge_invs_one_child

public void merge_invs_one_child()

Merges one child. Since there is only one child, the merge is trivial (each invariant can be just copied to the parent)

parent_vis

public VarInfo[] parent_vis(PptRelation rel,
                            PptSlice slice)

Creates a list of parent variables (i.e., variables at the parent program point) that matches slice. Returns null if any of the variables don't have a corresponding parent variables. The corresponding parent variable can match ANY of the members of an equality set. For example, suppose that the child is EXIT with variable A, with equality set members {A, orig(A)}; and suppose that this child is matched against ENTER. A does not have a relation (since it is a post value), but orig(a) does have a relation. Note that there are cases where this is not exactly correct. if you wanted to get all of the invariants over A where A is an equality set with B, and A and B were in different equality sets at the parent, the invariants true at A in the child are the union of those true at A and B at the parent.

merge_conditionals

public void merge_conditionals()

Merges the conditionals from the children of this ppt to this ppt. Only conditionals that exist at each child and whose splitting condition is valid here can be merged.

clean_for_merge

public void clean_for_merge()

Cleans up the ppt so that its invariants can be merged from other ppts. Not normally necessary unless the merge is taking place over multiple ppts maps based on different data. This allows a ppt to have its invariants recalculated.

remove_equality_invariants

public void remove_equality_invariants()

Remove the equality invariants added during equality post processing. These are not over leaders and can causes in some uses of the ppt. In particular, they cause problems during merging.

remove_implications

public void remove_implications()

Remove all of the implications from this program point. Can be used when recalculating implications. Actually removes the entire joiner_view.

remove_child_invs

public void remove_child_invs(PptRelation rel)

Removes any invariant in this ppt which has a matching invariant in the parent (as specified in the relation). Done to save space. Only safe when all processing of this child is complete (i.e., all of the parents of this child must have been merged) Another interesting problem arises with this code. As currently setup, it won't process combined exit points (which often have two parents), but it will process enter points. Once the enter point is removed, it can no longer parent filter the combined exit point. Also, the dynamic obvious code doesn't work anymore (because it is missing the appropriate invariants). This could be fixed by changing dynamic obvious to search up the tree (blecho!). Fix this by only doing this for ppts whose parent only has one child

build_permute

public static int[] build_permute(VarInfo[] vis1,
                                  VarInfo[] vis2)

Builds a permutation from vis1 to vis2. The result is vis1[i] = vis2[permute[i]]

debug_print_slice_info

public void debug_print_slice_info(Logger log,
                                   String descr,
                                   List<PptSlice> slices)

Debug print slice/inv count information to the specified logger

create_equality_inv

public PptSlice create_equality_inv(VarInfo v1,
                                    VarInfo v2,
                                    int samples)

Create an equality invariant over the specified variables. Samples should be the number of samples for the slice over v1 and v2. The slice should not already exist.

print_equality_stats

public static void print_equality_stats(Logger log,
                                        PptMap all_ppts)

Print statistics concerning equality sets over the entire set of ppts to the specified logger.

incSampleNumber

public void incSampleNumber()

Increments the number of samples processed by the program point by 1

is_exit

public boolean is_exit()

Is this is an exit ppt (combined or specific)?

is_enter

public boolean is_enter()

is this an enter ppt

is_basic_block

public boolean is_basic_block()

Is this a basic block ppt

is_combined_exit

public boolean is_combined_exit()

Is this a combined exit point?

is_subexit

public boolean is_subexit()

Is this a numbered (specific) exit point?

is_object

public boolean is_object()

Is this a ppt that represents an object?

is_class

public boolean is_class()

Is this a ppt that represents a class?

var_names

public String var_names()

bb_offset

public int bb_offset()

If this is a basic block, returns the offset in the DLL

find_combined_ppt_leader

public PptTopLevel find_combined_ppt_leader()

Finds the ppt whose combined ppt subsumes this one. Combined ppts must have been initialized

connected

public boolean connected(PptTopLevel ppt)

Returns true if there is a connection (using successors) from this ppt to ppt

connected

public boolean connected(PptTopLevel ppt,
                         Set<PptTopLevel> visited_set)

Returns true if all successor basic blocks eventually end up at the specified progrm point. All paths must go to ppt for this to return true. The visited_set should contain each program point visited along this path so far.

all_successors_goto

public boolean all_successors_goto(PptTopLevel ppt)

Returns true if all successor basic blocks eventually end up at the specified progrm point. All paths must go to ppt for this to return true

all_successors_goto

public int all_successors_goto(PptTopLevel ppt,
                               Set<PptTopLevel> visited_set)

all_predecessors_goto

public boolean all_predecessors_goto(PptTopLevel ppt)

Returns true if all prececessor basic blocks eventually end up at the specified program point. All paths must go to ppt for this to return true

all_predecessors_goto

public int all_predecessors_goto(PptTopLevel ppt,
                                 Set<PptTopLevel> visited_set)

Returns true if all predecessor basic blocks eventually end up at the specified progrm point. All paths must go to ppt for this to return true. The visited_set should contain each program point visited along this path so far.

Overview

Package

Class

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

daikon Class PptTopLevel

dkconfig_pairwise_implications

dkconfig_remove_merged_invs

first_pass_with_sample

flags

type

instantiated_inv_cnt

instantiated_slice_cnt

debug

debugInstantiate

debugTimeMerge

debugEqualTo

debugAddImplications

debugConditional

debugFlow

debugMerge

debugNISStats

debug_varinfo

name

ppt_name

constants

num_declvars

num_tracevars

num_orig_vars

num_static_constant_vars

splitters

children

parents

parent_relations

ppt_successors

predecessors

function_id

bb_length

combined_ppts_init

combined_ppt

combined_subsumed

combined_subsumed_by

last_values

invariants_merged

in_merge

invariants_removed

joiner_view

equality_view

redundant_invs

redundant_invs_equality

icfp

PptTopLevel

PptTopLevel

name

cond_iterator

has_splitters

num_array_vars

var_info_iterator

toString

trimToSize

num_samples

num_samples

num_samples

num_samples

num_values

num_values

num_values

numViews

worthDerivingFrom

add_bottom_up

inv_add

get_missingOutOfBounds

is_constant

is_prev_constant

is_missing

is_prev_missing

invariant_cnt

const_slice_cnt

const_inv_cnt

debug_invs

debug_unary_info

invariant_cnt_by_class

slice_cnt

create_derived_variables

addViews

daikon
Class PptTopLevel