bug in 32bit pcode

Author: philzook58

src/kdrag/contrib/pcode/__init__.py

@@ -585,7 +585,7 @@ def init_mem(self) -> MemState:
         >>> ctx.get_reg(memstate, "RAX")
         RAX!...
         """
-        memstate = MemState.Const("mem0")
+        memstate = MemState.Const("mem0", bits=self.bits)
         free_offset = 0
         for name, vnode in self.ctx.registers.items():
             # interestingness heuristic on length of name

src/kdrag/contrib/pcode/asmspec.py

@@ -29,31 +29,31 @@
 .pushsection .asmspec,"a"
 .ascii "\kind \label \"\expr\" \n"
 .popsection
-\label:
+\label :
 .endm
 
 # symbolic execution start points and precondition
 .macro kd_entry label smt_bool
-kd_boolstmt "kd_entry" \label \smt_bool
+kd_boolstmt "kd_entry" \label, \smt_bool
 .endm
 
 # Assert properties
 .macro kd_assert label smt_bool
-kd_boolstmt "kd_assert" \label \smt_bool
+kd_boolstmt "kd_assert" \label, \smt_bool
 .endm
 
 .macro kd_assume label smt_bool
-kd_boolstmt "kd_assume" \label \smt_bool
+kd_boolstmt "kd_assume" \label, \smt_bool
 .endm
 
 # symbolic execution end points and postcondition
 .macro kd_exit label smt_bool 
-kd_boolstmt "kd_entry" \label \smt_bool
+kd_boolstmt "kd_entry" \label, \smt_bool
 .endm
 
 # invariant
 .macro kd_cut label smt_bool
-kd_boolstmt "kd_cut" \label \smt_bool
+kd_boolstmt "kd_cut" \label, \smt_bool
 .endm 
 
 # For manipulation of executor ghost state. Often for saving values

src/kdrag/kernel.py

@@ -47,7 +47,7 @@ def __hash__(self) -> int:
         return hash(self.thm)
 
     def _repr_html_(self):
-        return "⊦" + repr(self.thm)
+        return "⊨" + repr(self.thm)
 
     def __repr__(self):
         return "|= " + repr(self.thm)

src/kdrag/utils.py

@@ -783,6 +783,7 @@ def has_right(self) -> bool:
 class Zipper:
     """
     A zipper for traversing and modifying terms. The Zipper retains a context stack of "holes" and the current term.
+    https://en.wikipedia.org/wiki/Zipper_(data_structure)
 
     >>> x,y,z = smt.Ints("x y z")
     >>> t = smt.Lambda([x,y], (x + y) * (y + z))