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}