1import claripy
2
3import logging
4l = logging.getLogger('claripy.test.replacements')
5
6def test_replacement_solver():
7    sr = claripy.SolverReplacement(claripy.SolverVSA(), replace_constraints=True, complex_auto_replace=True)
8    x = claripy.BVS('x', 32)
9
10    sr.add(x + 8 == 10)
11    assert sr.max(x) == sr.min(x)
12
13    sr2 = sr.branch()
14    sr2.add(x + 8 < 2000)
15    assert sr2.max(x) == sr2.min(x) == sr.max(x)
16
17def test_contradiction():
18    sr = claripy.SolverReplacement(claripy.Solver(), replace_constraints=True)
19    x = claripy.BVS('x', 32)
20
21    sr.add(x == 10)
22    assert sr.satisfiable()
23    assert sr.eval(x, 10) == (10,)
24
25    sr.add(x == 100)
26    assert not sr.satisfiable()
27
28def test_branching_replacement_solver():
29
30    #
31    # Simple case: replaceable thing first
32    #
33
34    x = claripy.BVS('x', 32)
35    s0 = claripy.SolverReplacement(claripy.Solver())
36    s0.add(x == 0)
37
38    s1a = s0.branch()
39    s1b = s0.branch()
40
41    s1a.add(x == 0)
42    s1b.add(x != 0)
43
44    assert s1a.satisfiable()
45    assert not s1b.satisfiable()
46
47    #
48    # Slightly more complex: different ==
49    #
50
51    x = claripy.BVS('x', 32)
52    s0 = claripy.SolverReplacement(claripy.Solver())
53    s0.add(x == 0)
54
55    s1a = s0.branch()
56    s1b = s0.branch()
57
58    s1a.add(x == 0)
59    s1b.add(x == 1)
60
61    assert s1a.satisfiable()
62    assert not s1b.satisfiable()
63
64    #
65    # Complex case: non-replaceable thing first
66    #
67
68    #x = claripy.BVS('x', 32)
69    #s0 = claripy.SolverReplacement(claripy.Solver())
70    #s0.add(x != 0)
71    #s1a = s0.branch()
72    #s1b = s0.branch()
73    #s1a.add(x != 0)
74    #s1b.add(x == 0)
75    #assert s1a.satisfiable()
76    #assert not s1b.satisfiable()
77
78if __name__ == '__main__':
79    test_branching_replacement_solver()
80    test_replacement_solver()
81    test_contradiction()
82