1import unittest
2import claripy
3
4from claripy import frontend_mixins, frontends, backend_manager, backends
5from claripy.backends.backend_smtlib import BackendSMTLibBase
6from claripy.frontends.constrained_frontend import ConstrainedFrontend
7from claripy.ast.strings import String
8
9KEEP_TEST_PERFORMANT = True
10
11class TestSMTLibBackend(unittest.TestCase):
12    def get_solver(self):
13        backend_manager.backends._register_backend(BackendSMTLibBase(), 'smt', False, False)
14
15        class SolverSMT(
16            frontend_mixins.ConstraintFixerMixin,
17            frontend_mixins.ConcreteHandlerMixin,
18            frontend_mixins.ConstraintFilterMixin,
19            frontend_mixins.ConstraintDeduplicatorMixin,
20            frontend_mixins.EagerResolutionMixin,
21            frontend_mixins.SMTLibScriptDumperMixin,
22            ConstrainedFrontend
23        ):
24            def __init__(self, *args, **kwargs):
25                self._solver_backend = backend_manager.backends.smt
26                super(SolverSMT, self).__init__(*args, **kwargs)
27
28        return SolverSMT()
29
30    def test_concat(self):
31        correct_script = '''(set-logic ALL)
32(declare-fun {0}symb_concat () String)
33(assert (let ((.def_0 (str.++  "conc" {0}symb_concat))) (let ((.def_1 (= .def_0 "concrete"))) .def_1)))
34(check-sat)
35'''.format(String.STRING_TYPE_IDENTIFIER)
36        str_concrete = claripy.StringV("conc")
37        str_symbol = claripy.StringS("symb_concat", 4, explicit_name=True)
38        solver = self.get_solver()
39        res = str_concrete + str_symbol
40        solver.add(res == claripy.StringV("concrete"))
41        script = solver.get_smtlib_script_satisfiability()
42        # with open("dump_concat.smt2", "w") as dump_f:
43            # dump_f.write(script)
44        self.assertEqual(correct_script, script)
45
46    def test_concat_simplification(self):
47        correct_script = '''(set-logic ALL)
48
49
50(check-sat)
51'''
52        solver = self.get_solver()
53        str_concrete = claripy.StringV("conc")
54        res = str_concrete + str_concrete + str_concrete
55        res2 = claripy.StrConcat(str_concrete, str_concrete) + str_concrete
56        solver.add(res == res2)
57        script = solver.get_smtlib_script_satisfiability()
58        self.assertEqual(correct_script, script)
59
60    def test_substr(self):
61        correct_script = '''(set-logic ALL)
62(declare-fun {0}symb_subst () String)
63(assert (let ((.def_0 (= ( str.substr {0}symb_subst 1 2) "on"))) .def_0))
64(check-sat)
65'''.format(String.STRING_TYPE_IDENTIFIER)
66        str_symbol = claripy.StringS("symb_subst", 4, explicit_name=True)
67        solver = self.get_solver()
68        res = claripy.StrSubstr(1, 2, str_symbol) == claripy.StringV('on')
69        solver.add(res)
70        script = solver.get_smtlib_script_satisfiability()
71        # with open("dump_substr.smt2", "w") as dump_f:
72            # dump_f.write(script)
73        self.assertEqual(correct_script, script)
74
75    def test_substr_BV_concrete_index(self):
76        correct_script = '''(set-logic ALL)
77(declare-fun {0}symb_subst () String)
78(assert (let ((.def_0 (= ( str.substr {0}symb_subst 1 2) "on"))) .def_0))
79(check-sat)
80'''.format(String.STRING_TYPE_IDENTIFIER)
81        str_symbol = claripy.StringS("symb_subst", 4, explicit_name=True)
82        solver = self.get_solver()
83        bv1 = claripy.BVV(1, 32)
84        bv2 = claripy.BVV(2, 32)
85        res = claripy.StrSubstr(bv1, bv2, str_symbol) == claripy.StringV('on')
86        solver.add(res)
87        script = solver.get_smtlib_script_satisfiability()
88        # with open("dump_substr_bv_concrete.smt2", "w") as dump_f:
89            # dump_f.write(script)
90        self.assertEqual(correct_script, script)
91
92    def test_substr_BV_symbolic_index(self):
93        correct_script = '''(set-logic ALL)
94(declare-fun {0}symb_subst () String)
95(declare-fun symb_subst_count () Int)
96(declare-fun symb_subst_start_idx () Int)
97(assert (let ((.def_0 (= ( str.substr {0}symb_subst symb_subst_start_idx symb_subst_count) "on"))) .def_0))
98(check-sat)
99'''.format(String.STRING_TYPE_IDENTIFIER)
100        str_symbol = claripy.StringS("symb_subst", 4, explicit_name=True)
101        solver = self.get_solver()
102        bv1 = claripy.BVS("symb_subst_start_idx", 32, explicit_name=True)
103        bv2 = claripy.BVS("symb_subst_count", 32, explicit_name=True)
104        res = claripy.StrSubstr(bv1, bv2, str_symbol) == claripy.StringV('on')
105        solver.add(res)
106        script = solver.get_smtlib_script_satisfiability()
107        # with open("dump_substr_bv_symbolic.smt2", "w") as dump_f:
108        #     dump_f.write(script)
109        self.assertEqual(correct_script, script)
110
111    def test_substr_BV_mixed_index(self):
112        correct_script = '''(set-logic ALL)
113(declare-fun {0}symb_subst () String)
114(declare-fun symb_subst_start_idx () Int)
115(assert (let ((.def_0 (= ( str.substr {0}symb_subst symb_subst_start_idx 2) "on"))) .def_0))
116(check-sat)
117'''.format(String.STRING_TYPE_IDENTIFIER)
118        str_symbol = claripy.StringS("symb_subst", 4, explicit_name=True)
119        solver = self.get_solver()
120        bv1 = claripy.BVS("symb_subst_start_idx", 32, explicit_name=True)
121        bv2 = claripy.BVV(2, 32)
122        res = claripy.StrSubstr(bv1, bv2, str_symbol) == claripy.StringV('on')
123        solver.add(res)
124        script = solver.get_smtlib_script_satisfiability()
125        # with open("dump_substr_bv_symbolic.smt2", "w") as dump_f:
126        #     dump_f.write(script)
127        self.assertEqual(correct_script, script)
128
129    def test_substr_simplification(self):
130        correct_script = '''(set-logic ALL)
131
132
133(check-sat)
134'''
135        str_concrete = claripy.StringV("concrete")
136        solver = self.get_solver()
137        solver.add(claripy.StrSubstr(1, 2, str_concrete) == claripy.StringV('on'))
138        script = solver.get_smtlib_script_satisfiability()
139        self.assertEqual(correct_script, script)
140
141    def test_replace(self):
142        correct_script = '''(set-logic ALL)
143(declare-fun {0}symb_repl () String)
144(assert (let ((.def_0 (= ( str.replace {0}symb_repl "a" "b" ) "cbne"))) .def_0))
145(check-sat)
146'''.format(String.STRING_TYPE_IDENTIFIER)
147        str_to_replace_symb = claripy.StringS("symb_repl", 4, explicit_name=True)
148        sub_str_to_repl = claripy.StringV("a")
149        replacement = claripy.StringV("b")
150        solver = self.get_solver()
151        repl_stringa = claripy.StrReplace(str_to_replace_symb, sub_str_to_repl, replacement)
152        solver.add(repl_stringa == claripy.StringV("cbne"))
153        script = solver.get_smtlib_script_satisfiability()
154        # with open("dump_replace.smt2", "w") as dump_f:
155            # dump_f.write(script)
156        self.assertEqual(correct_script, script)
157
158    def test_replace_simplification(self):
159        correct_script = '''(set-logic ALL)
160
161
162(check-sat)
163'''
164        str_to_replace = claripy.StringV("cane")
165        sub_str_to_repl = claripy.StringV("a")
166        replacement = claripy.StringV("b")
167        repl_stringa = claripy.StrReplace(str_to_replace, sub_str_to_repl, replacement)
168        solver = self.get_solver()
169        solver.add(repl_stringa == claripy.StringV("cbne"))
170        solver = self.get_solver()
171        script = solver.get_smtlib_script_satisfiability()
172        self.assertEqual(correct_script, script)
173
174    def test_ne(self):
175        correct_script = '''(set-logic ALL)
176(declare-fun {0}symb_ne () String)
177(assert (let ((.def_0 (= {0}symb_ne "concrete"))) (let ((.def_1 (not .def_0))) .def_1)))
178(check-sat)
179'''.format(String.STRING_TYPE_IDENTIFIER)
180        str_symb = claripy.StringS("symb_ne", 12, explicit_name=True)
181        solver = self.get_solver()
182        solver.add(str_symb != claripy.StringV("concrete"))
183        script = solver.get_smtlib_script_satisfiability()
184        # with open("dump_ne.smt2", "w") as dump_f:
185        #     dump_f.write(script)
186        self.assertEqual(correct_script, script)
187
188    def test_length(self):
189        correct_script = '''(set-logic ALL)
190(declare-fun {0}symb_length () String)
191(assert (let ((.def_0 (= (str.len {0}symb_length) 14))) .def_0))
192(check-sat)
193'''.format(String.STRING_TYPE_IDENTIFIER)
194        str_symb = claripy.StringS("symb_length", 12, explicit_name=True)
195        solver = self.get_solver()
196        # TODO: How do we want to dela with the size of a symbolic string?
197        solver.add(claripy.StrLen(str_symb, 32) == 14)
198        script = solver.get_smtlib_script_satisfiability()
199        # with open("dump_length.smt2", "w") as dump_f:
200        #     dump_f.write(script)
201        self.assertEqual(correct_script, script)
202
203    def test_length_simplification(self):
204        correct_script = '''(set-logic ALL)
205
206
207(check-sat)
208'''
209        str_concrete = claripy.StringV("concrete")
210        solver = self.get_solver()
211        solver.add(claripy.StrLen(str_concrete, 32) == 8)
212        script = solver.get_smtlib_script_satisfiability()
213        self.assertEqual(correct_script, script)
214
215
216    def test_or(self):
217        correct_script = '''(set-logic ALL)
218(declare-fun {0}Symb_or () String)
219(assert (let ((.def_0 (= {0}Symb_or "ciao"))) (let ((.def_1 (= {0}Symb_or "abc"))) (let ((.def_2 (or .def_1 .def_0))) .def_2))))
220(check-sat)
221'''.format(String.STRING_TYPE_IDENTIFIER)
222        str_symb = claripy.StringS("Symb_or", 4, explicit_name=True)
223        solver = self.get_solver()
224        res = claripy.Or((str_symb == claripy.StringV("abc")),
225                         (str_symb == claripy.StringV("ciao")))
226        solver.add(res)
227        script = solver.get_smtlib_script_satisfiability()
228        # with open("dump_or.smt2", "w") as dump_f:
229        #     dump_f.write(script)
230        self.assertEqual(correct_script, script)
231
232    def test_lt_etc(self):
233        correct_script = '''(set-logic ALL)
234(declare-fun {0}Symb_lt_test () String)
235(assert (let ((.def_0 (<= (str.len {0}Symb_lt_test) 4))) .def_0))
236(assert (let ((.def_0 (< (str.len {0}Symb_lt_test) 4))) .def_0))
237(assert (let ((.def_0 (<= 4 (str.len {0}Symb_lt_test)))) .def_0))
238(assert (let ((.def_0 (< 4 (str.len {0}Symb_lt_test)))) .def_0))
239(check-sat)
240'''.format(String.STRING_TYPE_IDENTIFIER)
241        str_symb = claripy.StringS("Symb_lt_test", 4, explicit_name=True)
242        solver = self.get_solver()
243        c1 = claripy.StrLen(str_symb, 32) <= 4
244        c2 = claripy.StrLen(str_symb, 32) < 4
245        c3 = claripy.StrLen(str_symb, 32) >= 4
246        c4 = claripy.StrLen(str_symb, 32) > 4
247        solver.add(c1)
248        solver.add(c2)
249        solver.add(c3)
250        solver.add(c4)
251        script = solver.get_smtlib_script_satisfiability()
252        # with open("dump_lt_etc.smt2", "w") as dump_f:
253        #     dump_f.write(script)
254        self.assertEqual(correct_script, script)
255
256
257    def test_contains(self):
258        correct_script = '''(set-logic ALL)
259(declare-fun {0}symb_contains () String)
260(assert ( str.contains {0}symb_contains "an"))
261(check-sat)
262'''.format(String.STRING_TYPE_IDENTIFIER)
263        str_symb = claripy.StringS("symb_contains", 4, explicit_name=True)
264        res = claripy.StrContains(str_symb, claripy.StringV("an"))
265        solver = self.get_solver()
266        solver.add(res)
267        script = solver.get_smtlib_script_satisfiability()
268        # with open("dump_contains.smt2", "w") as dump_f:
269        #     dump_f.write(script)
270        self.assertEqual(correct_script, script)
271
272    def test_contains_simplification(self):
273        correct_script = '''(set-logic ALL)
274
275
276(check-sat)
277'''
278        str_concrete = claripy.StringV("concrete")
279        solver = self.get_solver()
280        res = claripy.StrContains(str_concrete, claripy.StringV("nc"))
281        solver.add(res)
282        script = solver.get_smtlib_script_satisfiability()
283        self.assertEqual(correct_script, script)
284
285
286    def test_prefix(self):
287        correct_script = '''(set-logic ALL)
288(declare-fun {0}symb_prefix () String)
289(assert ( str.prefixof "an" {0}symb_prefix ))
290(check-sat)
291'''.format(String.STRING_TYPE_IDENTIFIER)
292        str_symb = claripy.StringS("symb_prefix", 4, explicit_name=True)
293        res = claripy.StrPrefixOf(claripy.StringV("an"), str_symb)
294        solver = self.get_solver()
295        solver.add(res)
296        script = solver.get_smtlib_script_satisfiability()
297        # with open("dump_prefix.smt2", "w") as dump_f:
298        #     dump_f.write(script)
299        self.assertEqual(correct_script, script)
300
301    def test_suffix(self):
302        correct_script = '''(set-logic ALL)
303(declare-fun {0}symb_suffix () String)
304(assert ( str.suffixof "an" {0}symb_suffix ))
305(check-sat)
306'''.format(String.STRING_TYPE_IDENTIFIER)
307        str_symb = claripy.StringS("symb_suffix", 4, explicit_name=True)
308        res = claripy.StrSuffixOf(claripy.StringV("an"), str_symb)
309        solver = self.get_solver()
310        solver.add(res)
311        script = solver.get_smtlib_script_satisfiability()
312        # with open("dump_suffix.smt2", "w") as dump_f:
313        #     dump_f.write(script)
314        self.assertEqual(correct_script, script)
315
316    def test_prefix_simplification(self):
317        correct_script = '''(set-logic ALL)
318
319
320(check-sat)
321'''
322        str_concrete = claripy.StringV("concrete")
323        solver = self.get_solver()
324        res = claripy.StrPrefixOf(claripy.StringV("conc"), str_concrete)
325        solver.add(res)
326        script = solver.get_smtlib_script_satisfiability()
327        self.assertEqual(correct_script, script)
328
329    def test_suffix_simplification(self):
330        correct_script = '''(set-logic ALL)
331
332
333(check-sat)
334'''
335        str_concrete = claripy.StringV("concrete")
336        solver = self.get_solver()
337        res = claripy.StrSuffixOf(claripy.StringV("rete"), str_concrete)
338        solver.add(res)
339        script = solver.get_smtlib_script_satisfiability()
340        self.assertEqual(correct_script, script)
341
342    def test_index_of(self):
343        correct_script = '''(set-logic ALL)
344(declare-fun {0}symb_suffix () String)
345(assert ( str.indexof {0}symb_suffix "an" 0 ))
346(check-sat)
347'''.format(String.STRING_TYPE_IDENTIFIER)
348        str_symb = claripy.StringS("symb_suffix", 4, explicit_name=True)
349        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), 0, 32)
350        solver = self.get_solver()
351        solver.add(res)
352        script = solver.get_smtlib_script_satisfiability()
353        # with open("dump_suffix.smt2", "w") as dump_f:
354        #     dump_f.write(script)
355        self.assertEqual(correct_script, script)
356
357    def test_index_of_simplification(self):
358        correct_script = '''(set-logic ALL)
359
360
361(check-sat)
362'''
363        str_concrete = claripy.StringV("concrete")
364        solver = self.get_solver()
365        res = claripy.StrIndexOf(str_concrete, claripy.StringV("rete"), 0, 32)
366        solver.add(res == 4)
367        script = solver.get_smtlib_script_satisfiability()
368        self.assertEqual(correct_script, script)
369
370    def test_index_of_symbolic_start_idx(self):
371        correct_script = '''(set-logic ALL)
372(declare-fun {0}symb_index_of () String)
373(declare-fun symb_start_idx () Int)
374(assert (let ((.def_0 (< 32 symb_start_idx))) .def_0))
375(assert (let ((.def_0 (< symb_start_idx 35))) .def_0))
376(assert (let ((.def_0 (= ( str.indexof {0}symb_index_of "an" symb_start_idx ) 33))) .def_0))
377(check-sat)
378'''.format(String.STRING_TYPE_IDENTIFIER)
379        str_symb = claripy.StringS("symb_index_of", 4, explicit_name=True)
380        start_idx = claripy.BVS("symb_start_idx", 32, explicit_name=True)
381
382        solver = self.get_solver()
383
384        solver.add(start_idx > 32)
385        solver.add(start_idx < 35)
386        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), start_idx, 32)
387
388        solver.add(res == 33)
389        script = solver.get_smtlib_script_satisfiability()
390        # with open("dump_suffix.smt2", "w") as dump_f:
391        #     dump_f.write(script)
392        self.assertEqual(correct_script, script)
393
394    def test_str_to_int(self):
395        correct_script = '''(set-logic ALL)
396(declare-fun {0}symb_strtoint () String)
397(assert (let ((.def_0 (= ( str.to.int {0}symb_strtoint ) 12))) .def_0))
398(check-sat)
399'''.format(String.STRING_TYPE_IDENTIFIER)
400        str_symb = claripy.StringS("symb_strtoint", 4, explicit_name=True)
401        res = claripy.StrToInt(str_symb, 32)
402        solver = self.get_solver()
403        solver.add(res == 12)
404        script = solver.get_smtlib_script_satisfiability()
405        # with open("dump_strtoint.smt2", "w") as dump_f:
406        #     dump_f.write(script)
407        self.assertEqual(correct_script, script)
408
409    def test_str_to_int_simplification(self):
410        correct_script = '''(set-logic ALL)
411
412
413(check-sat)
414'''
415        str_concrete = claripy.StringV("12")
416        solver = self.get_solver()
417        res = claripy.StrToInt(str_concrete, 32)
418        solver.add(res == 12)
419        script = solver.get_smtlib_script_satisfiability()
420        self.assertEqual(correct_script, script)
421
422    def test_str_extract(self):
423        correct_script = '''(set-logic ALL)
424(declare-fun STRING_symb_str_extract () String)
425(assert (let ((.def_0 (= ( str.substr STRING_symb_str_extract 5 1) "abc"))) .def_0))
426(check-sat)
427'''
428        str_symb = claripy.StringS("symb_str_extract", 12, explicit_name=True)
429        res = claripy.StrExtract(0, 1, claripy.StrExtract(1, 2, claripy.StrExtract(4, 8, str_symb)))
430        solver = self.get_solver()
431        solver.add(res == claripy.StringV("abc"))
432        script = solver.get_smtlib_script_satisfiability()
433        # with open("dump_strextract.smt2", "w") as dump_f:
434        #     dump_f.write(script)
435        self.assertEqual(correct_script, script)
436
437    def test_is_digit(self):
438        correct_script = '''(set-logic ALL)
439(declare-fun STRING_symb_str_is_digit () String)
440(assert (let ((.def_0 (= ( str.to.int STRING_symb_str_is_digit ) (- 1)))) (let ((.def_1 (not .def_0))) .def_1)))
441(check-sat)
442'''
443        str_symb = claripy.StringS("symb_str_is_digit", 12, explicit_name=True)
444        res = claripy.StrIsDigit(str_symb)
445        solver = self.get_solver()
446        solver.add(res)
447        script = solver.get_smtlib_script_satisfiability()
448        self.assertEqual(correct_script, script)
449
450    def test_is_digit_simplification(self):
451        correct_script = '''(set-logic ALL)
452
453
454(check-sat)
455'''
456        str_concrete = claripy.StringV("1")
457        res = claripy.StrIsDigit(str_concrete)
458        solver = self.get_solver()
459        solver.add(res)
460        script = solver.get_smtlib_script_satisfiability()
461        self.assertEqual(correct_script, script)
462
463    def test_int_to_str(self):
464        correct_script = '''(set-logic ALL)
465(declare-fun symb_int () Int)
466(assert (let ((.def_0 (= ( int.to.str symb_int ) "12"))) .def_0))
467(check-sat)
468'''
469        int_symb = claripy.BVS("symb_int", 32, explicit_name=True)
470        res = claripy.IntToStr(int_symb)
471        solver = self.get_solver()
472        solver.add(res == claripy.StringV("12"))
473        script = solver.get_smtlib_script_satisfiability()
474        self.assertEqual(correct_script, script)
475
476    def test_int_to_str_simplification(self):
477        correct_script = '''(set-logic ALL)
478
479
480(check-sat)
481'''
482        int_concrete = claripy.BVV(0xc, 32)
483        res = claripy.IntToStr(int_concrete)
484        solver = self.get_solver()
485        solver.add(res == claripy.StringV("12"))
486        script = solver.get_smtlib_script_satisfiability()
487        self.assertEqual(correct_script, script)
488
489if __name__ == "__main__":
490    suite = unittest.TestLoader().loadTestsFromTestCase(TestSMTLibBackend)
491    unittest.TextTestRunner(verbosity=2).run(suite)
492