diff --git a/.gitignore b/.gitignore index cb9e4a336d..fb44a46a54 100644 --- a/.gitignore +++ b/.gitignore @@ -85,3 +85,8 @@ .nia.cache .nra.cache .csdp.cache + +# Dune Build Results +_build/ +*.install +*.opam \ No newline at end of file diff --git a/MenhirLib/dune b/MenhirLib/dune new file mode 100644 index 0000000000..3fd4824b24 --- /dev/null +++ b/MenhirLib/dune @@ -0,0 +1,9 @@ +(coq.theory + (name MenhirLib) + (package MenhirLib) + ; can only be addressed upstream + (flags -w -deprecated-syntactic-definition) + (modules_flags + (Interpreter (:standard -w -undeclared-scope)))) + +(include_subdirs qualified) \ No newline at end of file diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index 78eb363fba..c7343dc685 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -16,7 +16,7 @@ (* Additional extraction directives specific to the AArch64 port *) -Require Archi Asm Asmgen SelectOp. +From compcert Require Archi Asm Asmgen SelectOp. (* Archi *) diff --git a/backend/dune b/backend/dune new file mode 100644 index 0000000000..1488227b56 --- /dev/null +++ b/backend/dune @@ -0,0 +1,11 @@ + +; apply preprocessor to .vp files +(rule + (action + (with-stdout-to SelectDiv.v + (run ndfun %{dep:SelectDiv.vp})))) + +(rule + (action + (with-stdout-to SplitLong.v + (run ndfun %{dep:SplitLong.vp})))) diff --git a/configure b/configure index a26193ff20..0ff216a759 100755 --- a/configure +++ b/configure @@ -1,5 +1,16 @@ #!/bin/sh +## This configure script now only uses the ocaml configure script internally and passes the arguments + +if ! command -v dune 2>&1 >/dev/null +then + echo "dune could not be found. required to run the configure tool." + exit 1 +fi + +dune exec tools/configure.exe -- "$@" +exit 0 + ####################################################################### # # # The Compcert verified compiler # diff --git a/cparser/dune b/cparser/dune new file mode 100644 index 0000000000..cd3de13cce --- /dev/null +++ b/cparser/dune @@ -0,0 +1,30 @@ +; menhir parser generation +; - TODO: can maybe be replaced with menhir stanza; however +; Error: I can't determine what library/executable the files produced by this stanza are part of. +; is currently produced + +;(menhir +; (modules Parser) +; (flags --coq --coq-no-version-check)) + +(rule + (targets Parser.v) + (action + (run menhir --coq --coq-no-version-check %{dep:Parser.vy}))) + +(ocamllex Lexer) + +; translate pre_parser to ml +(rule + (deps pre_parser.mly pre_parser_messages.ml) + (targets pre_parser.ml pre_parser.mli) + (action + (run menhir --table -v --no-stdlib -la 1 --explain pre_parser.mly --base pre_parser))) + +; generate error messages file based on cparser/GNUMakefile command +(rule + (targets pre_parser_messages.ml) + (action + (with-stdout-to %{targets} + ; TODO: configurable table + (run menhir --table pre_parser.mly -v --no-stdlib -la 1 -v -la 2 --compile-errors %{dep:handcrafted.messages})))) \ No newline at end of file diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000000..5cea0c53d4 --- /dev/null +++ b/doc/dune @@ -0,0 +1,8 @@ +; documentation generator +(rule + (package documentation) + (targets STAMP (dir html)) + (deps %{project_root}/extraction/compcert/Driver.exe ccomp.1 index.html style.css) + (action (with-stdout-to STAMP + (chdir %{workspace_root} + (run gen_documentation %{env:TARGET_PLATFORM=ppc}))))) \ No newline at end of file diff --git a/dune b/dune new file mode 100644 index 0000000000..e3d1e9893e --- /dev/null +++ b/dune @@ -0,0 +1,17 @@ +; .ini / .config generation rules +; For both the ini_creator and config_creator there is an implicit dependency on the binary itself, so the rule is evaluated again if the tool is changed. +(rule + (targets compcert.ini) + (action (with-stdout-to compcert.ini + (run ini_creator)))) + +(rule + (targets compcert.config) + (action (with-stdout-to compcert.config + (run config_creator)))) + +; binary shorthands +(env + ; for all build envs add tools to path -> makes them available for rules / preprocessing + (_ + (binaries tools/ndfun.exe tools/modorder.exe tools/config_to_ml.exe tools/ini_creator.exe tools/config_creator.exe tools/gen_documentation.exe))) \ No newline at end of file diff --git a/dune-project b/dune-project new file mode 100644 index 0000000000..3ca7a15caa --- /dev/null +++ b/dune-project @@ -0,0 +1,26 @@ +(lang dune 3.16) +(using coq 0.9) +(using menhir 3.0) +(using directory-targets 0.1) + +(name compcert) + +(generate_opam_files) + +(package + (name compcert) + (synopsis "Full Compcert Compiler")) + +(package + (name MenhirLib) + (synopsis "Menhir Components")) + +(package + (name Flocq) + (synopsis "Flocq Components")) + +(package + (name documentation) + (allow_empty) + (synopsis "Documentation for compcert") + (depends compcert MenhirLib Flocq)) \ No newline at end of file diff --git a/dune-workspace b/dune-workspace new file mode 100644 index 0000000000..3fa8882922 --- /dev/null +++ b/dune-workspace @@ -0,0 +1,54 @@ +(lang dune 3.16) + +; Defines different "contexts" - allows us to build all platform compilers at the same time +; by overwriting the environment variable TARGET_PLATFORM +; +; This environment variable is then used to decide, which platform code directories are used +; during compilation. +; Per default dune assumes TARGET_PLATFORM to be "ppc". + +; to specify platforms use `dune build _build/ _build/` +; to use ENV var TARGET_PLATFORM to specify platform use `dune build _build/default` + +(context default) +(context (default + (name x86_32) + (env + (_ + (env-vars + (TARGET_PLATFORM x86_32)))))) +(context (default + (name x86_64) + (env + (_ + (env-vars + (TARGET_PLATFORM x86_64)))))) + +(context (default + (name ppc) + (env + (_ + (env-vars + (TARGET_PLATFORM ppc)))))) + +(context (default + (name arm) + (env + (_ + (env-vars + (TARGET_PLATFORM arm)))))) + +(context (default + (name aarch64) + (env + (_ + (env-vars + (TARGET_PLATFORM aarch64)))))) + +(context (default + (name riscV) + (env + (_ + (env-vars + (TARGET_PLATFORM riscV)))))) + diff --git a/extraction/.gitignore b/extraction/compcert/.gitignore similarity index 100% rename from extraction/.gitignore rename to extraction/compcert/.gitignore diff --git a/extraction/compcert/dune b/extraction/compcert/dune new file mode 100644 index 0000000000..8203ad1b57 --- /dev/null +++ b/extraction/compcert/dune @@ -0,0 +1,62 @@ +(include ../shared.dune) + +; copy OCaml files from source files - only those not shared with clightgen already +; when trying to move extraction file into platform directory +(copy_files %{project_root}/platform/backend/*.{ml,mli}) +(copy_files %{project_root}/platform/TargetPlatformCopy/*.{ml,mli}) +(copy_files %{project_root}/platform/debug/*.{ml,mli}) +; This rule might get ignored by dune as extractionMachdep.v is not recognized as a explicit dependency of +; the extraction process. Error Message: Error: Can't find file extractionMachdep.v on loadpath. +; Can't depend on the copy process it, as the coq.theory stanza does not allow to specify arbitrary +; dependencies. Thus we need to explicitly tell dune to copy it over first before running extraction +; by using the rule stanza below +(copy_files %{project_root}/platform/TargetPlatformCopy/extractionMachdep.v) +(copy_files %{project_root}/platform/driver/*.{ml,mli}) +(copy_files %{project_root}/platform/common/*.{ml,mli}) + + +; generate "new" extraction.v to be able to depend on extractionMachdep for the extraction +(rule + (deps extraction.v extractionMachdep.v) + (targets extractionFull.v) + (package compcert) + (action (copy extraction.v extractionFull.v))) + + +; compile library with coq code and all relevant ml/mli files +(library + (name compcert) + ; no need to prefix imports to allow transition to dune + (wrapped false) + (package compcert) + ; runtime libraries + (modules_without_implementation c debugTypes dwarfTypes) + ; Driver is our runner which uses this library, GCC is unneeded file + (modules :standard \ Driver GCC) + (instrumentation (backend bisect_ppx)) + (flags -w -32) + (libraries menhirLib str unix)) + +; generate version.ml +(rule + (targets version.ml) + (package compcert) + (deps %{project_root}/VERSION) + (action + (with-stdout-to %{targets} + (chdir %{workspace_root} + (run config_to_ml %{deps}))))) + + +; generate final compcert executable +(executable + (name Driver) + (package compcert) + (public_name ccomp) + (modules Driver) + ; generate both bytecode and exe + (modes byte exe) + (instrumentation (backend bisect_ppx)) + (libraries compcert)) + +(include_subdirs no) \ No newline at end of file diff --git a/extraction/extraction.v b/extraction/compcert/extraction.v similarity index 89% rename from extraction/extraction.v rename to extraction/compcert/extraction.v index a714c8313a..b576e20401 100644 --- a/extraction/extraction.v +++ b/extraction/compcert/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,7 +150,7 @@ Set Extraction AccessOpaque. (* Go! *) -Cd "extraction". +(* Cd "extraction". *) Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/extraction/dune b/extraction/dune new file mode 100644 index 0000000000..2943377995 --- /dev/null +++ b/extraction/dune @@ -0,0 +1,32 @@ +; define extraction code based on env -> some modules are used only with some platforms +(subdir compcert (dynamic_include ../platform/dune.inc)) + + +; riscV +(subdir platform (rule + (action (copy riscV.dune dune.inc)) + (enabled_if (= %{env:TARGET_PLATFORM=ppc} riscV)))) + + +; arm +(subdir platform (rule + (action (copy arm.dune dune.inc)) + (enabled_if (= %{env:TARGET_PLATFORM=ppc} arm)))) + +; aarch64 +(subdir platform (rule + (action (copy aarch64.dune dune.inc)) + (enabled_if (= %{env:TARGET_PLATFORM=ppc} aarch64)))) + + + +; default, every other case is already specified +(subdir platform (rule + (action (copy default.dune dune.inc)) + (enabled_if + (not + (or + (= %{env:TARGET_PLATFORM=ppc} aarch64) + (or + (= %{env:TARGET_PLATFORM=ppc} arm) + (= %{env:TARGET_PLATFORM=ppc} riscV))))))) diff --git a/extraction/platform/aarch64.dune b/extraction/platform/aarch64.dune new file mode 100644 index 0000000000..558c7721f6 --- /dev/null +++ b/extraction/platform/aarch64.dune @@ -0,0 +1,151 @@ +; use all the relevant .v files and extract them to OCaml files +(coq.extraction + (prelude extractionFull) + (extracted_modules + Allocation + Alphabet + Archi + Ascii + Asmgen + Asm + AST + Automaton + Binary + BinarySingleNaN + BinInt + BinNat + BinNums + BinPos + BinPosDef + Bits + Bool + Bounds + 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 + Equalities + EquivDec + Errors + Events + Floats + 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 + Round + RTLgen + RTL + RTLtyping + SelectDiv + Selection + SelectLong + SelectOp + SimplExpr + SimplLocals + Specif + SpecFloat + 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) + (stdlib yes) + (theories compcert Flocq MenhirLib)) \ No newline at end of file diff --git a/extraction/platform/arm.dune b/extraction/platform/arm.dune new file mode 100644 index 0000000000..d4c62621fb --- /dev/null +++ b/extraction/platform/arm.dune @@ -0,0 +1,150 @@ +; use all the relevant .v files and extract them to OCaml files +(coq.extraction + (prelude extractionFull) + (extracted_modules + Allocation + Alphabet + Archi + Ascii + Asmgen + Asm + AST + Automaton + Binary + BinarySingleNaN + BinInt + BinNat + BinNums + BinPos + BinPosDef + Bits + Bool + Bounds + 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 + Equalities + EquivDec + Errors + Events + Floats + 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 + Round + RTLgen + RTL + RTLtyping + SelectDiv + Selection + SelectOp + SimplExpr + SimplLocals + Specif + SpecFloat + 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) + (stdlib yes) + (theories compcert Flocq MenhirLib)) \ No newline at end of file diff --git a/extraction/platform/default.dune b/extraction/platform/default.dune new file mode 100644 index 0000000000..294213a2a2 --- /dev/null +++ b/extraction/platform/default.dune @@ -0,0 +1,152 @@ +; use all the relevant .v files and extract them to OCaml files +(coq.extraction + (prelude extractionFull) + (extracted_modules + Allocation + Alphabet + Archi + Ascii + Asmgen + Asm + AST + Automaton + Binary + BinarySingleNaN + BinInt + BinNat + BinNums + BinPos + BinPosDef + Bits + Bool + BoolEqual + Bounds + 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 + Equalities + EquivDec + Errors + Events + Floats + 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 + Round + RTLgen + RTL + RTLtyping + SelectDiv + Selection + SelectLong + SelectOp + SimplExpr + SimplLocals + Specif + SpecFloat + 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) + (stdlib yes) + (theories compcert Flocq MenhirLib)) \ No newline at end of file diff --git a/extraction/platform/riscV.dune b/extraction/platform/riscV.dune new file mode 100644 index 0000000000..558c7721f6 --- /dev/null +++ b/extraction/platform/riscV.dune @@ -0,0 +1,151 @@ +; use all the relevant .v files and extract them to OCaml files +(coq.extraction + (prelude extractionFull) + (extracted_modules + Allocation + Alphabet + Archi + Ascii + Asmgen + Asm + AST + Automaton + Binary + BinarySingleNaN + BinInt + BinNat + BinNums + BinPos + BinPosDef + Bits + Bool + Bounds + 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 + Equalities + EquivDec + Errors + Events + Floats + 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 + Round + RTLgen + RTL + RTLtyping + SelectDiv + Selection + SelectLong + SelectOp + SimplExpr + SimplLocals + Specif + SpecFloat + 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) + (stdlib yes) + (theories compcert Flocq MenhirLib)) \ No newline at end of file diff --git a/extraction/shared.dune b/extraction/shared.dune new file mode 100644 index 0000000000..b3e144645f --- /dev/null +++ b/extraction/shared.dune @@ -0,0 +1,4 @@ + +(copy_files %{project_root}/platform/cfrontend/*.{ml,mli}) +(copy_files %{project_root}/platform/lib/*.{ml,mli,mll}) +(copy_files %{project_root}/platform/cparser/*.{ml,mli,mly,mll,messages}) ; load remaining parser files diff --git a/flocq/dune b/flocq/dune new file mode 100644 index 0000000000..ec3b3f523a --- /dev/null +++ b/flocq/dune @@ -0,0 +1,9 @@ +(coq.theory + (name Flocq) + (package Flocq) + ; can only be addressed upstream + (flags + -w -deprecated-syntactic-definition + -w -unused-pattern-matching-variable)) + +(include_subdirs qualified) \ No newline at end of file diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000000..4f3d59f979 --- /dev/null +++ b/lib/dune @@ -0,0 +1,2 @@ +; Convert lexer (.mll) files to .ml files +(ocamllex Readconfig Responsefile Tokenize) \ No newline at end of file diff --git a/platform/dune b/platform/dune new file mode 100644 index 0000000000..a2e774d7ad --- /dev/null +++ b/platform/dune @@ -0,0 +1,61 @@ +; Selectively compile Coq files based on TARGET_PLATFORM environment variable. +; +; We compile all Coq files using the coq.theory stanza of dune, which is very limited in selecting the modules to compile. +; One restriction is that we cannot dynamically set which modules to include in the theory, i.e. "everything from common/, backend/ & ppc/ but not arm/". +; So we resort to collecting the set of modules on the filesystem level and copy the needed directories into the platform/ directory. + +; Copy all files from currently selected architecture to "TargetPlatformCopy" directory. +; Can't copy processed .vp files from platform directories due to dependency cycle -> generate later in preprocess.dune. +; a.d. TODO are these aliases used at all? +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} ppc)) (files %{project_root}/powerpc/*))) + + +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_32)) (files %{project_root}/x86/*.{v,vp,ml,mli}))) +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_32)) (files %{project_root}/x86_32/*.{v,vp,ml,mli}))) + +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_64)) (files %{project_root}/x86/*.{v,vp,ml,mli}))) +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} x86_64)) (files %{project_root}/x86_64/*.{v,vp,ml,mli}))) + + +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} riscV)) (files %{project_root}/riscV/*))) + + +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} arm)) (files %{project_root}/arm/*))) + +(subdir TargetPlatformCopy + (copy_files (alias target_platform) (only_sources) (enabled_if (= %{env:TARGET_PLATFORM=ppc} aarch64)) (files %{project_root}/aarch64/*))) + +; copy files from all other relevant source directories +(subdir backend (copy_files %{project_root}/backend/*)) +(subdir cfrontend (copy_files %{project_root}/cfrontend/*)) +(subdir common (copy_files %{project_root}/common/*)) +(subdir cparser (copy_files %{project_root}/cparser/*)) +(subdir debug (copy_files %{project_root}/debug/*)) +(subdir driver (copy_files %{project_root}/driver/*)) +(subdir export (copy_files %{project_root}/export/*)) +(subdir lib (copy_files %{project_root}/lib/*)) + + +; Run preprocessing directives on .vp files +(include preprocess.dune) + +;Compile theory from all Coq files, excluding extraction code that is run directly during compilation. +(coq.theory + (name compcert) + (theories Flocq MenhirLib) + ; temp flag + (flags + -w -unused-pattern-matching-variable + -w -deprecated-since-8.19 + -w -deprecated-since-8.20) + (modules :standard \ common.Subtyping TargetPlatformCopy.extractionMachdep TargetPlatformCopy.extractionMachdepClight)) + +; Our Coq files are in subdirectories of platform/ so we need this for dune to compile them too. +(include_subdirs qualified) \ No newline at end of file diff --git a/platform/preprocess.dune b/platform/preprocess.dune new file mode 100644 index 0000000000..5c70586818 --- /dev/null +++ b/platform/preprocess.dune @@ -0,0 +1,22 @@ +; outsourced preprocessing of .vp files. + +; due to "only_sources" copies to TargetPlatformCopy, +; we must process target platform preprocessing here +; apply preprocessor to .vp files +(subdir TargetPlatformCopy +(rule + (action + (with-stdout-to SelectOp.v + (run ndfun %{dep:SelectOp.vp}))))) + +(subdir TargetPlatformCopy +(rule + (action + (with-stdout-to SelectLong.v + (run ndfun %{dep:SelectLong.vp}))))) + +(subdir TargetPlatformCopy +(rule + (action + (with-stdout-to ConstpropOp.v + (run ndfun %{dep:ConstpropOp.vp}))))) \ No newline at end of file diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v index 890735bad4..4eefbb0d2b 100644 --- a/riscV/extractionMachdep.v +++ b/riscV/extractionMachdep.v @@ -16,7 +16,7 @@ (* Additional extraction directives specific to the RISC-V port *) -Require Archi Asm. +From compcert Require Archi Asm. (* Archi *) diff --git a/tools/config_creator.ml b/tools/config_creator.ml new file mode 100644 index 0000000000..e24b52168c --- /dev/null +++ b/tools/config_creator.ml @@ -0,0 +1,15 @@ +open Printf +open MakefileConfig +open Version + +let _ = printf "# CompCert configuration parameters\n"; + printf "COMPCERT_ARCH=%s\n" arch; + printf "COMPCERT_MODEL=%s\n" model; + printf "COMPCERT_ABI=%s\n" abi; + printf "COMPCERT_ENDIANNESS=%s\n" endianness; + printf "COMPCERT_BITSIZE=%s\n" bitsize; + printf "COMPCERT_SYSTEM=%s\n" system; + printf "COMPCERT_VERSION=%s\n" version; + printf "COMPCERT_BUILDNR=%s\n" buildnr; + printf "COMPCERT_TAG=%s\n" tag; + printf "COMPCERT_BRANCH=%s\n" branch; diff --git a/tools/config_to_ml.ml b/tools/config_to_ml.ml new file mode 100644 index 0000000000..6555cbaefe --- /dev/null +++ b/tools/config_to_ml.ml @@ -0,0 +1,34 @@ +open Printf + +(* Module to parse config file to output in ocaml format *) + +let translate_file f = + let ic = open_in f in + try + while true do + let l = input_line ic in + (* allow for empty lines and comments *) + if not (l = "" || String.starts_with ~prefix:"#" l) then begin + let r = Str.regexp {|\([^=]*\)=\(.*\)|} in + (* line does not match *) + if not (Str.string_match r l 0) then + (* insert line as comment *) + printf "(* %s *)\n" l + else + (* identifier must be "clean" identifier according to variable identifier definition *) + let identifier = String.lowercase_ascii (Str.matched_group 1 l) in + let value = Str.matched_group 2 l in + let value_escaped_backslash = Str.global_replace (Str.regexp {|\\|}) {|\\\\|} value in + let value_escaped = Str.global_replace (Str.regexp {|"|}) {|\\"|} value_escaped_backslash in + printf "let %s = \"%s\"\n" identifier value_escaped + end + done + with End_of_file -> + close_in ic + +(* Entrypoint -> read first arg of input, should be Config Format (VERSION, Makefile.config,...) file *) +let _ = + if Array.length Sys.argv = 2 then + translate_file Sys.argv.(1) + else + invalid_arg "expected only one file name argument" \ No newline at end of file diff --git a/tools/configure.ml b/tools/configure.ml new file mode 100644 index 0000000000..f6bd2ce4fb --- /dev/null +++ b/tools/configure.ml @@ -0,0 +1,478 @@ +open Printf + + +(* Command line args parsing *) + + +let usage_msg = "Usage: ./configure [options] target +For help on options and targets, do: ./configure -help +" + +let prefix = ref "/usr/local" +let libdir = ref (!prefix ^ "/lib/compcert") +let bindir = ref (!prefix ^ "/bin") +let sharedir = ref "" +let mandir = ref (!prefix ^ "/share/man") +let toolprefix = ref "" +let ignore_coq_version = ref false +let ignore_ocaml_version = ref false +let has_runtime_lib = ref true +let has_standard_headers = ref true + +(* Only used for compiler options for .ini/.config files*) +let target = ref "" +(* let no_runtime_lib = ref false; build via package *) + +let anon_fun input = if !target = "" then + target := input else raise (Arg.Bad "Specify only one target") + + +let speclist = [ + ("-prefix", Arg.Set_string prefix, "Install in /bin and /lib/compcert"); + ("-bindir", Arg.Set_string bindir, "Install binaries in "); + ("-sharedir", Arg.Set_string sharedir, "Install configuration file in "); + ("-mandir", Arg.Set_string mandir, "Install man pages in "); + ("-libdir", Arg.Set_string libdir, "Install libraries in "); + ("-no-runtime-lib", Arg.Clear has_runtime_lib, "Do not compile nor install the runtime support library"); + ("-no-standard-headers", Arg.Clear has_standard_headers, "Do not install nor use the standard .h headers"); + ("-ignore-coq-version", Arg.Set ignore_coq_version, "Accept to use experimental or unsupported versions of Coq"); + ("-ignore-ocaml-version", Arg.Set ignore_ocaml_version, "Accept to use experimental or unsupported versions of OCaml"); + ("-toolprefix", Arg.Set_string toolprefix, "Prefix names of tools (\"gcc\", etc) with ") +] + +let _ = Arg.parse speclist anon_fun usage_msg + +(* Quits configure process *) +let invalid_input reason = + printf "Error: %s\n" reason; + printf "%s" usage_msg; + exit 2 + + +let has_double_ref = ref true +let abi_ref = ref "" + +let rec check_target_starts_with choices = match choices with + | [] -> false + | prefix::choices -> (String.starts_with ~prefix !target) || (check_target_starts_with choices) + +(* detect target data *) +let (arch, model, endianess, bitsize) = + if check_target_starts_with [ "arm-" ; "armv7a-"] then + "arm", "armv7a", "little", 32 + else if check_target_starts_with [ "armv6-"] then + "arm", "armv6", "little", 32 + else if check_target_starts_with [ "armv6t2-"] then + "arm", "armv6t2", "little", 32 + else if check_target_starts_with [ "armv7r-"] then + "arm", "armv7r", "little", 32 + else if check_target_starts_with [ "armv7m-"] then + "arm", "armv7m", "little", 32 + else if check_target_starts_with [ "armv7m+nofp.dp-"] then + (has_double_ref := false; ("arm", "armv7m", "little", 32)) + else if check_target_starts_with [ "armeb-" ; "armebv7a"] then + "arm", "armv7a", "big", 32 + else if check_target_starts_with [ "armebv6-"] then + "arm", "armv6", "big", 32 + else if check_target_starts_with [ "armebv6t2-"] then + "arm", "armv6t2", "big", 32 + else if check_target_starts_with [ "armebv7r-"] then + "arm", "armv7r", "big", 32 + else if check_target_starts_with [ "armebv7m-"] then + "arm", "armv7m", "big", 32 + else if check_target_starts_with [ "x86_32-" ; "ia32-" ; "i386-"] then + "x86", "32sse2", "little", 32 + else if check_target_starts_with [ "x86_64-" ; "amd64-"] then + "x86", "64", "little", 64 + else if check_target_starts_with [ "powerpc-" ; "ppc-"] then + "powerpc", "ppc32", "big", 32 + else if check_target_starts_with [ "powerpc64-" ; "ppc64-"] then + "powerpc", "ppc64", "big", 32 + else if check_target_starts_with [ "e5500-"] then + "powerpc", "e5500", "big", 32 + else if check_target_starts_with [ "powerpcvle-" ; "ppcvle-"] then + (has_double_ref := false; "powerpc_vle", "ppc32", "big", 32 ) + else if check_target_starts_with [ "riscv32-" ; "rv32-"] then + "riscV", "32", "little", 32 + else if check_target_starts_with [ "riscv64-" ; "rv64-"] then + "riscV", "64", "little", 64 + else if check_target_starts_with [ "aarch64-" ; "arm64-"] then + "aarch64", "default", "little", 64 + else if !target = "peaktop" then + (abi_ref := "eabi"; has_double_ref := false; "peaktop", "default", "little", 32 ) + else if !target = "tricore-eabi" || !target = "tricore-eabi-llvm" then + (abi_ref := "eabi"; has_double_ref := false; "tricore", "tc161", "little", 32) + else if !target = "manual" then + ("", "", "", 0) + else if !target = "" then + invalid_input "no target architecture specified" + else + invalid_input "unkown target architecture." + +let target_suffix = let split = Str.bounded_split (Str.regexp "-") !target 2 in + if List.length split = 2 then + List.nth split 1 + else "" + +let rec check_target_suffix_in list = match list with + | [] -> false + | suffix::list -> target_suffix = suffix || check_target_suffix_in list + +let _ = printf "arch: %s, model: %s, endianess: %s, bitsize: %d, suffix: %s\n" arch model endianess bitsize target_suffix + + +(* Target Configuration with defaults *) +let asm_supports_cfi = ref None +let cc = ref (!toolprefix ^ "gcc") +let cc_options = ref "" +let casm = ref (!toolprefix ^ "gcc") +let casm_options = ref "-c" +let casmruntime = ref "" +let clinker = ref (!toolprefix ^ "gcc") +let clinker_options = ref "" +let clinker_needs_no_pie = ref true +let cprepro = ref (!toolprefix ^ "gcc") +let cprepro_options = ref "-E" +let archiver = ref (!toolprefix ^ "ar rcs") +let libmath = ref "-lm" +let responsefile = ref "gnu" +let system = ref "" + +(* Set more flags depending on arch and target suffix *) +let _ = match arch with + | "arm" -> begin + begin if check_target_suffix_in ["eabi"; "linux"] then + abi_ref := "eabi" + else if check_target_suffix_in ["eabihf"; "hf"; "hardfloat"] then + abi_ref := "hardfloat" + else + invalid_input (sprintf "invalid eabi/system '%s' for architecture ARM." target_suffix) end; + cprepro_options := "-U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"; + system := "linux" + end + | "powerpc" | "powerpc_vle" -> begin + if check_target_suffix_in ["eabi"; "eabi-diab"; "linux"] then begin + begin if target_suffix = "linux" then + abi_ref := "linux" + else + abi_ref := "eabi" + end; + if target_suffix = "eabi-diab" then begin + asm_supports_cfi := Some false; + casm := !toolprefix ^ "das"; + casm_options := "-Xalign-value"; + cc := !toolprefix ^ "dcc"; + clinker_needs_no_pie := false; + clinker := !toolprefix ^ "dcc"; + cprepro := !toolprefix ^ "dcc"; + cprepro_options := "-E -D__GNUC__ -D__CHAR_UNSIGNED__"; + archiver := !toolprefix ^ "dar -q"; + libmath := "-lm"; + system := "diab"; + responsefile := "diab" + end else begin + casmruntime := !toolprefix ^ "gcc -c -Wa,-mregnames"; + cprepro_options := "-U__GNUC__ -E"; + system := "linux" + end + end else + invalid_input (sprintf "invalid eabi/system '%s' for architecture PowerPC/PowerPC VLE." target_suffix) + end + | "x86" when bitsize = 32 -> + if target_suffix = "bsd" then begin + abi_ref := "standard"; + cc_options := "-m32"; + casm_options := "-m32 -c"; + clinker_options := "-m32"; + cprepro_options := "-m32 -U__GNUC__ -E"; + system := "bsd" + end else if target_suffix = "linux" then begin + abi_ref := "standard"; + cc_options := "-m32"; + casm_options := "-m32 -c"; + clinker_options := "-m32"; + cprepro_options := "-m32 -U__GNUC__ -E"; + system := "linux" + end else + invalid_input (sprintf "invalid eabi/system '%s' for architecture IA32/X86_32." target_suffix) + | "x86" when bitsize = 64 -> + if target_suffix = "bsd" then begin + abi_ref := "standard"; + cc_options := "-m64"; + casm_options := "-m64 -c"; + clinker_options := "-m64"; + cprepro_options := "-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"; + system := "bsd" + end else if target_suffix = "linux" then begin + abi_ref := "standard"; + cc_options := "-m64"; + casm_options := "-m64 -c"; + clinker_options := "-m64"; + cprepro_options := "-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"; + system := "linux" + end else if check_target_suffix_in ["macos"; "macosx"] then begin + abi_ref := "macos"; + cc_options := "-arch x86_64"; + casm_options := "-arch x86_64 -c"; + clinker_options := "-arch x86_64"; + clinker_needs_no_pie := false; + cprepro_options := "-arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"; + libmath := ""; + system := "macos" + end else if target_suffix = "cygwin" then begin + abi_ref := "standard"; + cc_options := "-m64"; + casm_options := "-m64 -c"; + clinker_options := "-m64"; + cprepro_options := "-m64 -U__GNUC__ -U__SIZEOF_INT128__ '-D__attribute__(x)=' -E"; + system := "cygwin" + end else + invalid_input (sprintf "invalid eabi/system '%s' for architecture X86_64." target_suffix) + | "riscV" -> begin + let model_options = if model = "64" then + "-march=rv64imafd -mabi=lp64d" + else "-march=rv32imafd -mabi=ilp32d" in + abi_ref := "standard"; + cc_options := model_options; + casm_options := model_options ^ " -c"; + clinker_options := model_options; + cprepro_options := model_options ^ " -U__GNUC__ -E"; + system := "linux" + end + | "aarch64" -> if target_suffix = "linux" then begin + abi_ref := "standard"; + cprepro_options := "-U__GNUC__ -E"; + system := "linux" + end else if check_target_suffix_in ["macos"; "macosx"] then begin + abi_ref := "apple"; + casm := !toolprefix ^ "cc"; + casm_options := "-c -arch arm64"; + cc := !toolprefix ^ "cc -arch arm64"; + clinker := !toolprefix ^ "cc"; + clinker_needs_no_pie := false; + cprepro := !toolprefix ^ "cc"; + cprepro_options := "-arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"; + libmath := ""; + system := "macos" + end else + invalid_input (sprintf "invalid eabi/system '%s' for architecture AArch64." target_suffix) + | "peaktop" -> begin + asm_supports_cfi := Some false; + casm := !toolprefix ^ "gcc"; + casm_options := "-c"; + cc := !toolprefix ^ "gcc"; + clinker := !toolprefix ^ "gcc"; + cprepro := !toolprefix ^ "gcc"; + cprepro_options := "-E -U__GNUC__"; + libmath := ""; + system := "peaktop" + end + | "tricore" -> begin + asm_supports_cfi := Some false; + system := "tricore"; + if target_suffix = "eabi-llvm" then begin + casm := !toolprefix ^ "clang"; + cc := !toolprefix ^ "clang"; + clinker := !toolprefix ^ "clang"; + cprepro := !toolprefix ^ "clang"; + archiver := !toolprefix ^ "llvm-ar rcs"; + casm_options := "-march=tc162 -c"; + cprepro_options := "-march=tc162 -std=c99 -E -U__GNUC__"; + clinker_options := "-march=tc162" + end else begin + casm := !toolprefix ^ "gcc"; + cc := !toolprefix ^ "gcc"; + clinker := !toolprefix ^ "gcc"; + cprepro := !toolprefix ^ "gcc"; + casm_options := "-mtc161 -mcpu=tc22xx -c"; + cprepro_options := "-mtc161 -mcpu=tc22xx -std=c99 -E -U__GNUC__"; + clinker_options := "-mtc161 -mcpu=tc22xx" + end + end + | "" when !target = "manual" -> begin end + | _ -> begin + invalid_input (sprintf "somehow got invalid system with architecture %s." arch) + end + +let _ = begin if !casmruntime = "" then casmruntime := !casm ^ " " ^ !casm_options end + +(* TODO test C compiler with cmd-line options *) + +(* test assembler support for CFI directives *) +let _ = begin if not (!target = "manual") && !asm_supports_cfi = None then + printf "Testing assembler support for CFI directives..."; + let (asm_file, oc) = Filename.open_temp_file "compcert-configure-temp" ".s" in + let content = {|testfun: + .file 1 "testfun.c" + .loc 1 1 + .cfi_startproc + .cfi_adjust_cfa_offset 16 + .cfi_endproc|} in + Printf.fprintf oc "%s\n" content; + let command = Printf.sprintf "%s %s -o %s \"%s\" 2>%s" !casm !casm_options Filename.null asm_file Filename.null in + let ec = Sys.command command in + asm_supports_cfi := Some (ec = 0); + Printf.printf "%s\n" (if !asm_supports_cfi = Some true then "yes" else "no") +end + + +(* TODO Test Availability of Option '-no-pie' or '-nopie' *) +(* Availability of Required Tools: Not necessary *) + +(* TODO Determine $sharedir or check that user-provided $sharedir is valid *) + +(* Generate Makefile.config *) +let config_base = sprintf "PREFIX=%s +BINDIR=%s +LIBDIR=%s +MANDIR=%s +SHAREDIR=%s +COMPFLAGS=-bin-annot +" !prefix !bindir !libdir !mandir !sharedir + +let config_extension = if !target = "manual" then + " +# Target architecture +# ARCH=powerpc +# ARCH=powerpc_vle +# ARCH=arm +# ARCH=x86 +# ARCH=riscV +# ARCH=aarch6 +# ARCH=peaktop +# ARCH=tricore +ARCH= + +# Hardware variant +# MODEL=ppc32 # for plain PowerPC +# MODEL=ppc64 # for PowerPC with 64-bit instructions +# MODEL=e5500 # for Freescale e5500 PowerPC variant +# MODEL=armv6 # for ARM +# MODEL=armv6t2 # for ARM +# MODEL=armv7a # for ARM +# MODEL=armv7r # for ARM +# MODEL=armv7m # for ARM +# MODEL=32sse2 # for x86 in 32-bit mode +# MODEL=64 # for x86 in 64-bit mode +# MODEL=default # for others +MODEL= + +# Target ABI +# ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms +# ABI=eabi # for ARM +# ABI=hardfloat # for ARM +# ABI=standard # for others +ABI= + +# Target bit width +# BITSIZE=64 # for x86 in 64-bit mode, RiscV in 64-bit mode, AArch64 +# BITSIZE=32 # otherwise +BITSIZE= + +# Target endianness +# ENDIANNESS=big # for ARM or PowerPC +# ENDIANNESS=little # for ARM or x86 or RiscV or AArch64 +ENDIANNESS= + +# Target operating system and development environment +# +# Possible choices for PowerPC: +# SYSTEM=linux +# SYSTEM=diab +# +# Possible choices for ARM, AArch64, RiscV: +# SYSTEM=linux +# +# Possible choices for x86: +# SYSTEM=linux +# SYSTEM=bsd +# SYSTEM=macos +# SYSTEM=cygwin +SYSTEM= + +# C compiler (for testing only) +CC=cc + +# Assembler for assembling compiled files +CASM=cc +CASM_OPTIONS=-c + +# Assembler for assembling runtime library files +CASMRUNTIME=$(CASM) $(CASM_OPTIONS) + +# Linker +CLINKER=cc +CLINKER_OPTIONS=-no-pie + +# Preprocessor for .c files +CPREPRO=cc +CPREPRO_OPTIONS=-U__GNUC__ -E + +# Archiver to build .a libraries +ARCHIVER=ar rcs + +# Math library. Set to empty under macOS +LIBMATH=-lm + +# Turn on/off the installation and use of the runtime support library +HAS_RUNTIME_LIB=true + +# Turn on/off the installation and use of the standard header files +HAS_STANDARD_HEADERS=true + +# Turn on/off support for double precision floating point only for selected architectures +HAS_DOUBLE=true + +# Whether the assembler $(CASM) supports .cfi debug directives +ASM_SUPPORTS_CFI=false +#ASM_SUPPORTS_CFI=true + +# Turn on/off compilation of clightgen +CLIGHTGEN=false + +# Turn on/off compilation of only clightgen +CLIGHTGEN_ONLY=false + +# Whether the other tools support responsefiles in GNU syntax or Diab syntax +RESPONSEFILE=gnu # diab + +# Whether to use the local copies of Flocq and MenhirLib +LIBRARY_FLOCQ=local # external +LIBRARY_MENHIRLIB=local # external +" else begin + let s = format_of_string "ABI=%s +ARCH=%s +ASM_SUPPORTS_CFI=%B +BITSIZE=%d +CASM=%s +CASM_OPTIONS=%s +CASMRUNTIME=%s +CC=%s %s +CLINKER=%s +CLINKER_OPTIONS=%s +CPREPRO=%s +CPREPRO_OPTIONS=%s +ARCHIVER=%s +ENDIANNESS=%s +HAS_RUNTIME_LIB=%B +HAS_STANDARD_HEADERS=%B +HAS_DOUBLE=%B +LIBMATH=%s +MODEL=%s +SYSTEM=%s +RESPONSEFILE=%s +" in + sprintf s !abi_ref arch (Option.get !asm_supports_cfi) bitsize !casm !casm_options !casmruntime !cc !cc_options !clinker !clinker_options !cprepro !cprepro_options !archiver endianess !has_runtime_lib !has_standard_headers !has_double_ref !libmath model !system !responsefile +end + +let _ = let config_oc = open_out "Makefile.config" in + output_string config_oc (config_base ^ config_extension); + close_out config_oc + +(* Write default _CoqProject file with dune support *) +let coq_project_content = "-R _build/default/platform/lib compcert.lib -R _build/default/platform/common compcert.common -R _build/default/platform/TargetPlatformCopy compcert.TargetPlatformCopy -R _build/default/platform/backend compcert.backend -R _build/default/platform/cfrontend compcert.cfrontend -R _build/default/platform/driver compcert.driver -R _build/default/platform/cparser compcert.cparser -R _build/default/platform/export compcert.export -R _build/default/flocq Flocq -R _build/default/MenhirLib MenhirLib\n" + +let _ = let coqproject_oc = open_out "_CoqProject" in + output_string coqproject_oc coq_project_content; + close_out coqproject_oc + diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000..a9fdd903c8 --- /dev/null +++ b/tools/dune @@ -0,0 +1,53 @@ +(executable + (name ndfun) + ; silence warnings for unused variable (27) + (flags :standard -w -27) + (libraries str)) + +(executable + (name modorder) + ; silence warnings for unused field (69) + (flags :standard -w -69) + (libraries str)) + +; config file format to ml generator +(executable + (name config_to_ml) + (libraries str)) + +; config file generator +(executable + (name ini_creator)) + +(executable + (name config_creator)) + +; documentation generator +(executable + (name gen_documentation) + (libraries str)) + +(rule + (targets MakefileConfig.ml) + (deps %{project_root}/Makefile.config) + (action + (with-stdout-to %{targets} + (chdir %{workspace_root} + (run config_to_ml %{deps}))))) + +(rule + (targets Version.ml) + (deps %{project_root}/VERSION) + (action + (with-stdout-to %{targets} + (chdir %{workspace_root} + (run config_to_ml %{deps}))))) + +(executable + (name configure) + ; TODO: with updated configure script remove unused variables + (flags :standard -w -32) + (libraries str)) + + +(include_subdirs no) \ No newline at end of file diff --git a/tools/gen_documentation.ml b/tools/gen_documentation.ml new file mode 100644 index 0000000000..1f8e8867de --- /dev/null +++ b/tools/gen_documentation.ml @@ -0,0 +1,113 @@ +(* Tool to generate documentation using coq2html from .v files compiled to compcert theory + +Copies around directories in build system. +*) +let copy_dir source_path target_path = + let command = if Sys.win32 then + Printf.sprintf "xcopy %s %s /i /q /s /e /y" source_path target_path + else + Printf.sprintf "cp -a -R -f %s %s" source_path target_path + in let _ = Sys.command(command) in () + +let to_directory platform = match platform with + | "aarch64" -> "aarch64" + | "arm" -> "arm" + | "peaktop" -> "peaktop" + | "ppc" -> "powerpc" + | "ppc_vle" -> "powerpc_vle" + | "riscV" -> "riscV" + | "tricore" -> "tricore" + | "x86_32" -> "x86_32" + | "x86_64" -> "x86_64" + | x -> invalid_arg ("unexpected platform '" ^ x ^ "'") + +let copy_and_rename new_platform_name file_dir = begin + let cwd = Sys.getcwd () in + Sys.chdir (Filename.concat cwd "platform"); + copy_dir "." (Filename.concat cwd file_dir); + Sys.chdir cwd; + (* rename platform *) + Sys.rename (Filename.concat file_dir "TargetPlatformCopy") (Filename.concat file_dir new_platform_name) +end + + +let suffix_files_in_dirs directories suffix = + List.map (fun dir -> + let files_in_dir = (List.map (fun file -> Filename.concat dir file) (Array.to_list (Sys.readdir dir))) in + let v_files = List.filter (fun f -> + Sys.is_regular_file f && (Filename.check_suffix f suffix) + ) files_in_dir in + (dir, v_files) + ) directories + +let dirs_and_files_of_suffix dir suffix = + let content = (Array.to_list (Sys.readdir dir)) in + let content_prefixed = if dir = "." then content else List.map (fun l -> Filename.concat dir l) content in + let directories = List.filter (fun f -> Sys.is_directory f) content_prefixed in + (* add prefix dir *) + Printf.printf "Dirs %s\n" (String.concat ", " directories); + suffix_files_in_dirs directories suffix + +(* collects .v files and directory names (if directory has .v files) *) +let collect_files_in_dirs dir = + let dir_file_pairs = dirs_and_files_of_suffix dir ".v" in + (List.filter_map (fun (dir, files) -> if files = [] then None else Some dir) dir_file_pairs, List.concat_map snd dir_file_pairs) + +let read_whole_file filename = + let ch = In_channel.open_bin filename in + let s = In_channel.input_all ch in + In_channel.close ch; + s + +let write_whole_file filename s = + let ch = Out_channel.open_bin filename in + Out_channel.output_string ch s; + Out_channel.close ch + +let patch_file plat f = + let read_content = read_whole_file f in + (* Replace all ".TargetPlatformCopy." with ".."*) + let regx = Str.regexp {|\.TargetPlatformCopy\.|} in + let patched_content = Str.global_replace regx ("."^plat^".") read_content in + (* Remove file *) + Sys.remove f; + write_whole_file f patched_content + +let patch_glob_files dir plat = + let glob_file_pairs = dirs_and_files_of_suffix dir ".glob" in + let glob_files = List.concat_map snd glob_file_pairs in + List.iter (patch_file plat) glob_files + +let docs_for_platform new_platform_name = + let file_dir = "platform_doc" in + (* Copy platform code *) + copy_and_rename new_platform_name file_dir; + Sys.chdir file_dir; + Printf.printf "Copied dirs...\n"; + (* Patch references to TargetPlatformCopy to platform name *) + patch_glob_files "." new_platform_name; + (* Collect all .v files *) + let (plat_dirs, plat_files) = collect_files_in_dirs "." in + let (flocq_dirs, flocq_files) = collect_files_in_dirs (Filename.concat ".." "flocq") in + let menhir_dirs = [Filename.concat ".." "MenhirLib"] in + let menhir_files = snd (List.hd (suffix_files_in_dirs menhir_dirs ".v")) in + (* Generate docs *) + let globs = List.map (fun dir -> Filename.concat dir "*.glob") (List.concat [plat_dirs; flocq_dirs; menhir_dirs]) in + let files = List.concat [plat_files; flocq_files; menhir_files] in + let output_dir = Filename.concat ".." (Filename.concat "doc" "html") in + Printf.printf "Creating directory...\n"; + Sys.mkdir output_dir 0o777; + Printf.printf "Generating docs...\n"; + let command = Printf.sprintf "coq2html -d %s -base compcert -short-names %s %s" output_dir (String.concat " " globs) (String.concat " " files) in + Printf.printf "Running command: \n%s" command; + Sys.command command + + + +let _ = + if Array.length Sys.argv = 2 then + docs_for_platform (to_directory Sys.argv.(1)) + else + invalid_arg "expected only one file name argument" + + diff --git a/tools/ini_creator.ml b/tools/ini_creator.ml new file mode 100644 index 0000000000..b84f2a3d69 --- /dev/null +++ b/tools/ini_creator.ml @@ -0,0 +1,20 @@ +open Printf +open MakefileConfig + +let _ = printf "stdlib_path=%s\n" libdir; + printf "prepro=%s\n" cprepro; + printf "linker=%s\n" clinker; + printf "asm=%s\n" casm; + printf "prepro_options=%s\n" cprepro_options; + printf "asm_options=%s\n" casm_options; + printf "linker_options=%s\n" clinker_options; + printf "arch=%s\n" arch; + printf "model=%s\n" model; + printf "abi=%s\n" abi; + printf "endianness=%s\n" endianness; + printf "system=%s\n" system; + printf "has_runtime_lib=%s\n" has_runtime_lib; + printf "has_standard_headers=%s\n" has_standard_headers; + printf "has_double=%s\n" has_double; + printf "asm_supports_cfi=%s\n" asm_supports_cfi; + printf "response_file_style=%s\n" responsefile \ No newline at end of file diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v index d1a29c729c..91dfd39a43 100644 --- a/x86/extractionMachdep.v +++ b/x86/extractionMachdep.v @@ -16,7 +16,7 @@ (* Additional extraction directives specific to the x86-64 port *) -Require Archi SelectOp. +From compcert Require Archi SelectOp. (* Archi *)