23       : Context(std::make_unique<WatchedLiteralsSolver>()) {}  in DataflowAnalysisContextTest()
25   DataflowAnalysisContext Context;  member in __anond56684750111::DataflowAnalysisContextTest
30   auto &X = Context.createAtomicBoolValue();  in TEST_F()
31   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
37   auto &X = Context.createAtomicBoolValue();  in TEST_F()
38   auto &XAndX = Context.getOrCreateConjunction(X, X);  in TEST_F()
44   auto &X = Context.createAtomicBoolValue();  in TEST_F()
45   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
46   auto &XAndY1 = Context.getOrCreateConjunction(X, Y);  in TEST_F()
47   auto &XAndY2 = Context.getOrCreateConjunction(X, Y);  in TEST_F()
50   auto &YAndX = Context.getOrCreateConjunction(Y, X);  in TEST_F()
53   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
54   auto &XAndZ = Context.getOrCreateConjunction(X, Z);  in TEST_F()
60   auto &X = Context.createAtomicBoolValue();  in TEST_F()
61   auto &XOrX = Context.getOrCreateDisjunction(X, X);  in TEST_F()
67   auto &X = Context.createAtomicBoolValue();  in TEST_F()
68   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
69   auto &XOrY1 = Context.getOrCreateDisjunction(X, Y);  in TEST_F()
70   auto &XOrY2 = Context.getOrCreateDisjunction(X, Y);  in TEST_F()
73   auto &YOrX = Context.getOrCreateDisjunction(Y, X);  in TEST_F()
76   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
77   auto &XOrZ = Context.getOrCreateDisjunction(X, Z);  in TEST_F()
83   auto &X = Context.createAtomicBoolValue();  in TEST_F()
84   auto &NotX1 = Context.getOrCreateNegation(X);  in TEST_F()
85   auto &NotX2 = Context.getOrCreateNegation(X);  in TEST_F()
88   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
89   auto &NotY = Context.getOrCreateNegation(Y);  in TEST_F()
95   auto &X = Context.createAtomicBoolValue();  in TEST_F()
96   auto &XImpliesX = Context.getOrCreateImplication(X, X);  in TEST_F()
97   EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true));  in TEST_F()
102   auto &X = Context.createAtomicBoolValue();  in TEST_F()
103   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
104   auto &XImpliesY1 = Context.getOrCreateImplication(X, Y);  in TEST_F()
105   auto &XImpliesY2 = Context.getOrCreateImplication(X, Y);  in TEST_F()
108   auto &YImpliesX = Context.getOrCreateImplication(Y, X);  in TEST_F()
111   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
112   auto &XImpliesZ = Context.getOrCreateImplication(X, Z);  in TEST_F()
117   auto &X = Context.createAtomicBoolValue();  in TEST_F()
118   auto &XIffX = Context.getOrCreateIff(X, X);  in TEST_F()
119   EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true));  in TEST_F()
124   auto &X = Context.createAtomicBoolValue();  in TEST_F()
125   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
126   auto &XIffY1 = Context.getOrCreateIff(X, Y);  in TEST_F()
127   auto &XIffY2 = Context.getOrCreateIff(X, Y);  in TEST_F()
130   auto &YIffX = Context.getOrCreateIff(Y, X);  in TEST_F()
133   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
134   auto &XIffZ = Context.getOrCreateIff(X, Z);  in TEST_F()
139   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
140   auto &C = Context.createAtomicBoolValue();  in TEST_F()
141   EXPECT_FALSE(Context.flowConditionImplies(FC, C));  in TEST_F()
145   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
146   auto &C = Context.createAtomicBoolValue();  in TEST_F()
147   Context.addFlowConditionConstraint(FC, C);  in TEST_F()
148   EXPECT_TRUE(Context.flowConditionImplies(FC, C));  in TEST_F()
152   auto &FC1 = Context.makeFlowConditionToken();  in TEST_F()
153   auto &C1 = Context.createAtomicBoolValue();  in TEST_F()
154   Context.addFlowConditionConstraint(FC1, C1);  in TEST_F()
158   auto &FC2 = Context.forkFlowCondition(FC1);  in TEST_F()
159   EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));  in TEST_F()
163   auto &C2 = Context.createAtomicBoolValue();  in TEST_F()
164   Context.addFlowConditionConstraint(FC2, C2);  in TEST_F()
165   EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));  in TEST_F()
166   EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));  in TEST_F()
170   auto &C1 = Context.createAtomicBoolValue();  in TEST_F()
171   auto &C2 = Context.createAtomicBoolValue();  in TEST_F()
172   auto &C3 = Context.createAtomicBoolValue();  in TEST_F()
174   auto &FC1 = Context.makeFlowConditionToken();  in TEST_F()
175   Context.addFlowConditionConstraint(FC1, C1);  in TEST_F()
176   Context.addFlowConditionConstraint(FC1, C3);  in TEST_F()
178   auto &FC2 = Context.makeFlowConditionToken();  in TEST_F()
179   Context.addFlowConditionConstraint(FC2, C2);  in TEST_F()
180   Context.addFlowConditionConstraint(FC2, C3);  in TEST_F()
182   auto &FC3 = Context.joinFlowConditions(FC1, FC2);  in TEST_F()
183   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));  in TEST_F()
184   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));  in TEST_F()
185   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));  in TEST_F()
190   auto &FC1 = Context.makeFlowConditionToken();  in TEST_F()
191   EXPECT_TRUE(Context.flowConditionIsTautology(FC1));  in TEST_F()
194   auto &FC2 = Context.makeFlowConditionToken();  in TEST_F()
195   Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true));  in TEST_F()
196   EXPECT_TRUE(Context.flowConditionIsTautology(FC2));  in TEST_F()
199   auto &FC3 = Context.makeFlowConditionToken();  in TEST_F()
200   Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false));  in TEST_F()
201   EXPECT_FALSE(Context.flowConditionIsTautology(FC3));  in TEST_F()
204   auto &C1 = Context.createAtomicBoolValue();  in TEST_F()
205   auto &FC4 = Context.makeFlowConditionToken();  in TEST_F()
206   Context.addFlowConditionConstraint(FC4, C1);  in TEST_F()
207   EXPECT_FALSE(Context.flowConditionIsTautology(FC4));  in TEST_F()
210   auto &FC5 = Context.makeFlowConditionToken();  in TEST_F()
211   Context.addFlowConditionConstraint(  in TEST_F()
212       FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1)));  in TEST_F()
213   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));  in TEST_F()
217   auto &X = Context.createAtomicBoolValue();  in TEST_F()
218   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
219   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
220   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
221   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
224   EXPECT_TRUE(Context.equivalentBoolValues(X, X));  in TEST_F()
226   EXPECT_FALSE(Context.equivalentBoolValues(X, Y));  in TEST_F()
229   EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));  in TEST_F()
231   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
232       Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));  in TEST_F()
236       Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));  in TEST_F()
239       Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));  in TEST_F()
241   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
242       Context.getOrCreateDisjunction(X, True), True));  in TEST_F()
244   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
245       Context.getOrCreateDisjunction(X, False), X));  in TEST_F()
249       Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));  in TEST_F()
252       Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));  in TEST_F()
255       Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));  in TEST_F()
257   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
258       Context.getOrCreateConjunction(X, False), False));  in TEST_F()
262       Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),  in TEST_F()
263                                    Context.getOrCreateDisjunction(Y, X)));  in TEST_F()
266       Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),  in TEST_F()
267                                    Context.getOrCreateConjunction(Y, X)));  in TEST_F()
270   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
271       Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),  in TEST_F()
272       Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));  in TEST_F()
274   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
275       Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),  in TEST_F()
276       Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));  in TEST_F()
281   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
282   auto &Other = Context.createAtomicBoolValue();  in TEST_F()
285   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
286   Context.addFlowConditionConstraint(FC, True);  in TEST_F()
289   EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&True, &Other}}),  in TEST_F()
294   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
295   auto &Other = Context.createAtomicBoolValue();  in TEST_F()
298   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
299   Context.addFlowConditionConstraint(FC, False);  in TEST_F()
302   EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&False, &Other}}),  in TEST_F()
308   auto &X = Context.createAtomicBoolValue();  in TEST_F()
309   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
310   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
313   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
314   Context.addFlowConditionConstraint(FC, X);  in TEST_F()
318       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
319   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));  in TEST_F()
323       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
324   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));  in TEST_F()
328   auto &X = Context.createAtomicBoolValue();  in TEST_F()
329   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
330   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
333   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
334   Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));  in TEST_F()
338       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
339   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));  in TEST_F()
343       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
344   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));  in TEST_F()
348   auto &X = Context.createAtomicBoolValue();  in TEST_F()
349   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
350   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
351   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
354   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
355   Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));  in TEST_F()
359       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
360   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));  in TEST_F()
364       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
365   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));  in TEST_F()
369   auto &X = Context.createAtomicBoolValue();  in TEST_F()
370   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
371   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
372   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
375   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
376   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));  in TEST_F()
380       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
381   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));  in TEST_F()
385       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
386   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));  in TEST_F()
390   auto &X = Context.createAtomicBoolValue();  in TEST_F()
391   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
392   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
393   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
396   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
397   Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y));  in TEST_F()
401       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
402   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));  in TEST_F()
406       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
407   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));  in TEST_F()
411       Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});  in TEST_F()
412   EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True));  in TEST_F()
416       Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});  in TEST_F()
417   EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,  in TEST_F()
418                                            Context.getOrCreateNegation(X)));  in TEST_F()
422   auto &X = Context.createAtomicBoolValue();  in TEST_F()
423   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
424   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
425   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
428   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
429   Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y));  in TEST_F()
433       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});  in TEST_F()
434   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));  in TEST_F()
438       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});  in TEST_F()
439   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse,  in TEST_F()
440                                            Context.getOrCreateNegation(Y)));  in TEST_F()
444       Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});  in TEST_F()
445   EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X));  in TEST_F()
449       Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});  in TEST_F()
450   EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,  in TEST_F()
451                                            Context.getOrCreateNegation(X)));  in TEST_F()
455   auto &X = Context.createAtomicBoolValue();  in TEST_F()
456   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
457   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
458   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
459   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
462   auto &FC = Context.makeFlowConditionToken();  in TEST_F()
463   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));  in TEST_F()
465   auto &ForkedFC = Context.forkFlowCondition(FC);  in TEST_F()
466   Context.addFlowConditionConstraint(ForkedFC, Z);  in TEST_F()
471       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});  in TEST_F()
472   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
473       ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));  in TEST_F()
474   auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(  in TEST_F()
476   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));  in TEST_F()
480       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});  in TEST_F()
482       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});  in TEST_F()
484       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});  in TEST_F()
485   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));  in TEST_F()
486   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));  in TEST_F()
487   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));  in TEST_F()
491   auto &X = Context.createAtomicBoolValue();  in TEST_F()
492   auto &Y = Context.createAtomicBoolValue();  in TEST_F()
493   auto &Z = Context.createAtomicBoolValue();  in TEST_F()
494   auto &True = Context.getBoolLiteralValue(true);  in TEST_F()
495   auto &False = Context.getBoolLiteralValue(false);  in TEST_F()
498   auto &FC1 = Context.makeFlowConditionToken();  in TEST_F()
499   Context.addFlowConditionConstraint(FC1, X);  in TEST_F()
501   auto &FC2 = Context.makeFlowConditionToken();  in TEST_F()
502   Context.addFlowConditionConstraint(FC2, Y);  in TEST_F()
504   auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);  in TEST_F()
505   Context.addFlowConditionConstraint(JoinedFC, Z);  in TEST_F()
509       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});  in TEST_F()
511       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});  in TEST_F()
512   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));  in TEST_F()
513   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));  in TEST_F()
517       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});  in TEST_F()
518   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
519       JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));  in TEST_F()
524       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});  in TEST_F()
526       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});  in TEST_F()
527   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
528       JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));  in TEST_F()
529   EXPECT_TRUE(Context.equivalentBoolValues(  in TEST_F()
530       JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));  in TEST_F()
534       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});  in TEST_F()
535   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));  in TEST_F()