ProgramState { public ProgramState addConstraint(SymbolicValue symbolicValue, Constraint constraint) { Preconditions.checkState(!(symbolicValue instanceof RelationalSymbolicValue && constraint == BooleanConstraint.FALSE), "Relations stored in PS should always use TRUE constraint. SV: %s", symbolicValue); ConstraintsByDomain constraintsForSV = constraints.get(symbolicValue); if(constraintsForSV == null) { constraintsForSV = ConstraintsByDomain.empty(); } return addConstraints(symbolicValue, constraintsForSV.put(constraint)); } private  ProgramState(PMap<Symbol, SymbolicValue> values,PMap<Integer, SymbolicValue> valuesByIndex, PMap<SymbolicValue, Integer> references,
                       PMap<SymbolicValue, ConstraintsByDomain> constraints, PMap<ProgramPoint, Integer> visitedPoints,
                       PStack<SymbolicValueSymbol> stack, SymbolicValue exitSymbolicValue); private  ProgramState(PMap<Symbol, SymbolicValue> values, PMap<SymbolicValue, Integer> references,
                       PMap<SymbolicValue, ConstraintsByDomain> constraints, PMap<ProgramPoint, Integer> visitedPoints,
                       PStack<SymbolicValueSymbol> stack, SymbolicValue exitSymbolicValue); private  ProgramState(ProgramState ps, PStack<SymbolicValueSymbol> newStack); private  ProgramState(ProgramState ps, PMap<SymbolicValue, ConstraintsByDomain> newConstraints); ProgramState stackValue(SymbolicValue sv); ProgramState stackValue(SymbolicValue sv, @Nullable Symbol symbol); Pop unstackValue(int nbElements); @CheckForNull SymbolicValue peekValue(); SymbolicValueSymbol peekValueSymbol(); SymbolicValue peekValue(int i); List<SymbolicValue> peekValues(int n); List<SymbolicValueSymbol> peekValuesAndSymbols(int n); int numberOfTimeVisited(ProgramPoint programPoint); @Override boolean equals(Object o); @Override int hashCode(); @Override String toString(); ProgramState addConstraintTransitively(SymbolicValue symbolicValue, Constraint constraint); Set<RelationalSymbolicValue> knownRelations(); ProgramState addConstraint(SymbolicValue symbolicValue, Constraint constraint); ProgramState addConstraints(SymbolicValue symbolicValue, ConstraintsByDomain constraintsForSV); ProgramState removeConstraintsOnDomain(SymbolicValue sv, Class<? extends Constraint> domain); @VisibleForTesting ProgramState put(Symbol symbol, SymbolicValue value); ProgramState cleanupDeadSymbols(Set<Symbol> liveVariables, Collection<SymbolicValue> protectedSymbolicValues); ProgramState cleanupConstraints(Collection<SymbolicValue> protectedSymbolicValues); static boolean isField(Symbol symbol); boolean canReach(SymbolicValue symbolicValue); ProgramState visitedPoint(ProgramPoint programPoint, int nbOfVisit); @Nullable ConstraintsByDomain getConstraints(SymbolicValue sv); @CheckForNull T getConstraint(SymbolicValue sv, Class<T> domain); int constraintsSize(); @CheckForNull SymbolicValue getValue(int index); @CheckForNull SymbolicValue getValue(Symbol symbol); List<SymbolicValue> getValuesWithConstraints(final Constraint constraint); void storeExitValue(); @CheckForNull SymbolicValue exitValue(); boolean exitingOnRuntimeException(); static final ProgramState EMPTY_STATE; }
@Test void testing_equals() { SymbolicValue sv1 = new SymbolicValue(); ProgramState state = ProgramState.EMPTY_STATE.addConstraint(sv1, ObjectConstraint.NOT_NULL); ProgramState state2 = ProgramState.EMPTY_STATE.addConstraint(sv1, ObjectConstraint.NOT_NULL); ProgramState state3 = ProgramState.EMPTY_STATE.addConstraint(sv1, ObjectConstraint.NULL); assertThat(state) .isNotEqualTo(null) .isNotEqualTo(new Object()) .isNotEqualTo(state3) .isEqualTo(state2); }
@Test void test_setting_constraint_on_relational_sv() throws Exception { RelationalSymbolicValue rel = new RelationalSymbolicValue(RelationalSymbolicValue.Kind.EQUAL); SymbolicValueTestUtil.computedFrom(rel, new SymbolicValue(), new SymbolicValue()); assertThatThrownBy(() -> ProgramState.EMPTY_STATE.addConstraint(rel, BooleanConstraint.FALSE)) .isInstanceOf(IllegalStateException.class) .hasMessageStartingWith("Relations stored in PS should always use TRUE constraint"); }