Skip to content

Commit

Permalink
Refactor tests to use unittest
Browse files Browse the repository at this point in the history
  • Loading branch information
twizmwazin committed Jun 28, 2024
1 parent e246433 commit d82197f
Show file tree
Hide file tree
Showing 19 changed files with 2,224 additions and 2,393 deletions.
24 changes: 11 additions & 13 deletions tests/common_backend_smt_solver.py
Original file line number Diff line number Diff line change
@@ -1,29 +1,27 @@
from unittest import skip
import typing
import unittest

from decorator import decorator
from test_backend_smt import TestSMTLibBackend

import claripy


# use of decorator instead of the usual pattern is important because nose2 will check the argspec and wraps does not
# preserve that!
@decorator
def if_installed(f, *args, **kwargs):
try:
return f(*args, **kwargs)
except claripy.errors.MissingSolverError:
return skip("Missing Solver")(f)
def if_installed(test_func: typing.Callable):
def wrapper(*args, **kwargs):
try:
return test_func(*args, **kwargs)
except claripy.errors.MissingSolverError as exception:
raise unittest.SkipTest from exception

return wrapper


KEEP_TEST_PERFORMANT = True


class SmtLibSolverTestBase(TestSMTLibBackend):
@skip
def get_solver(self):
pass
# raise NotImplementedError
raise NotImplementedError

@if_installed
def test_concat(self):
Expand Down
278 changes: 134 additions & 144 deletions tests/test_annotations.py
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
# pylint:disable=missing-class-docstring,multiple-statements
# pylint:disable=missing-class-docstring
import unittest

import claripy


Expand Down Expand Up @@ -55,149 +57,137 @@ def apply_annotation(self, o, a):
return o + a.number


def test_backend():
x = claripy.BVV(10, 32).annotate(AnnotationA("a", 1))
assert BackendA().convert(x) == 11


def test_simplification():
x = claripy.BVS("x", 32).annotate(AnnotationA("a", 1))
y = x ^ x
assert y.depth == 1
assert len(y.annotations) == 0

x = claripy.BVS("x", 32).annotate(AnnotationB("a", 1))
y = x ^ x
assert y.depth == 2

x = claripy.BVS("x", 32).annotate(AnnotationC("a", 1))
y = x ^ x
assert y.depth == 1
assert len(y.annotations) == 1
assert y.annotations[0].number == 2


def test_missing_annotations_from_simplification():
relocatable_anno = AnnotationC("a", 2)

x0 = claripy.BVS("x", 32)
x1 = claripy.BVV(24, 32)
k = (x1 + x0).annotate(relocatable_anno)

x3 = claripy.simplify(k)

assert len(x3.annotations) == 1


def test_annotations():
x = claripy.BVS("x", 32) + 1
xx = x._apply_to_annotations(lambda a: a)
assert x is xx

a1 = AnnotationA("a", 1)
a2 = AnnotationA("a", 1)

x1 = x.annotate(a1)
x2 = x1.annotate(a2)
x2a = x.annotate(a1, a2)
x3 = x2.remove_annotation(a1)
x4 = x3.remove_annotation(a2)
x5 = x2.remove_annotations({a1, a2})

assert x.variables == x1.variables
assert x.variables == x2.variables
assert x.variables == x2a.variables
assert x.variables == x3.variables
assert x.variables == x4.variables
assert x.variables == x5.variables

assert x is not x1
assert x is not x2
assert x is not x3
assert x1 is not x2
assert x1 is not x3
assert x2 is not x3
assert x2 is x2a
assert x is x4
assert x is x5

assert x.op == x1.op
assert x.annotations == ()
assert x1.annotations == (a1,)
assert x2.annotations == (a1, a2)
assert x3.annotations == (a2,)

assert claripy.backends.z3.convert(x).eq(claripy.backends.z3.convert(x3))

const = claripy.BVV(1, 32)
consta = const.annotate(AnnotationB("a", 0))
const1 = consta + 1
const1a = const1.annotate(AnnotationB("b", 1))
const2 = const1a + 1
# const2 should be (const1a + 1), instead of (1 + 1 + 1)
# the flatten simplifier for __add__ should not be applied as AnnotationB is not relocatable (and not eliminatable)
assert const2.depth == 3


def test_eagerness():
x = claripy.BVV(10, 32).annotate(AnnotationD())
y = x + 1
assert y.annotations == x.annotations


def test_ast_hash_should_consider_relocatable_annotations():
relocatable_anno = AnnotationC("a", 2)
const = claripy.BVV(1337, 32)
x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
y0 = claripy.Concat(x0, const)

# make the annotation not relocatable
# this is of course a hack, but it can demonstrate the problem
relocatable_anno._relocatable = False
x0._relocatable_annotations = frozenset()

y1 = claripy.Concat(x0, const)

assert len(y0.annotations) == 1
assert len(y1.annotations) == 0
assert y0._hash != y1._hash


def test_remove_relocatable_annotations():
relocatable_anno = AnnotationC("a", 2)
const = claripy.BVV(1337, 32)

x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
y0 = claripy.Concat(x0, const)
assert len(y0.annotations) == 1
assert y0.annotations == (relocatable_anno,)

y1 = y0.remove_annotation(relocatable_anno)

assert len(y1.annotations) == 0


def test_duplicated_annotations_from_makelike():
relocatable_anno = AnnotationC("a", 2)

x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
x1 = claripy.BVV(24, 32)

# make_like() should not re-apply child annotations if the child is the make_like target
x2 = x0 + x1
assert len(x2.annotations) == 1

# simplify() should not re-apply annotations since annotations are kept during the simplification process by
# make_like().
x3 = claripy.simplify(x0 + x1)
assert len(x3.annotations) == 1
class TestAnnotation(unittest.TestCase):
def test_backend(self):
x = claripy.BVV(10, 32).annotate(AnnotationA("a", 1))
assert BackendA().convert(x) == 11

def test_simplification(self):
x = claripy.BVS("x", 32).annotate(AnnotationA("a", 1))
y = x ^ x
assert y.depth == 1
assert len(y.annotations) == 0

x = claripy.BVS("x", 32).annotate(AnnotationB("a", 1))
y = x ^ x
assert y.depth == 2

x = claripy.BVS("x", 32).annotate(AnnotationC("a", 1))
y = x ^ x
assert y.depth == 1
assert len(y.annotations) == 1
assert y.annotations[0].number == 2

def test_missing_annotations_from_simplification(self):
relocatable_anno = AnnotationC("a", 2)

x0 = claripy.BVS("x", 32)
x1 = claripy.BVV(24, 32)
k = (x1 + x0).annotate(relocatable_anno)

x3 = claripy.simplify(k)

assert len(x3.annotations) == 1

def test_annotations(self):
x = claripy.BVS("x", 32) + 1
xx = x._apply_to_annotations(lambda a: a)
assert x is xx

a1 = AnnotationA("a", 1)
a2 = AnnotationA("a", 1)

x1 = x.annotate(a1)
x2 = x1.annotate(a2)
x2a = x.annotate(a1, a2)
x3 = x2.remove_annotation(a1)
x4 = x3.remove_annotation(a2)
x5 = x2.remove_annotations({a1, a2})

assert x.variables == x1.variables
assert x.variables == x2.variables
assert x.variables == x2a.variables
assert x.variables == x3.variables
assert x.variables == x4.variables
assert x.variables == x5.variables

assert x is not x1
assert x is not x2
assert x is not x3
assert x1 is not x2
assert x1 is not x3
assert x2 is not x3
assert x2 is x2a
assert x is x4
assert x is x5

assert x.op == x1.op
assert x.annotations == ()
assert x1.annotations == (a1,)
assert x2.annotations == (a1, a2)
assert x3.annotations == (a2,)

assert claripy.backends.z3.convert(x).eq(claripy.backends.z3.convert(x3))

const = claripy.BVV(1, 32)
consta = const.annotate(AnnotationB("a", 0))
const1 = consta + 1
const1a = const1.annotate(AnnotationB("b", 1))
const2 = const1a + 1
# const2 should be (const1a + 1), instead of (1 + 1 + 1)
# the flatten simplifier for __add__ should not be applied as AnnotationB is not relocatable (and not eliminatable)
assert const2.depth == 3

def test_eagerness(self):
x = claripy.BVV(10, 32).annotate(AnnotationD())
y = x + 1
assert y.annotations == x.annotations

def test_ast_hash_should_consider_relocatable_annotations(self):
relocatable_anno = AnnotationC("a", 2)
const = claripy.BVV(1337, 32)
x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
y0 = claripy.Concat(x0, const)

# make the annotation not relocatable
# this is of course a hack, but it can demonstrate the problem
relocatable_anno._relocatable = False
x0._relocatable_annotations = frozenset()

y1 = claripy.Concat(x0, const)

assert len(y0.annotations) == 1
assert len(y1.annotations) == 0
assert y0._hash != y1._hash

def test_remove_relocatable_annotations(self):
relocatable_anno = AnnotationC("a", 2)
const = claripy.BVV(1337, 32)

x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
y0 = claripy.Concat(x0, const)
assert len(y0.annotations) == 1
assert y0.annotations == (relocatable_anno,)

y1 = y0.remove_annotation(relocatable_anno)

assert len(y1.annotations) == 0

def test_duplicated_annotations_from_makelike(self):
relocatable_anno = AnnotationC("a", 2)

x0 = claripy.BVS("x", 32).annotate(relocatable_anno)
x1 = claripy.BVV(24, 32)

# make_like() should not re-apply child annotations if the child is the make_like target
x2 = x0 + x1
assert len(x2.annotations) == 1

# simplify() should not re-apply annotations since annotations are kept during the simplification process by
# make_like().
x3 = claripy.simplify(x0 + x1)
assert len(x3.annotations) == 1


if __name__ == "__main__":
test_annotations()
test_backend()
test_eagerness()
test_ast_hash_should_consider_relocatable_annotations()
test_remove_relocatable_annotations()
test_duplicated_annotations_from_makelike()
test_simplification()
unittest.main()
61 changes: 31 additions & 30 deletions tests/test_ast.py
Original file line number Diff line number Diff line change
@@ -1,36 +1,37 @@
import claripy


def test_lite_repr():
one = claripy.BVV(1, 8)
two = claripy.BVV(2, 8)
a = claripy.BVS("a", 8, explicit_name=True)
b = claripy.BVS("b", 8, explicit_name=True)

assert (a + one * b + two).shallow_repr() == "<BV8 a + 1 * b + 2>"
assert ((a + one) * (b + two)).shallow_repr() == "<BV8 (a + 1) * (b + 2)>"
assert (a * one + b * two).shallow_repr() == "<BV8 a * 1 + b * 2>"
assert (
(one + a) * (two + b) + (two + a) * (one + b)
).shallow_repr() == "<BV8 (1 + a) * (2 + b) + (2 + a) * (1 + b)>"
import unittest

import claripy

def test_associativity():
x = claripy.BVS("x", 8, explicit_name=True)
y = claripy.BVS("y", 8, explicit_name=True)
z = claripy.BVS("z", 8, explicit_name=True)
w = claripy.BVS("w", 8, explicit_name=True)

assert (x - (y - (z - w))).shallow_repr() == "<BV8 x - (y - (z - w))>"
assert (x - y - z - w).shallow_repr() == "<BV8 x - y - z - w>"
assert (x * (y * (z * w))).shallow_repr() == (x * y * z * w).shallow_repr()
assert (x * y * z * w).shallow_repr() == "<BV8 x * y * z * w>"
assert (x + y - z - w).shallow_repr() == "<BV8 x + y - z - w>"
assert (x + (y - (z - w))).shallow_repr() == "<BV8 x + (y - (z - w))>"
assert (x * y / z % w).shallow_repr() == "<BV8 x * y / z % w>"
assert (x * (y / (z % w))).shallow_repr() == "<BV8 x * (y / (z % w))>"
class TestAST(unittest.TestCase):
def test_lite_repr(self):
one = claripy.BVV(1, 8)
two = claripy.BVV(2, 8)
a = claripy.BVS("a", 8, explicit_name=True)
b = claripy.BVS("b", 8, explicit_name=True)

assert (a + one * b + two).shallow_repr() == "<BV8 a + 1 * b + 2>"
assert ((a + one) * (b + two)).shallow_repr() == "<BV8 (a + 1) * (b + 2)>"
assert (a * one + b * two).shallow_repr() == "<BV8 a * 1 + b * 2>"
assert (
(one + a) * (two + b) + (two + a) * (one + b)
).shallow_repr() == "<BV8 (1 + a) * (2 + b) + (2 + a) * (1 + b)>"

def test_associativity(self):
x = claripy.BVS("x", 8, explicit_name=True)
y = claripy.BVS("y", 8, explicit_name=True)
z = claripy.BVS("z", 8, explicit_name=True)
w = claripy.BVS("w", 8, explicit_name=True)

assert (x - (y - (z - w))).shallow_repr() == "<BV8 x - (y - (z - w))>"
assert (x - y - z - w).shallow_repr() == "<BV8 x - y - z - w>"
assert (x * (y * (z * w))).shallow_repr() == (x * y * z * w).shallow_repr()
assert (x * y * z * w).shallow_repr() == "<BV8 x * y * z * w>"
assert (x + y - z - w).shallow_repr() == "<BV8 x + y - z - w>"
assert (x + (y - (z - w))).shallow_repr() == "<BV8 x + (y - (z - w))>"
assert (x * y / z % w).shallow_repr() == "<BV8 x * y / z % w>"
assert (x * (y / (z % w))).shallow_repr() == "<BV8 x * (y / (z % w))>"


if __name__ == "__main__":
test_lite_repr()
test_associativity()
unittest.main()
Loading

0 comments on commit d82197f

Please sign in to comment.