Issue #196: excessive proof-checking times in .v files generated by clightgen

The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196.

The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _".  From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.

Author: xavierleroy

Changelog

@@ -24,6 +24,7 @@ Usability:
 Bug fixing:
 
 - Issue #179: clightgen produces wrong output for "switch" statements.
+- Issue #196: excessive proof times in .v files produced by clightgen.
 - Do not generate code for functions with "inline" specifier that are
   neither static nor extern, as per ISO C99.
 - Some line number information was missing for some goto labels and

exportclight/Clightdefs.v

@@ -65,8 +65,27 @@ Definition talignas (n: N) (ty: type) :=
 Definition tvolatile_alignas (n: N) (ty: type) :=
   tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
 
-Definition make_composite_env (comps: list composite_definition): composite_env :=
-  match build_composite_env comps with
-  | OK e => e
-  | Error _ => PTree.empty _
-  end.
+Definition wf_composites (types: list composite_definition) : Prop :=
+  match build_composite_env types with OK _ => True | Error _ => False end.
+
+Definition build_composite_env' (types: list composite_definition)
+                                (WF: wf_composites types)
+                             : { ce | build_composite_env types  = OK ce }.
+Proof.
+  revert WF. unfold wf_composites. case (build_composite_env types); intros.
+- exists c; reflexivity.
+- contradiction.
+Defined.
+
+Definition mkprogram (types: list composite_definition)
+                     (defs: list (ident * globdef fundef type))
+                     (public: list ident)
+                     (main: ident)
+                     (WF: wf_composites types) : Clight.program :=
+  let (ce, EQ) := build_composite_env' types WF in
+  {| prog_defs := defs;
+     prog_public := public;
+     prog_main := main;
+     prog_types := types;
+     prog_comp_env := ce;
+     prog_comp_env_eq := EQ |}.

exportclight/ExportClight.ml

@@ -550,13 +550,14 @@ let print_program p prog =
   fprintf p "Definition composites : list composite_definition :=@ ";
   print_list print_composite_definition p prog.prog_types;
   fprintf p ".@ @ ";
-  fprintf p "Definition prog : Clight.program := {|@ ";
-  fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.Ctypes.prog_defs;
-  fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.Ctypes.prog_public;
-  fprintf p "prog_main := %a;@ " ident prog.Ctypes.prog_main;
-  fprintf p "prog_types := composites;@ ";
-  fprintf p "prog_comp_env := make_composite_env composites;@ ";
-  fprintf p "prog_comp_env_eq := refl_equal _@ ";
-  fprintf p "|}.@ ";
+  fprintf p "Definition global_definitions :=@ ";
+  print_list print_ident_globdef p prog.Ctypes.prog_defs;
+  fprintf p ".@ @ ";
+  fprintf p "Definition public_idents :=@ ";
+  print_list ident p prog.Ctypes.prog_public;
+  fprintf p ".@ @ ";
+  fprintf p "Definition prog : Clight.program := @ ";
+  fprintf p "  mkprogram composites global_definitions public_idents %a Logic.I.@ @ "
+            ident prog.Ctypes.prog_main;
   print_assertions p;
   fprintf p "@]@."