001package daikon.test.inv;
002
003import static java.util.logging.Level.INFO;
004import static org.junit.Assert.assertEquals;
005import static org.junit.Assert.assertTrue;
006
007import daikon.*;
008import daikon.config.*;
009import daikon.inv.*;
010import daikon.inv.binary.twoScalar.*;
011import daikon.test.*;
012import java.util.Comparator;
013import java.util.Random;
014import junit.framework.*;
015import org.junit.BeforeClass;
016import org.junit.Test;
017
018/** Daikon unit test class. */
019@SuppressWarnings("nullness") // testing code
020public class InvariantTester {
021
022  /** prepare for tests */
023  @BeforeClass
024  public static void setUpClass() {
025    daikon.LogHelper.setupLogs(INFO);
026    FileIO.new_decl_format = true;
027  }
028
029  @SuppressWarnings("interning")
030  public VarInfo newIntVarInfo(String name) {
031    return new VarInfo(
032        name, ProglangType.INT, ProglangType.INT, VarComparabilityNone.it, VarInfoAux.getDefault());
033  }
034
035  @Test
036  public void testClassVarnameComparator() {
037    Comparator<Invariant> c = new Invariant.ClassVarnameComparator();
038
039    VarInfo[] vars = {Common.newIntVarInfo("x"), Common.newIntVarInfo("y")};
040    PptTopLevel ppt = Common.makePptTopLevel("Foo:::OBJECT", vars);
041    PptSlice slice = new PptSlice2(ppt, vars);
042
043    Invariant inv1, inv2, inv2_2, inv2_3, inv2_4, inv2_5, inv2_6, inv3, inv4, inv5, inv6;
044
045    Configuration.getInstance()
046        .apply("daikon.inv.binary.twoScalar.NumericInt.BitwiseComplement.enabled = 1");
047
048    inv1 = NumericInt.BitwiseComplement.get_proto().instantiate(slice);
049    assertEquals(0, c.compare(inv1, inv1));
050
051    inv2 = IntEqual.get_proto().instantiate(slice);
052    inv2_2 = IntNonEqual.get_proto().instantiate(slice);
053    inv2_3 = IntLessThan.get_proto().instantiate(slice);
054    inv2_4 = IntLessEqual.get_proto().instantiate(slice);
055    inv2_5 = IntGreaterThan.get_proto().instantiate(slice);
056    inv2_6 = IntGreaterEqual.get_proto().instantiate(slice);
057    assertTrue(c.compare(inv1, inv2) > 0);
058    assertTrue(c.compare(inv1, inv2_2) > 0);
059    assertTrue(c.compare(inv1, inv2_3) > 0);
060    assertTrue(c.compare(inv1, inv2_4) > 0);
061    assertTrue(c.compare(inv1, inv2_5) > 0);
062    assertTrue(c.compare(inv1, inv2_6) > 0);
063
064    inv3 = LinearBinary.get_proto().instantiate(slice);
065    assertTrue(c.compare(inv3, inv1) < 0);
066
067    inv4 = IntNonEqual.get_proto().instantiate(slice);
068    assertTrue(c.compare(inv1, inv4) > 0);
069
070    inv5 = Implication.makeImplication(ppt, inv1, inv2, false, inv1, inv2);
071    inv6 = Implication.makeImplication(ppt, inv1, inv3, false, inv1, inv3);
072    assertTrue(c.compare(inv5, inv6) < 0);
073
074    inv5 = Implication.makeImplication(ppt, inv2, inv1, false, inv2, inv1);
075    inv6 = Implication.makeImplication(ppt, inv2, inv3, false, inv2, inv3);
076    assertTrue(c.compare(inv5, inv6) > 0);
077
078    inv5 = Implication.makeImplication(ppt, inv3, inv2, false, inv3, inv2);
079    inv6 = Implication.makeImplication(ppt, inv3, inv1, false, inv3, inv1);
080    assertTrue(c.compare(inv5, inv6) < 0);
081
082    inv5 = Implication.makeImplication(ppt, inv1, inv4, false, inv1, inv4);
083    inv6 = Implication.makeImplication(ppt, inv3, inv4, false, inv3, inv4);
084    assertTrue(c.compare(inv5, inv6) > 0);
085
086    inv5 = Implication.makeImplication(ppt, inv2, inv4, false, inv2, inv4);
087    inv6 = Implication.makeImplication(ppt, inv4, inv1, false, inv4, inv1);
088    assertTrue(c.compare(inv5, inv6) < 0);
089
090    VarInfo[] vars2 = {Common.newIntVarInfo("x"), Common.newIntVarInfo("z")};
091    PptTopLevel ppt2 = Common.makePptTopLevel("Foo:::OBJECT", vars2);
092    PptSlice slice2 = new PptSlice2(ppt2, vars2);
093    inv2 = NumericInt.BitwiseComplement.get_proto().instantiate(slice2);
094    assertTrue(c.compare(inv1, inv2) < 0);
095
096    vars2[0] = Common.newIntVarInfo("a");
097    vars2[1] = Common.newIntVarInfo("y");
098    ppt2 = Common.makePptTopLevel("Foo:::OBJECT", vars2);
099    slice2 = new PptSlice2(ppt2, vars2);
100    inv2 = NumericInt.BitwiseComplement.get_proto().instantiate(slice2);
101    assertTrue(c.compare(inv1, inv2) > 0);
102  }
103
104  @Test
105  public void test_prob_is_ge() {
106    assertEquals(1.0, Invariant.prob_is_ge(0, 11), 0);
107    assertEquals(1.0, Invariant.prob_is_ge(1, 11), 0);
108    assertEquals(.9, Invariant.prob_is_ge(2, 11), 0);
109    assertEquals(.8, Invariant.prob_is_ge(3, 11), 0);
110    assertEquals(.2, Invariant.prob_is_ge(9, 11), 0);
111    assertEquals(.1, Invariant.prob_is_ge(10, 11), 0);
112    assertEquals(0.0, Invariant.prob_is_ge(11, 11), 0);
113    assertEquals(0.0, Invariant.prob_is_ge(20, 11), 0);
114  }
115
116  @Test
117  public void test_prob_and() {
118
119    assertEquals(0.0, Invariant.prob_and(0, 0), 0);
120    assertEquals(1.0, Invariant.prob_and(0, 1), 0);
121    assertEquals(1.0, Invariant.prob_and(1, 0), 0);
122    assertEquals(1.0, Invariant.prob_and(1, 1), 0);
123    assertEquals(.5, Invariant.prob_and(0, .5), 0);
124    assertEquals(.5, Invariant.prob_and(.5, 0), 0);
125    assertEquals(1.0, Invariant.prob_and(1, .5), 0);
126    assertEquals(1.0, Invariant.prob_and(.5, 1), 0);
127    assertEquals(.1, Invariant.prob_and(0, .1), 0);
128    assertEquals(.1, Invariant.prob_and(.1, 0), 0);
129    assertEquals(1.0, Invariant.prob_and(1, .1), 0);
130    assertEquals(1.0, Invariant.prob_and(.1, 1), 0);
131    assertEquals(.75, Invariant.prob_and(.5, .5), 0);
132    assertEquals(.91, Invariant.prob_and(.1, .9), 0);
133    assertEquals(.91, Invariant.prob_and(.9, .1), 0);
134
135    Random r = new Random(20010907);
136    for (int i = 0; i < 100; i++) {
137      double x = r.nextDouble();
138      double y = r.nextDouble();
139      double z = r.nextDouble();
140      double r1 = Invariant.prob_and(x, y, z);
141      double r2 = Invariant.prob_and(x, Invariant.prob_and(y, z));
142      double r3 = Invariant.prob_and(Invariant.prob_and(x, y), z);
143      assertEquals(r1, r2, .000001);
144      assertEquals(r1, r3, .000001);
145      assertEquals(r2, r3, .000001);
146    }
147  }
148
149  @Test
150  public void test_prob_or() {
151    assertEquals(0.0, Invariant.prob_or(0, 0), 0);
152    assertEquals(0.0, Invariant.prob_or(0, 1), 0);
153    assertEquals(0.0, Invariant.prob_or(1, 0), 0);
154    assertEquals(1.0, Invariant.prob_or(1, 1), 0);
155    assertEquals(0.0, Invariant.prob_or(0, .5), 0);
156    assertEquals(0.0, Invariant.prob_or(.5, 0), 0);
157    assertEquals(.5, Invariant.prob_or(1, .5), 0);
158    assertEquals(.5, Invariant.prob_or(.5, 1), 0);
159    assertEquals(0.0, Invariant.prob_or(0, .1), 0);
160    assertEquals(0.0, Invariant.prob_or(.1, 0), 0);
161    assertEquals(.1, Invariant.prob_or(1, .1), 0);
162    assertEquals(.1, Invariant.prob_or(.1, 1), 0);
163    assertEquals(.5, Invariant.prob_or(.5, .5), 0);
164    assertEquals(.1, Invariant.prob_or(.1, .9), 0);
165    assertEquals(.1, Invariant.prob_or(.9, .1), 0);
166  }
167}