pcode cace actually firing now

Author: philzook58

src/kdrag/contrib/pcode/__init__.py

@@ -106,6 +106,23 @@ def getRegisterName(self) -> str:
         return f"Roff{self.offset:X}_size{self.size}"
 
 
+# Varnode by default has pointer identity. This makes dictionaries not work correctly.
+
+pypcode.Varnode.__hash__ = lambda self: hash((self.space.name, self.offset, self.size))
+
+
+def varnode_eq(self: pypcode.Varnode, other) -> bool:
+    return (
+        isinstance(other, pypcode.Varnode)
+        and self.space.name == other.space.name
+        and self.offset == other.offset
+        and self.size == other.size
+    )
+
+
+pypcode.Varnode.__eq__ = varnode_eq
+
+
 class CachedArray(NamedTuple):
     """
     CachedArray keeps some writes unapplied to the array.
@@ -163,28 +180,6 @@ def store(self, vnode: pypcode.Varnode, value: smt.BitVecRef) -> "CachedArray":
             assert all(own in cache for own in owner.values())
             return self._replace(data=data, cache=cache, owner=owner)
 
-    """
-    def flush(self, vnode) -> smt.ArrayRef:
-        offset0 = vnode.offset
-        data = self.data
-        owner = self.owner
-        cache = self.cache
-        flushed = {}
-        for i in range(vnode.size):
-            offset = offset0 + 1
-            vnode1 = owner.get(offset)
-            if vnode1 is not None and vnode1 not in flushed:
-                data = bv.store_concat(data, vnode1.offset, cache[vnode1])
-                flushed.add(vnode1)
-        return data
-
-    def flush_all(self) -> smt.ArrayRef:  # to_expr
-        data = self.data
-        for vnode, value in self.cache.items():
-            data = bv.store_concat(data, vnode.offset, value)
-        return data
-    """
-
     def read(self, vnode: pypcode.Varnode) -> smt.BitVecRef:
         if vnode in self.cache:
             return self.cache[vnode]

src/kdrag/contrib/pcode/asmspec.py

@@ -326,7 +326,7 @@ def vc(self, ctx: pcode.BinaryContext) -> smt.BoolRef:
         if isinstance(self.assertion, OutOfGas):
             return smt.BoolVal(False)
         return smt.Implies(
-            smt.And(*self.path_cond),
+            smt.simplify(smt.And(*self.path_cond)),
             substitute_state(self.assertion.expr, ctx, self.memstate, self.ghost_env),
         )
 

src/kdrag/printers/c.py

@@ -9,13 +9,30 @@
 
 
 def ctype_of_sort(s: smt.SortRef):
+    """
+    >>> ctype_of_sort(smt.ArraySort(smt.BitVecSort(8), smt.BitVecSort(32), smt.BitVecSort(16)))
+    'uint16_t**'
+    """
     if s == smt.BoolSort():
         return "bool"
-    if isinstance(s, smt.BitVecSortRef):
+    elif isinstance(s, smt.BitVecSortRef):
         if s.size() in [8, 16, 32, 64]:
             return f"uint{s.size()}_t"
         else:
             raise NotImplementedError("No support for arbitrary C int sizes", s.size())
+    elif isinstance(s, smt.ArraySortRef):
+        doms = smt.domains(s)
+        assert all(
+            isinstance(d, smt.BitVecSortRef) and d.size() in [8, 16, 32, 64]
+            for d in doms
+        )
+        range_ = ctype_of_sort(s.range())
+        return range_ + "*" * len(doms)
+    # datatypes and enums
+    # elif isinstance(s, smt.DatatypeSortRef):
+    #    if s.num_constructors() != 1:
+    #        raise NotImplementedError("No support for multi-constructor datatypes", s)
+
     else:
         raise NotImplementedError(f"Cannot convert {s} to C type")
 
@@ -100,6 +117,12 @@ def is_valid_c_identifier_strict(identifier: str) -> bool:
 def c_of_expr(
     ctx: list[smt.ExprRef], sig: list[smt.FuncDeclRef], e: smt.ExprRef
 ) -> str:
+    """
+    >>> x,y = smt.BitVecs("x y", 32)
+    >>> mem = smt.Array("mem", smt.BitVecSort(32), smt.BitVecSort(8))
+    >>> c_of_expr([x,y,mem], [], mem[x + y])
+    '(mem[(x + y)])'
+    """
     ctype_of_sort(e.sort())  # check sort is supported
     if any(e.eq(c) for c in ctx):
         assert is_valid_c_identifier_strict(e.decl().name())
@@ -115,6 +138,11 @@ def c_of_expr(
             return f"""{e.decl().name()}({", ".join(children)})"""
         elif smt.is_if(e):
             return f"({children[0]} ? {children[1]} : {children[2]})"
+        elif smt.is_select(e):
+            assert nargs == 2
+            return f"({children[0]}[{children[1]}])"
+        elif smt.is_store(e):
+            raise NotImplementedError("Store expressions not supported in C codegen", e)
         elif isinstance(e, smt.BoolRef):
             if smt.is_true(e):
                 return "true"
@@ -175,7 +203,7 @@ def cstring(name, args, body):
     return f"""\
 #include <stdint.h>
 #include <stdbool.h>
-{ctype_of_sort(body.sort())} {name}({', '.join([f"{ctype_of_sort(arg.sort())} {arg.decl().name()}" for arg in args])}){{
+{ctype_of_sort(body.sort())} {name}({", ".join([f"{ctype_of_sort(arg.sort())} {arg.decl().name()}" for arg in args])}){{
     return {c_of_expr(args, [decl], body)};
 }}
 """
@@ -225,7 +253,7 @@ def compile_c(c_code, opts=[]):
 def link(name, args, body, filename):
     ffi = cffi.FFI()
     ffi.cdef(f"""\
-    {ctype_of_sort(body.sort())} {name}({', '.join([f"{ctype_of_sort(arg.sort())}" for arg in args])});
+    {ctype_of_sort(body.sort())} {name}({", ".join([f"{ctype_of_sort(arg.sort())}" for arg in args])});
     """)
     lib = ffi.dlopen(filename)
     return lib

src/kdrag/solvers/__init__.py

@@ -454,6 +454,34 @@ def check(self):
         return self.check_tptp_status(self.res.stdout)
 
 
+"""
+class EProverSolver(BaseSolver):
+    def __init__(self):
+        new = download(
+            "https://github.com/philzook58/eprover/releases/download/E.3.2.5-ho/eprover-ho",
+            "eprover-ho",
+            "56a1dd51be0ba3194851cfb6f4ecc563c82cd5e2f5009dd1a7268af91150c9cd",
+        )
+        super().__init__()
+        self.options["format"] = "tff"
+
+    def check(self):
+        filename = "/tmp/eprover.p"
+        self.write_tptp(filename, format=self.options["format"])
+        cmd = [
+            binpath("eprover-ho"),
+            "--auto-schedule=8",
+            filename,
+        ]
+        if "timeout" in self.options:
+            cmd.extend(["--cpu-limit=" + str(self.options["timeout"] // 1000 + 1)])
+        self.res = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+        if len(self.res.stderr) > 0:
+            raise Exception("Eprover error", self.res.stderr)
+        return self.check_tptp_status(self.res.stdout)
+"""
+
+
 class EProverTHFSolver(BaseSolver):
     def check(self):
         filename = "/tmp/eprover.p"

src/kdrag/tactics.py

@@ -357,10 +357,13 @@ def __repr__(self):
             return "Nothing to do!"
         ctxrepr = pprint.pformat(self.ctx)
         goalrepr = repr(self.goal)
-        if len(ctxrepr) + len(goalrepr) <= 75:
+        totlen = len(ctxrepr) + len(goalrepr)
+        if totlen <= 75:
             goalctx = ctxrepr + " ?|= " + repr(self.goal)
-        else:
+        elif totlen <= 1000:
             goalctx = ctxrepr + "\n?|= " + repr(self.goal)
+        else:
+            return "?|= " + self.to_expr().sexpr()
         if len(self.sig) == 0:
             return goalctx
         else: