diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-15 11:54:51 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-15 11:54:51 +0200 |
commit | ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee (patch) | |
tree | 8797015ad9d75bbaf6fadcdd0c418d29020120ab /exportclight/ExportClight.ml | |
parent | 0aa08f5d521401644b5c839239de97f587e0a217 (diff) | |
download | compcert-ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee.tar.gz compcert-ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee.zip |
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.
Diffstat (limited to 'exportclight/ExportClight.ml')
-rw-r--r-- | exportclight/ExportClight.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 8001dca7..3136ed54 100644 --- a/exportclight/ExportClight.ml +++ b/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 "@]@." |