RelationalSymbolicValue extends BinarySymbolicValue { @Override public List<ProgramState> setConstraint(ProgramState initialProgramState, BooleanConstraint booleanConstraint) { return setConstraint(initialProgramState, booleanConstraint, new HashSet<>(initialProgramState.knownRelations())); } RelationalSymbolicValue(Kind kind); @VisibleForTesting  RelationalSymbolicValue(Kind kind, SymbolicValue leftOp, SymbolicValue rightOp); @Override List<ProgramState> setConstraint(ProgramState initialProgramState, BooleanConstraint booleanConstraint); @Override boolean equals(Object o); boolean isEquality(); @Override int hashCode(); @Override String toString(); @VisibleForTesting Kind kind();  }
@Test void test_conjuction_equal() throws Exception { RelationalSymbolicValue aLEb = relationalSV(Tree.Kind.LESS_THAN_OR_EQUAL_TO, a, b); RelationalSymbolicValue bLEa = relationalSV(Tree.Kind.LESS_THAN_OR_EQUAL_TO, b, a); RelationalSymbolicValue aEb = relationalSV(Tree.Kind.EQUAL_TO, a, b); ProgramState state = Iterables.getOnlyElement(aEb.setConstraint(stateWithRelations(aLEb, bLEa), TRUE)); assertThat(state.getConstraint(aEb, BooleanConstraint.class)).isEqualTo(TRUE); }
@Test void test_chained_transitivity() throws Exception { int chainLength = 45; SymbolicValue[] sv = new SymbolicValue[chainLength]; RelationalSymbolicValue[] given = new RelationalSymbolicValue[chainLength - 1]; sv[0] = new SymbolicValue(); for (int i = 1; i < chainLength; i++) { sv[i] = new SymbolicValue(); given[i - 1] = relationalSV(Tree.Kind.LESS_THAN, sv[i - 1], sv[i]); } RelationalSymbolicValue firstLessThanLast = relationalSV(Tree.Kind.LESS_THAN, sv[0], sv[chainLength - 1]); ProgramState programState = Iterables.getOnlyElement(firstLessThanLast.setConstraint(stateWithRelations(given), TRUE)); assertThat(programState.getConstraint(firstLessThanLast, BooleanConstraint.class)).isEqualTo(TRUE); }
@Test void test_transitive_constraint_copy() throws Exception { SymbolicValue aNEb = relationalSV(Tree.Kind.NOT_EQUAL_TO, b, a); SymbolicValue bNEc = relationalSV(Tree.Kind.NOT_EQUAL_TO, c, b); ProgramState programState = ProgramState.EMPTY_STATE; List<ProgramState> programStates = aNEb.setConstraint(programState, TRUE); programState = Iterables.getOnlyElement(programStates); programStates = bNEc.setConstraint(programState, TRUE); programState = Iterables.getOnlyElement(programStates); SymbolicValue aNEc = relationalSV(Tree.Kind.NOT_EQUAL_TO, c, a); programStates = aNEc.setConstraint(programState, FALSE); assertThat(programStates).hasSize(1); programStates = aNEc.setConstraint(programState, TRUE); assertThat(programStates).hasSize(1); }
@Test void test_constraint_copy() throws Exception { ProgramState ps = ProgramState.EMPTY_STATE; SymbolicValue a = new SymbolicValue(); SymbolicValue b = new SymbolicValue(); List<ProgramState> newProgramStates = a.setConstraint(ps, ZERO); ps = Iterables.getOnlyElement(newProgramStates); SymbolicValue aGEb = relationalSV(Tree.Kind.GREATER_THAN_OR_EQUAL_TO, b, a); newProgramStates = aGEb.setConstraint(ps, TRUE); ps = Iterables.getOnlyElement(newProgramStates); assertThat(ps.getConstraint(a, DivisionByZeroCheck.ZeroConstraint.class)).isEqualTo(ZERO); assertThat(ps.getConstraint(b, DivisionByZeroCheck.ZeroConstraint.class)).isNull(); }
@Test void test_constraints_are_copied_over_transitive_relations() throws Exception { ProgramState ps = ProgramState.EMPTY_STATE; ps = Iterables.getOnlyElement(a.setConstraint(ps, ObjectConstraint.NULL)); RelationalSymbolicValue ab = relationalSV(Tree.Kind.EQUAL_TO, a, b); ps = setTrue(ps, ab); assertNullConstraint(ps, b); RelationalSymbolicValue cd = relationalSV(Tree.Kind.EQUAL_TO, c, d); ps = setTrue(ps, cd); RelationalSymbolicValue de = relationalSV(Tree.Kind.EQUAL_TO, d, e); ps = setTrue(ps, de); assertNoConstraints(ps, c); assertNoConstraints(ps, d); assertNoConstraints(ps, e); assertThat(ps.getConstraint(relationalSV(Tree.Kind.EQUAL_TO, c, e), BooleanConstraint.class)).isEqualTo(TRUE); RelationalSymbolicValue bc = relationalSV(Tree.Kind.EQUAL_TO, b, c); ps = setTrue(ps, bc); assertNullConstraint(ps, b); assertNullConstraint(ps, c); assertNullConstraint(ps, d); assertNullConstraint(ps, e); }
@Test void test_constraint_copy_of_sv_with_no_constraints_is_symmetric() throws Exception { ProgramState ps = ProgramState.EMPTY_STATE; SymbolicValue svZero = new SymbolicValue(); ps = Iterables.getOnlyElement(svZero.setConstraint(ps, ZERO)); SymbolicValue sv = new SymbolicValue(); RelationalSymbolicValue neq = new RelationalSymbolicValue(NOT_EQUAL, svZero, sv); ProgramState psWithNeq = setTrue(ps, neq); assertThat(psWithNeq.getConstraint(svZero, ZERO.getClass())).isEqualTo(ZERO); neq = new RelationalSymbolicValue(NOT_EQUAL, sv, svZero); psWithNeq = setTrue(ps, neq); assertThat(psWithNeq.getConstraint(svZero, ZERO.getClass())).isEqualTo(ZERO); }
@Test void test_constraint_copy_of_not_null_constraint() throws Exception { ProgramState ps = ProgramState.EMPTY_STATE; SymbolicValue svNotNull = new SymbolicValue(); ps = Iterables.getOnlyElement(svNotNull.setConstraint(ps, ObjectConstraint.NOT_NULL)); SymbolicValue sv = new SymbolicValue(); RelationalSymbolicValue neq = new RelationalSymbolicValue(NOT_EQUAL, svNotNull, sv); ProgramState result = setTrue(ps, neq); assertNoConstraints(result, sv); neq = new RelationalSymbolicValue(NOT_EQUAL, NULL_LITERAL, sv); result = setTrue(ps, neq); assertThat(result.getConstraint(sv, ObjectConstraint.class)).isEqualTo(ObjectConstraint.NOT_NULL); RelationalSymbolicValue eq = new RelationalSymbolicValue(EQUAL, NULL_LITERAL, sv); result = setTrue(ps, eq); assertNullConstraint(result, sv); eq = new RelationalSymbolicValue(METHOD_EQUALS, sv, svNotNull); result = setTrue(ps, eq); assertThat(result.getConstraint(sv, ObjectConstraint.class)).isEqualTo(ObjectConstraint.NOT_NULL); }
@Test void recursion_on_copy_constraint_should_stop_distilled() { ProgramState ps = ProgramState.EMPTY_STATE; SymbolicValue sv0 = new SymbolicValue(); ps = ps.addConstraint(sv0, TRUE); ps = ps.addConstraint(neq(sv0, NULL_LITERAL), TRUE); SymbolicValue sv1 = new SymbolicValue(); ps = ps.addConstraint(eq(sv1, NULL_LITERAL), TRUE); ps = ps.addConstraint(neq(sv1, sv0), TRUE); SymbolicValue sv2 = new SymbolicValue(); ps = ps.addConstraint(sv2, ObjectConstraint.NULL); ps = ps.addConstraint(eq(sv2, sv1), TRUE); RelationalSymbolicValue sv2NeqNull = neq(sv2, NULL_LITERAL); ps = ps.addConstraint(eq(sv2, sv2NeqNull), TRUE); ps = ps.addConstraint(eq(sv1, sv2NeqNull), TRUE); List<ProgramState> result = sv2NeqNull.setConstraint(ps, FALSE); assertThat(result).hasSize(1); assertThat(result.get(0).getConstraint(sv2, BooleanConstraint.class)).isEqualTo(BooleanConstraint.FALSE); }