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/Clightdefs.v | |
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/Clightdefs.v')
-rw-r--r-- | exportclight/Clightdefs.v | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index fda5bb55..1124fae8 100644 --- a/exportclight/Clightdefs.v +++ b/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 |}. |