Support for building with Dune

.gitignore

@@ -85,3 +85,8 @@
 .nia.cache
 .nra.cache
 .csdp.cache
+
+# Dune Build Results
+_build/
+*.install
+*.opam

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)

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

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

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                         #

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

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

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

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

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/<platform1> _build/<platform2>`
+; 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))))))
+

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)

extraction/extraction.v → 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

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