From 6470b5ef25007ece8fea5754bee204e6b5ba0312 Mon Sep 17 00:00:00 2001
From: Pip Cet <pipcet@gmail.com>
Date: Wed, 24 Feb 2021 09:25:44 +0000
Subject: [PATCH] Assert at runtime that assume's assumptions actually hold.

* src/comp.c (emit_limple_insn): Handle (assert) insns.
(Fcomp__assert): New function.
(syms_of_comp): New defsubr for above.

* lisp/emacs-lisp/comp.el (comp-passes): Add `comp-assert-assumes'
pass.
(comp-emit-assert, comp-assert-assumes-func, comp-assert-assumes):
New functions.
---
 lisp/emacs-lisp/comp.el | 40 ++++++++++++++++++++++++
 src/comp.c              | 69 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 109 insertions(+)

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 60c040926e54c..d53b8876aa8ad 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -178,6 +178,7 @@ comp-passes
                         comp-tco
                         comp-fwprop
                         comp-remove-type-hints
+                        comp-assert-assumes
                         comp-final)
   "Passes to be executed in order.")
 
@@ -3385,6 +3386,45 @@ comp-remove-type-hints
            (comp-ctxt-funcs-h comp-ctxt)))
 
 
+;;; Assert-assumes pass specific code.
+(defun comp-emit-assert (lhs assertion)
+  (let (insns)
+    (pcase assertion
+      ((and (pred comp-mvar-p))
+       (let ((f `(lambda (x y) (equal x y))))
+         (comp-add-const-to-relocs f)
+         (push `(assert ,f ,lhs ,assertion) insns)))
+      ((and (pred comp-cstr-p)))
+      (`(and . ,operands)
+       (dolist (op operands)
+         (setq insns (nconc insns (comp-emit-assert lhs op)))))
+      (`(not ,(and (pred comp-mvar-p) operand))
+       (let ((f `(lambda (x y) (not (equal x y)))))
+         (comp-add-const-to-relocs f)
+         (push `(assert ,f ,lhs ,assertion) insns))))
+    insns))
+
+(defun comp-assert-assumes-func ()
+  (cl-loop
+   for b being each hash-value of (comp-func-blocks comp-func)
+   do (comp-loop-insn-in-block b
+        (pcase insn
+          (`(assume ,(and (pred comp-mvar-p) lhs)
+                    ,rhs)
+           (let ((f `(lambda (x y) (not (equal x y)))))
+             (comp-add-const-to-relocs f)
+             (setf (cdr insn-cell)
+                   (nconc (comp-emit-assert lhs rhs)
+                          (cdr insn-cell)))))))))
+
+(defun comp-assert-assumes (_)
+  "Turn (assume ...) insns into asserts."
+  (maphash (lambda (_ f)
+             (let ((comp-func f))
+               (comp-assert-assumes-func)
+               (comp-log-func comp-func 3)))
+           (comp-ctxt-funcs-h comp-ctxt)))
+
 ;;; Final pass specific code.
 
 (defun comp-args-to-lambda-list (args)
diff --git a/src/comp.c b/src/comp.c
index a8b8ef95fa14d..2a5eebee104ed 100644
--- a/src/comp.c
+++ b/src/comp.c
@@ -2037,6 +2037,58 @@ emit_limple_insn (Lisp_Object insn)
 			       n);
       emit_cond_jump (test, target1, target2);
     }
+  else if (EQ (op, Qassert))
+    {
+      Lisp_Object callee = Qcomp__assert;
+      emit_comment (SSDATA (Fprin1_to_string (arg[0], Qnil)));
+      imm_reloc_t reloc = obj_to_reloc (arg[0]);
+      gcc_jit_rvalue *assert_args[i];
+      assert_args[0] = gcc_jit_lvalue_as_rvalue (
+	gcc_jit_context_new_array_access (comp.ctxt,
+					  NULL,
+					  reloc.array.r_val,
+					  reloc.idx));
+      for (ptrdiff_t j = 1; j < i; j++)
+	assert_args[j] = emit_mvar_rval (arg[j]);
+
+      gcc_jit_lvalue *tmp_arr =
+	gcc_jit_function_new_local (
+				    comp.func,
+				    NULL,
+				    gcc_jit_context_new_array_type
+				    (comp.ctxt,
+				     NULL,
+				     comp.lisp_obj_type,
+				     i),
+				    "local_%d");
+
+      for (ptrdiff_t j = 0; j < i; j++)
+	{
+	  gcc_jit_block_add_assignment (
+					comp.block,
+					NULL,
+					gcc_jit_context_new_array_access (
+									  comp.ctxt,
+									  NULL,
+									  gcc_jit_lvalue_as_rvalue (tmp_arr),
+									  gcc_jit_context_new_rvalue_from_int (comp.ctxt,
+													       comp.int_type,
+													       j)),
+					assert_args[j]);
+	}
+
+      gcc_jit_rvalue *call = emit_call_ref (callee,
+		     i,
+		     gcc_jit_context_new_array_access (comp.ctxt,
+						       NULL,
+						       gcc_jit_lvalue_as_rvalue (tmp_arr),
+						       comp.zero),
+		     false);
+
+      gcc_jit_block_add_eval (comp.block,
+			      NULL,
+			      call);
+    }
   else if (EQ (op, Qphi) || EQ (op, Qassume))
     {
       /* Nothing to do for phis or assumes in the backend.  */
@@ -4980,6 +5032,20 @@ DEFUN ("comp--late-register-subr", Fcomp__late_register_subr,
   return Qnil;
 }
 
+DEFUN ("comp--assert", Fcomp__assert, Scomp__assert, 1, MANY, 0,
+       doc: /* */)
+  (ptrdiff_t nargs, Lisp_Object *args)
+{
+  if (NILP (Ffuncall (nargs, args)))
+    {
+      xsignal1 (Qnative_compiler_error,
+		Fcons (build_string ("assertion failed"),
+		       Flist (nargs, args)));
+    }
+
+  return Qnil;
+}
+
 static bool
 file_in_eln_sys_dir (Lisp_Object filename)
 {
@@ -5076,6 +5142,8 @@ syms_of_comp (void)
   DEFSYM (Qdirect_call, "direct-call");
   DEFSYM (Qdirect_callref, "direct-callref");
   DEFSYM (Qassume, "assume");
+  DEFSYM (Qassert, "assert");
+  DEFSYM (Qcomp__assert, "comp--assert");
   DEFSYM (Qsetimm, "setimm");
   DEFSYM (Qreturn, "return");
   DEFSYM (Qunreachable, "unreachable");
@@ -5179,6 +5247,7 @@ syms_of_comp (void)
   defsubr (&Scomp__register_lambda);
   defsubr (&Scomp__register_subr);
   defsubr (&Scomp__late_register_subr);
+  defsubr (&Scomp__assert);
   defsubr (&Snative_elisp_load);
 
   staticpro (&comp.exported_funcs_h);
-- 
2.30.0