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 *)