From 55c8b5e43d42f0021f3f5c7e99b9e7ff8e7bd988 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Mar 2020 16:45:15 -0400 Subject: [PATCH] [draft] Preliminary support for building with Dune Dear CompCert developers, this is a proof-of-concept highlighting a full build of x86 using the Dune build system. The PR is not meant to be merged yet, but as a demonstration and to gather feedback. In particular, it has a few quirks that should be solved soon Dune upstream: - no proper configuration - mixed Coq/ML dirs require a hack - only works with Dune master IMHO, I think it would make sense to eventually finish and merge this PR, either as the main build system, or as secondary one, to be used in Coq's Continous Integration system. Dune support is very interesting for Coq developers as it allows for composed, incremental builds with Coq itself; this means a large speed-up in practice. --- .gitignore | 3 + backend/dune | 11 +++ compcert.opam | 0 cparser/dune | 4 + dune | 17 ++++ dune-project | 5 + extraction/dune.disabled | 198 +++++++++++++++++++++++++++++++++++++++ extraction/extraction.v | 45 +++++---- tools/dune | 7 ++ x86/dune | 17 ++++ x86/extractionMachdep.v | 2 + 11 files changed, 286 insertions(+), 23 deletions(-) create mode 100644 backend/dune create mode 100644 compcert.opam create mode 100644 cparser/dune create mode 100644 dune create mode 100644 dune-project create mode 100644 extraction/dune.disabled create mode 100644 tools/dune create mode 100644 x86/dune diff --git a/.gitignore b/.gitignore index e735fec3e8..1f90033841 100644 --- a/.gitignore +++ b/.gitignore @@ -82,3 +82,6 @@ .nia.cache .nra.cache .csdp.cache + +_build +.merlin diff --git a/backend/dune b/backend/dune new file mode 100644 index 0000000000..2058e3aed0 --- /dev/null +++ b/backend/dune @@ -0,0 +1,11 @@ +(rule + (targets SplitLong.v) + (action + (with-stdout-to %{targets} + (run ndfun %{dep:SplitLong.vp})))) + +(rule + (targets SelectDiv.v) + (action + (with-stdout-to %{targets} + (run ndfun %{dep:SelectDiv.vp})))) diff --git a/compcert.opam b/compcert.opam new file mode 100644 index 0000000000..e69de29bb2 diff --git a/cparser/dune b/cparser/dune new file mode 100644 index 0000000000..4968f11656 --- /dev/null +++ b/cparser/dune @@ -0,0 +1,4 @@ +(rule + (targets Parser.v) + (action + (run menhir --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check %{dep:Parser.vy}))) diff --git a/dune b/dune new file mode 100644 index 0000000000..68a8e91023 --- /dev/null +++ b/dune @@ -0,0 +1,17 @@ +(coq.theory + (name compcert) + (package compcert) + (modules :standard \ common.Subtyping x86.extractionMachdep extraction.extraction) + (flags + -w -unused-pattern-matching-variable + -w -deprecated-ident-entry + -w -deprecated-hint-rewrite-without-locality + -w -undeclared-scope)) + +(include_subdirs qualified) + +(dirs :standard \ arm powerpc riscV aarch64 x86_64 flocq) + +(env + (_ (binaries tools/ndfun.exe))) + diff --git a/dune-project b/dune-project new file mode 100644 index 0000000000..bca5efca71 --- /dev/null +++ b/dune-project @@ -0,0 +1,5 @@ +(lang dune 3.3) +(using coq 0.4) +(using menhir 2.1) + +(name compcert) diff --git a/extraction/dune.disabled b/extraction/dune.disabled new file mode 100644 index 0000000000..9fca6f7427 --- /dev/null +++ b/extraction/dune.disabled @@ -0,0 +1,198 @@ +(coq.extraction + (prelude extraction) + (extracted_modules + Allocation + Alphabet + Archi + Ascii + Asmgen + Asm + AST + Automaton + Binary + BinInt + BinNat + BinNums + BinPosDef + BinPos + Bits + BoolEqual + Bool + Bounds + Bracket + Builtins0 + Builtins1 + Builtins + Cabs + Cexec + CleanupLabels + Clight + Cminorgen + Cminor + CminorSel + Cminortyping + CombineOp + Compare_dec + Compiler + Compopts + Constprop + ConstpropOp + Conventions1 + Conventions + Cop + Coqlib + CSEdomain + CSE + Csem + Csharpminor + Cshmgen + Csyntax + Ctypes + Ctyping + Datatypes + Deadcode + Debugvar + DecidableClass + Decidableplus + DecidableType + Determinism + Digits + Equalities + EquivDec + Errors + Events + Floats + FLT + FMapAVL + FMapList + FSetAVL + FSetAVLplus + FSetInterface + Globalenvs + Grammar + Heaps + IEEE754_extra + Initializers + Inlining + Int0 + Integers + Interpreter_complete + Interpreter_correct + Interpreter + IntvSets + Iteration + Kildall + Lattice + Linearize + Linear + Lineartyping + List0 + Liveness + Locations + LTL + Mach + Machregs + Main + Maps + Memdata + Memory + Memtype + Mergesort + MSetAVL + MSetInterface + Nat + NeedDomain + NeedOp + Op + Ordered + OrderedType + OrdersAlt + OrdersFacts + Orders + OrdersTac + Parser + PeanoNat + Postorder + Registers + Renumber + Ring + Round + RTLgen + RTL + RTLtyping + SelectDiv + Selection + SelectLong + SelectOp + SimplExpr + SimplLocals + Specif + SplitLong + Stacking + Stacklayout + String0 + Switch + Tailcall + Tunneling + UnionFind + Unityping + Unusedglob + Validator_complete + Validator_safe + ValueAnalysis + ValueAOp + ValueDomain + Values + ZArith_dec + Zaux + Zbits + Zbool + Znumtheory + Zpower) + (theories compcert)) + +(include_subdirs no) + +(library + (name compcert) + (wrapped false) + (modules_without_implementation C debugTypes dwarfTypes) + (modules :standard \ Driver GCC) + (flags -w -32) + (libraries menhirLib)) + +(copy_files %{project_root}/backend/*.{ml,mli}) +(copy_files %{project_root}/common/*.{ml,mli}) +(copy_files %{project_root}/lib/*.{ml,mli,mll}) +(copy_files %{project_root}/driver/*.{ml,mli}) +(copy_files %{project_root}/cfrontend/*.{ml,mli}) +(copy_files %{project_root}/cparser/*.{ml,mli}) +(copy_files %{project_root}/cparser/pre_parser.mly) +(copy_files %{project_root}/cparser/handcrafted.messages) +(copy_files %{project_root}/cparser/Lexer.mll) +(copy_files %{project_root}/debug/*.{ml,mli}) +(copy_files %{project_root}/x86/*.{ml,mli}) + +(ocamllex Lexer Tokenize Readconfig Responsefile) +(menhir + (modules pre_parser) + (flags --table -v --no-stdlib -la 1)) + +(executable + (name Driver) + (public_name ccomp) + (modules Driver) + (libraries str unix compcert)) + +(rule + (targets pre_parser_messages.ml) + (action + (with-stdout-to %{targets} + (run menhir --table pre_parser.mly -v --no-stdlib -la 1 -v -la 2 --compile-errors %{dep:handcrafted.messages})))) + +(rule + (targets version.ml) + (action + (with-stdout-to %{targets} + (bash "cat ../VERSION | sed -e 's|\\(.*\\)=\\(.*\\)|let \\1 = \\\"\\2\\\"|g'")))) + diff --git a/extraction/extraction.v b/extraction/extraction.v index 621298f832..bdbd7a2c75 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -14,27 +14,28 @@ (* *) (* *********************************************************************) -Require Coqlib. -Require Wfsimpl. -Require DecidableClass Decidableplus. -Require AST. -Require Iteration. -Require Floats. -Require SelectLong. -Require Selection. -Require RTLgen. -Require Inlining. -Require ValueDomain. -Require Tailcall. -Require Allocation. -Require Bounds. -Require Ctypes. -Require Csyntax. -Require Ctyping. -Require Clight. -Require Compiler. -Require Parser. -Require Initializers. +From compcert Require Coqlib. +From compcert Require Wfsimpl. +From Coq Require DecidableClass. +From compcert Require Decidableplus. +From compcert Require AST. +From compcert Require Iteration. +From compcert Require Floats. +From compcert Require SelectLong. +From compcert Require Selection. +From compcert Require RTLgen. +From compcert Require Inlining. +From compcert Require ValueDomain. +From compcert Require Tailcall. +From compcert Require Allocation. +From compcert Require Bounds. +From compcert Require Ctypes. +From compcert Require Csyntax. +From compcert Require Ctyping. +From compcert Require Clight. +From compcert Require Compiler. +From compcert Require Parser. +From compcert Require Initializers. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -149,8 +150,6 @@ Set Extraction AccessOpaque. (* Go! *) -Cd "extraction". - Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000..796faf7001 --- /dev/null +++ b/tools/dune @@ -0,0 +1,7 @@ +(executable + (name ndfun) + (flags :standard -w -27) + (modules ndfun) + (libraries str)) + +(include_subdirs no) diff --git a/x86/dune b/x86/dune new file mode 100644 index 0000000000..53ae9a6279 --- /dev/null +++ b/x86/dune @@ -0,0 +1,17 @@ +(rule + (targets SelectOp.v) + (action + (with-stdout-to %{targets} + (run ndfun %{dep:SelectOp.vp})))) + +(rule + (targets ConstpropOp.v) + (action + (with-stdout-to %{targets} + (run ndfun %{dep:ConstpropOp.vp})))) + +(rule + (targets SelectLong.v) + (action + (with-stdout-to %{targets} + (run ndfun %{dep:SelectLong.vp})))) diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v index 26a3f0a74e..20c63f232d 100644 --- a/x86/extractionMachdep.v +++ b/x86/extractionMachdep.v @@ -16,6 +16,8 @@ (* Additional extraction directives specific to the x86-64 port *) +(* This was in original dune PR *) +(* From compcert Require SelectOp ConstpropOp. *) Require Archi SelectOp. (* Archi *)