Merge PR #9900: [native compiler] Fix critical bug with stuck primitive projections

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot

4 files changed, 35 insertions, 2 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index c0a5b9095c..f532e1b68f 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -207,6 +207,15 @@ Conversion machines
   GH issue number: ?
   risk: 
 
+  component: primitive projections, native_compute
+  summary: stuck primitive projections computed incorrectly by native_compute
+  introduced: 1 Jun 2018, e1e7888a, ppedrot
+  impacted released versions: 8.9.0
+  impacted coqchk versions: none
+  found by: maximedenes exploiting bug #9684
+  exploit: test-suite/bugs/closed/bug_9684.v
+  GH issue number: #9684
+
 Conflicts with axioms in library
 
   component: library of real numbers
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2dab14e732..94ed288d2d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1958,7 +1958,7 @@ let compile_mind mb mind stack =
       let cargs = Array.init arity
         (fun i -> if Int.equal i proj_arg then Some ci_uid else None)
       in
-      let i = push_symbol (SymbProj (ind, j)) in
+      let i = push_symbol (SymbProj (ind, proj_arg)) in
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0b2d760ca8..0003fc7280 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -222,7 +222,12 @@ and nf_type_sort env sigma v =
   match kind_of_value v with
   | Vaccu accu -> 
       let t,s = nf_accu_type env sigma accu in
-      let s = try destSort s with DestKO -> assert false in
+      let s =
+        try
+          destSort (whd_all env s)
+        with DestKO ->
+          CErrors.anomaly (Pp.str "Value should be a sort")
+      in
       t, s
   | _ -> assert false
 
diff --git a/test-suite/bugs/closed/bug_9684.v b/test-suite/bugs/closed/bug_9684.v
new file mode 100644
index 0000000000..436a00585b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9684.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record foo := mkFoo { proj1 : bool; proj2 : bool }.
+
+Definition x := mkFoo true false.
+Definition proj x := proj2 x.
+
+Lemma oops : proj = fun x => proj1 x.
+Proof. Fail native_compute; reflexivity. Abort.
+
+(*
+Lemma bad : False.
+assert (proj1 x = proj x).
+  rewrite oops; reflexivity.
+discriminate.
+Qed.
+
+Print Assumptions bad.
+*)