finite set. sig on ir.blocks

Author: philzook58

src/kdrag/contrib/ir/__init__.py

@@ -34,34 +34,50 @@ class Block:
     insns: list[smt.ExprRef]
 
     @classmethod
-    def of_expr(cls, e: smt.ExprRef) -> "Block":
+    def of_defined_fun(cls, f: smt.FuncDeclRef) -> "Block":
+        """
+        >>> x, y = smt.Ints("x y")
+        >>> f = kd.define("f809", [x,y], x + x + y)
+        >>> Block.of_defined_fun(f)
+        ^(Int,Int):
+        %0 = + %var0, %var0
+        %1 = + %0, %var1
+        """
+        defn = kd.kernel.defns.get(f)
+        if defn is None:
+            raise ValueError(f"Function {f} is not defined to knuckledragger")
+        else:
+            body = defn._subst_fun_body
+            return cls.of_expr(body, sig=[f.domain(i) for i in range(f.arity())])
+
+    @classmethod
+    def of_expr(cls, e: smt.ExprRef, sig=[]) -> "Block":
         """
         >>> x,y = smt.BitVecs("x y", 64)
         >>> x,y = smt.Var(1, smt.BitVecSort(64)), smt.Var(0, smt.BitVecSort(64))
         >>> z = smt.BitVec("z", 64)
-        >>> Block.of_expr(smt.If(True, (x + y)*42, x - y + z))
+        >>> Block.of_expr(smt.If(True, (x + y)*42, x - y + z), [smt.BitVecSort(64), smt.BitVecSort(64)])
         ^(bv64,bv64):
         %0 = bvadd %var1, %var0
         %1 = bvmul %0, 42
         %2 = bvsub %var1, %var0
         %3 = bvadd %2, z
         %4 = if True, %1, %3
         """
-        sig = {}
-        insns = []
-        seen = set()
-        todo = [e]
+        if not smt.is_if(e):
+            insns = []
+            seen = set()
+            todo = [e]
+        else:
+            insns = [e]
+            seen = set(e.children())
+            todo = list(e.children())
         while todo:
             e = todo.pop()
             # if smt.is_const(e) and not kd.utils.is_value(e):
             #    args.append(e)
             if smt.is_var(e):
-                idx = smt.get_var_index(e)
-                sort = sig.get(idx)
-                if sort is None:
-                    sig[idx] = e.sort()
-                else:
-                    assert sig[idx] == e.sort()
+                pass
             elif smt.is_const(e):
                 continue
             else:
@@ -70,7 +86,6 @@ def of_expr(cls, e: smt.ExprRef) -> "Block":
                     if arg not in seen:
                         seen.add(arg)
                         todo.append(arg)
-        sig = [sig[idx] for idx in range(len(sig))]
         insns.reverse()
         return cls(sig=sig, insns=insns)
 
@@ -98,7 +113,7 @@ def __repr__(self) -> str:
                 rhs = str(insn)
             else:
                 rhs = f"{insn.decl().name()} {", ".join(self.vname(arg) for arg in insn.children())}"
-            res.append(f"%{i} = {rhs}")
+            res.append(f"\t%{i} = {rhs}")
         return "\n".join(res)
 
     def succ_calls(self) -> list[smt.ExprRef]:
@@ -119,6 +134,12 @@ class Function:
     entry: Label  # smt.FuncDeclRef?
     blocks: dict[Label, Block]  # 0th block is entry. Or "entry" is entry? Naw. 0th.
 
+    @classmethod
+    def of_defined_funs(cls, funs: list[smt.FuncDeclRef]):
+        blocks = {f.name(): Block.of_defined_fun(f) for f in funs}
+        entry = funs[0].name()
+        return cls(entry=entry, blocks=blocks)
+
     def calls_of(self) -> dict[str, list[tuple[Label, smt.ExprRef]]]:
         """
         Returns a mapping from labels to a list of calls to that label
@@ -140,6 +161,14 @@ def phis(self):
             phis[label] = zip(*[call.children() for _, call in preds[label]])
         return phis
 
+    def __repr__(self) -> str:
+        res = [f"fn {self.entry} {{"]
+        for label, blk in self.blocks.items():
+            res.append(f"@{label}:")
+            res.append(str(blk))
+        res.append("}")
+        return "\n".join(res)
+
 
 @dataclass
 class Spec:

src/kdrag/contrib/pcode/__init__.py

@@ -753,6 +753,18 @@ def sym_execute(
                     todo.append((memstate1, pc1, max_insns, path_cond))  # type: ignore
         return res
 
+    def execute_block(self, memstate: MemState, addr: int) -> list[SimState]:
+        path_cond = None
+        while True:
+            states = self.sym_execute(memstate, addr, path_cond=path_cond)
+            if len(states) != 1 or states[0].pc[0] < addr:
+                return states
+            else:
+                memstate = states[0].memstate
+                (addr, pc) = states[0].pc
+                assert pc == 0
+                path_cond = states[0].path_cond
+
     def get_reg(self, memstate: MemState, regname: str) -> smt.BitVecRef:
         """
         Get the value of a register from the memstate.

src/kdrag/theories/int.py

@@ -6,6 +6,8 @@
 import kdrag.smt as smt
 
 Z = smt.IntSort()
+ZSet = smt.SetSort(Z)
+ISet = ZSet
 
 
 def induct_nat(x, P):
@@ -156,7 +158,7 @@ def induct_nat_strong(x, P):
 dvd_fact = _l.qed().forall([m, n])
 
 
-P = smt.Array("P", Z, smt.BoolSort())
+P = smt.Const("P", ZSet)  # smt.Array("P", Z, smt.BoolSort())
 search = kd.define("search", [P, n], smt.If(P[n], n, smt.If(P[-n], -n, P[n + 1])))
 choose = kd.notation.choose.define([P], search(P, 0))
 # A choice operator. Also a relative of Kleene Mu
@@ -178,3 +180,16 @@ def induct_nat_strong(x, P):
 
 # 0 <= bchoose() <= N
 bexists = kd.define("bexists", [P, N], P[bchoose(P, N)])
+
+
+A = smt.Const("A", ZSet)
+has_ub = kd.define("ZSet.has_ub", [A, y], kd.QForAll([x], A[x], x <= y))
+# closed under union,inter,etc.
+# closed upward has_ub_le
+
+
+is_ub = kd.define("ZSet.is_ub", [A], smt.Exists([x], has_ub(A, x)))
+has_lb = kd.define("ZSet.has_lb", [A, y], kd.QForAll([x], A[x], y <= x))
+is_lb = kd.define("ZSet.is_lb", [A], smt.Exists([x], has_lb(A, x)))
+# has_bounds = kd.define("has_bounds", [A,x,y], smt.And(has_ub(A,x), has_lb(A,y)))
+finite = kd.define("ZSet.finite", [A], smt.And(is_ub(A), is_lb(A)))

src/kdrag/theories/set.py

@@ -315,7 +315,9 @@ def Finite(A: smt.ArrayRef) -> smt.BoolRef:
     """
     A set is finite if it has a finite number of elements.
 
-    See https://cvc5.github.io/docs/cvc5-1.1.2/theories/sets-and-relations.html#finite-sets
+    See:
+    - https://cvc5.github.io/docs/cvc5-1.1.2/theories/sets-and-relations.html#finite-sets
+    - https://isabelle.in.tum.de/library/HOL/HOL-Library/FSet.html
 
     >>> IntSet = Set(smt.IntSort())
     >>> kd.prove(Finite(IntSet.empty))
@@ -334,6 +336,29 @@ def Finite(A: smt.ArrayRef) -> smt.BoolRef:
     # return A == smt.Lambda([x], smt.Contains(finwit(A), smt.Unit(x))
 
 
+@functools.cache
+def finite_decl(T: smt.SortRef) -> smt.FuncDeclRef:
+    """
+    Abstracted finite predicate for sets of T.
+    """
+    A = smt.Const("A", smt.SetSort(T))
+    return kd.define(f"{T.name()}.finite", [A], Finite(A))
+
+
+def finite(A):
+    doms = smt.domains(A)
+    assert len(doms) == 1
+    return finite_decl(doms[0])(A)
+
+
+@functools.cache
+def finite_empty(T: smt.SortRef) -> kd.Proof:
+    """
+    Prove that the empty set is finite for sets of T.
+    """
+    return kd.prove(finite(Set(T).empty), unfold=True)
+
+
 RSet = Set(smt.RealSort())
 IntSet = Set(smt.IntSort())
 BoolSet = Set(smt.BoolSort())