diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 35fa442c16d383b8a47d63faa9ccbf7c323c4688..9509d97d411ef8cc8350a05d638e049fb6945d6c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -85,17 +85,8 @@ frontend:
tests:
stage: tests
script:
- - export DIR=$(nix run nixpkgs#gnumake -- -np | grep -oPh "(?<=RUST_SRC = ).*")
- - mkdir .ci_tmp
- - echo ${DIR} | xargs -r -n 1 | cut -d'/' -f1 | uniq | xargs -r mv -v -t .ci_tmp
- - cd .ci_tmp
- - echo "(lang dune 3.8)" >| dune-project
- - echo "(using coq 0.8)" >> dune-project
- - |
- for folder in ${DIR}
- do
- cd $folder
- nix shell -c cargo refinedrust
- cd -
- nix shell -c dune build --display=short --root=.
- done
+ - nix shell -c nix run nixpkgs#gnumake -- setup-nix
+ - nix shell -c nix run nixpkgs#gnumake -- generate_stdlib
+ - nix shell -c nix run nixpkgs#gnumake -- generate_case_studies
+ - cd case_studies
+ - nix shell -c dune build --display=short
diff --git a/Makefile b/Makefile
index c5d1656add03db65204f3b923e5023929024a7a9..9f43f98f39e1135978bd4f19453e0e57a966970c 100644
--- a/Makefile
+++ b/Makefile
@@ -15,9 +15,15 @@ clean: clean_all
.PHONY: clean
frontend:
- cd rr_frontend && ./refinedrust build && ./refinedrust install
+ @cd rr_frontend && ./refinedrust build && ./refinedrust install
-RUST_SRC = stdlib/alloc stdlib/option stdlib/result stdlib/spin stdlib/vec case_studies/paper-examples case_studies/tests case_studies/minivec
+setup-nix:
+ rm -f dune-project
+
+setup-dune:
+ echo "(lang dune 3.8)" > dune-project
+
+CASE_STUDIES = case_studies/paper-examples case_studies/tests case_studies/minivec
%.gen: % phony
cd $< && cargo refinedrust
@@ -27,9 +33,15 @@ RUST_SRC = stdlib/alloc stdlib/option stdlib/result stdlib/spin stdlib/vec case_
cd $< && cargo clean
.PHONY: phony
-generate_all: $(addsuffix .gen, $(RUST_SRC))
+generate_stdlib:
+ make -C stdlib generate_stdlib
+generate_case_studies: $(addsuffix .gen, $(CASE_STUDIES))
+generate_all: generate_stdlib generate_case_studies
-clean_all: $(addsuffix .clean, $(RUST_SRC))
+clean_stdlib:
+ make -C stdlib clean_stdlib
+clean_case_studies: $(addsuffix .clean, $(CASE_STUDIES))
+clean_all: clean_case_studies clean_stdlib
.PHONY: generate_all
@@ -63,11 +75,11 @@ export BUILDDEP_OPAM_BODY
# Create a virtual Opam package with the same deps as RefinedC, but no
# build.
-builddep/refinedrust-builddep.opam: refinedrust.opam Makefile
+builddep/refinedrust-builddep.opam: theories/refinedrust.opam Makefile
@echo "# Creating builddep package."
@mkdir -p builddep
@echo "$$BUILDDEP_OPAM_BODY" > $@
- @opam show -f depends: ./refinedrust.opam >> $@
+ @opam show -f depends: ./theories/refinedrust.opam >> $@
@echo "]" >> $@
# Install the virtual Opam package to ensure that:
diff --git a/case_studies/dune-project b/case_studies/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..18d4a5d9e6ae8656b624e9a6d83f0fc278382419
--- /dev/null
+++ b/case_studies/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.8)
+(using coq 0.8)
+(name refinedrust-examples)
+(package (name refinedrust-examples) (allow_empty))
+
diff --git a/coq-caesium-config-no-align.opam b/coq-caesium-config-no-align.opam
deleted file mode 100644
index 3104792032883b3feb3c1267c348b95358736dec..0000000000000000000000000000000000000000
--- a/coq-caesium-config-no-align.opam
+++ /dev/null
@@ -1,22 +0,0 @@
-opam-version: "2.0"
-name: "coq-caesium-config-no-align"
-synopsis: "Configuration package to configure Caesium to not use alignment"
-description: """
-Installing this package instructs the refinedc package to disable alignment in the Caesium C semantics.
-"""
-license: "BSD-3-Clause"
-
-maintainer: ["Michael Sammler <msammler@mpi-sws.org>"]
-authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]
-
-homepage: "https://plv.mpi-sws.org/refinedc"
-bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
-dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
-
-conflict-class: [ "coq-caesium-config" ]
-
-depends: [
-]
-
-build: [
-]
diff --git a/dune b/dune
deleted file mode 100644
index 474f9b99b1833d3a0c152035e4abe7d26dac76bc..0000000000000000000000000000000000000000
--- a/dune
+++ /dev/null
@@ -1,17 +0,0 @@
-; Add project-wide flags here.
-;(env
- ;(dev
- ;(binaries (tools/coqc_timing.sh as coqc))
- ;(flags :standard))
- ;(release
- ;(binaries (tools/coqc_timing.sh as coqc))
- ;(flags :standard)))
-
-;(ignored_subdirs (frontend))
-;(dirs :standard \ rr_frontend)
-
-
-;(install
- ;(files FAQ.md ANNOTATIONS.md)
- ;(section doc)
- ;(package refinedc))
diff --git a/flake.nix b/flake.nix
index 368fd1d5cbd97f865bed9462f508ca80aa2450fc..8ac5c61dae70a437dcb59563f52e1f6f62821a6a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -113,11 +113,7 @@
pname = name;
opam-name = name;
- src = with nix-filter.lib;
- nix-filter {
- root = ./.;
- include = ["dune-project" (inDirectory "theories")];
- };
+ src = ./theories;
propagatedBuildInputs = with coq.pkgs; [coq-record-update equations lambda-rust];
@@ -138,13 +134,32 @@
postInstall = with pkgs.lib.strings; ''
wrapProgram $out/bin/refinedrust-rustc \
- --set LD_LIBRARY_PATH "${rust.lib}"
+ --set LD_LIBRARY_PATH "${rust.lib}" \
+ --set DYLD_FALLBACK_LIBRARY_PATH "${rust.lib}"
wrapProgram $out/bin/${pname} \
--set PATH "${makeSearchPath "bin" buildInputs}"
'';
};
+
+ stdlib = coq.pkgs.mkCoqDerivation {
+ inherit meta version;
+
+ pname = "refinedrust-stdlib";
+ opam-name = "refinedrust-stdlib";
+ src = ./stdlib;
+
+ buildInputs = [packages.frontend rust.toolchain];
+ propagatedBuildInputs = [packages.theories];
+
+ preBuild = ''
+ dune() { command dune $@ --display=short; }
+ make generate_stdlib
+ '';
+ useDune = true;
+ };
+
default = pkgs.buildEnv {
inherit meta;
@@ -155,7 +170,7 @@
nativeBuildInputs = [pkgs.makeWrapper];
postBuild = with pkgs.lib.strings; ''
wrapProgram $out/bin/dune \
- --set COQPATH "${makeSearchPath "lib/coq/${coq.version}/user-contrib" (fetchCoqDeps packages.theories)}"
+ --set COQPATH "${makeSearchPath "lib/coq/${coq.version}/user-contrib" (fetchCoqDeps packages.stdlib)}"
'';
};
};
@@ -165,6 +180,7 @@
shellHook = ''
export LD_LIBRARY_PATH=''${LD_LIBRARY_PATH}:${rust.lib}
+ export DYLD_FALLBACK_LIBRARY_PATH=''${DYLD_FALLBACK_LIBRARY_PATH}:${rust.lib}
export RUST_SRC_PATH=${rust.src}/rustc_driver/Cargo.toml
'';
};
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 2e2fbc6d28561df671590b803db2b025387ccd17..907e9e5818e0827b19a3cddfd7f3ac3695c805eb 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -108,6 +108,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
/// the second component determines whether to include it in the code file as well
extra_imports: HashSet<(radium::CoqPath, bool)>,
coq_path_prefix: String,
+ dune_package: Option<String>,
shim_registry: shim_registry::ShimRegistry<'rcx>,
}
@@ -624,12 +625,17 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let mut dune_file = io::BufWriter::new(fs::File::create(generated_dune_path.as_path()).unwrap());
let extra_theories: Vec<_> =
self.extra_imports.iter().filter_map(|(path, _)| path.path.clone()).collect();
+ let dune_package = if let Some(ref dune_package) = self.dune_package {
+ format!("(package {dune_package})\n")
+ } else {
+ format!("")
+ };
write!(
dune_file,
"\
; Generated by [refinedrust], do not edit.\n\
(coq.theory\n\
- (flags -w -notation-overridden -w -redundant-canonical-projection)\n\
+ (flags -w -notation-overridden -w -redundant-canonical-projection)\n{dune_package}\
(name {generated_module_path})\n\
(theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust {}))",
extra_theories.join(" ")
@@ -691,7 +697,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
write!(dune_file, "\
; Generated by [refinedrust], do not edit.\n\
(coq.theory\n\
- (flags -w -notation-overridden -w -redundant-canonical-projection)\n\
+ (flags -w -notation-overridden -w -redundant-canonical-projection)\n{dune_package}\
(name {proof_module_path})\n\
(modules {})\n\
(theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust {} {}.{}.generated))",
@@ -1094,6 +1100,9 @@ where
let path_prefix = crate_spec.prefix.unwrap_or("refinedrust.examples".to_string());
info!("Setting Coq path prefix: {:?}", path_prefix);
+ let package = crate_spec.package;
+ info!("Setting dune package: {:?}", package);
+
// get module attributes
let module_attrs = get_module_attributes(&env)?;
@@ -1158,6 +1167,7 @@ where
extra_imports: imports.into_iter().map(|x| (x, false)).collect(),
coq_path_prefix: path_prefix,
shim_registry,
+ dune_package: package,
const_registry: ConstScope {
statics: HashMap::new(),
},
diff --git a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
index fa2c7341f69eaa52a92dad8022b73e641d71c257..fa30039346372140661a17775873301a0b1d6a1c 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -22,6 +22,7 @@ pub struct CrateAttrs {
pub imports: Vec<specs::CoqPath>,
pub prefix: Option<String>,
pub includes: Vec<String>,
+ pub package: Option<String>,
}
pub struct VerboseCrateAttrParser {}
@@ -42,6 +43,7 @@ impl CrateAttrParser for VerboseCrateAttrParser {
let mut imports: Vec<specs::CoqPath> = Vec::new();
let mut includes: Vec<String> = Vec::new();
let mut prefix: Option<String> = None;
+ let mut package: Option<String> = None;
for &it in attrs.iter() {
let ref path_segs = it.path.segments;
@@ -65,6 +67,13 @@ impl CrateAttrParser for VerboseCrateAttrParser {
}
prefix = Some(path.value().to_string());
},
+ "package" => {
+ let path: parse::LitStr = buffer.parse(&meta).map_err(str_err)?;
+ if let Some(_) = package {
+ return Err(format!("multiple rr::package attributes have been provided"));
+ }
+ package = Some(path.value().to_string());
+ },
_ => {
return Err(format!("unknown attribute for crate specification: {:?}", args));
},
@@ -75,6 +84,7 @@ impl CrateAttrParser for VerboseCrateAttrParser {
imports,
prefix,
includes,
+ package,
})
}
}
diff --git a/scripts/install-stdlib.sh b/scripts/install-stdlib.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ea9e2eb5555dda1ed24f770e27fb5c6d7ddb5921
--- /dev/null
+++ b/scripts/install-stdlib.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# Installs RefinedRust stdlib in the current opam switch.
+# Inputs:
+# - REFINEDRUST_ROOT: the root directory of the RefinedRust checkout
+
+opam pin remove refinedrust-stdlib -y
+opam remove refinedrust-stdlib -y
+opam pin add refinedrust-stdlib.dev $REFINEDRUST_ROOT/stdlib -y
diff --git a/scripts/install-typesystem.sh b/scripts/install-typesystem.sh
index fd40d02b961a652a9912be475b8bbab91f78a5df..3490fbc2477f34d206af75c47f86561aa9f66135 100755
--- a/scripts/install-typesystem.sh
+++ b/scripts/install-typesystem.sh
@@ -6,4 +6,4 @@
opam pin remove refinedrust -y
opam remove refinedrust -y
-opam pin add refinedrust.dev $REFINEDRUST_ROOT -y
+opam pin add refinedrust.dev $REFINEDRUST_ROOT/theories -y
diff --git a/stdlib/Makefile b/stdlib/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..33cf8dcc88d724781a91563bf6d8d8abd025d338
--- /dev/null
+++ b/stdlib/Makefile
@@ -0,0 +1,16 @@
+STDLIB = alloc option result spin vec
+
+%.gen: % phony
+ cd $< && cargo refinedrust
+.PHONY: phony
+
+%.clean: % phony
+ cd $< && cargo clean
+.PHONY: phony
+
+generate_stdlib: $(addsuffix .gen, $(STDLIB))
+
+clean_stdlib: $(addsuffix .clean, $(STDLIB))
+
+stdlib: generate_stdlib
+ dune build --display short
diff --git a/stdlib/alloc/src/lib.rs b/stdlib/alloc/src/lib.rs
index 18ac3c5b35b432b44700781be24c1cbde9127bdb..6b2a469828cdad1793a46e45afea8c4db5a2ca90 100644
--- a/stdlib/alloc/src/lib.rs
+++ b/stdlib/alloc/src/lib.rs
@@ -3,6 +3,7 @@
#![feature(custom_inner_attributes)]
#![feature(allocator_api)]
+#![rr::package("refinedrust-stdlib")]
#![rr::coq_prefix("stdlib.alloc")]
use std::ptr::NonNull;
diff --git a/stdlib/dune b/stdlib/dune
new file mode 100644
index 0000000000000000000000000000000000000000..07ea9a9f3e6236968c8a373ea9039465d3ba962b
--- /dev/null
+++ b/stdlib/dune
@@ -0,0 +1,5 @@
+(install
+ (files
+ (glob_files_rec *.rrlib))
+ (section share)
+ (package refinedrust-stdlib))
diff --git a/stdlib/dune-project b/stdlib/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..bc06edc172de2dd0147aac77c5c596004acc77c4
--- /dev/null
+++ b/stdlib/dune-project
@@ -0,0 +1,4 @@
+(lang dune 3.8)
+(using coq 0.8)
+(name refinedrust-stdlib)
+(package (name refinedrust-stdlib))
diff --git a/stdlib/option/src/lib.rs b/stdlib/option/src/lib.rs
index 18a45ba3366056929c701bb1035586ebfb1e41c9..dc3c8b6369bdfd4c77a9df70c7e4b596a9d2700e 100644
--- a/stdlib/option/src/lib.rs
+++ b/stdlib/option/src/lib.rs
@@ -1,6 +1,7 @@
#![feature(register_tool)]
#![register_tool(rr)]
#![feature(custom_inner_attributes)]
+#![rr::package("refinedrust-stdlib")]
#![rr::coq_prefix("stdlib.option")]
diff --git a/stdlib/refinedrust-stdlib.opam b/stdlib/refinedrust-stdlib.opam
new file mode 100644
index 0000000000000000000000000000000000000000..ebe82ff46108eeb579561e8cbf13fcbd6c3f6711
--- /dev/null
+++ b/stdlib/refinedrust-stdlib.opam
@@ -0,0 +1,21 @@
+opam-version: "2.0"
+name: "refinedrust"
+synopsis: "RefinedRust verification framework"
+homepage: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
+bug-reports: "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev"
+maintainer: "Lennard Gäher"
+authors: "Lennard Gäher"
+description: """
+RefinedRust is a prototype framework for verifying safe and unsafe Rust code.
+"""
+license: "BSD-3-Clause"
+
+depends: [
+ "refinedrust" {= version | = "~dev"}
+]
+
+build: [
+ [make "generate_stdlib"]
+ ["dune" "subst"] {pinned}
+ ["dune" "build" "-p" name "-j" jobs]
+]
diff --git a/stdlib/result/src/lib.rs b/stdlib/result/src/lib.rs
index 408ee0afbba375573f988e4c293eed55aa22ac1a..99c7de5581b425db4f622f149a858dc2f770762a 100644
--- a/stdlib/result/src/lib.rs
+++ b/stdlib/result/src/lib.rs
@@ -1,6 +1,7 @@
#![feature(register_tool)]
#![register_tool(rr)]
#![feature(custom_inner_attributes)]
+#![rr::package("refinedrust-stdlib")]
#![rr::coq_prefix("stdlib.result")]
#![rr::import("stdlib.result.theories", "result")]
@@ -10,9 +11,11 @@ use std::fmt;
#[rr::export_as(core::result::Result)]
#[rr::refined_by("result (place_rfn {rt_of T}) (place_rfn {rt_of E})")]
pub enum Result<T, E> {
+ #[rr::export_as(core::result::Result::Ok)]
#[rr::pattern("Ok" $ "x")]
#[rr::refinement("-[x]")]
Ok(T),
+ #[rr::export_as(core::result::Result::Err)]
#[rr::pattern("Err" $ "x")]
#[rr::refinement("-[x]")]
Err(E),
diff --git a/stdlib/result/theories/dune b/stdlib/result/theories/dune
index d154b48f870d9a4588e369f6929979dd6658ef53..838c36ff649299dfbe46594bd498c717246f85f3 100644
--- a/stdlib/result/theories/dune
+++ b/stdlib/result/theories/dune
@@ -1,4 +1,5 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
+(package refinedrust-stdlib)
(name stdlib.result.theories)
(theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust))
diff --git a/stdlib/spin/src/lib.rs b/stdlib/spin/src/lib.rs
index c952a2deed961bb6df0fe92de012fa24f7ca5011..895bbfa836d1c8b6251af2d03cbf1356aceff55f 100644
--- a/stdlib/spin/src/lib.rs
+++ b/stdlib/spin/src/lib.rs
@@ -1,7 +1,7 @@
#![feature(register_tool)]
#![register_tool(rr)]
#![feature(custom_inner_attributes)]
-
+#![rr::package("refinedrust-stdlib")]
#![rr::coq_prefix("stdlib.spin")]
mod relax;
diff --git a/stdlib/spin/theories/once/dune b/stdlib/spin/theories/once/dune
index e3ad26dc6a6bf4ec76686035de8159485d20f530..c5650a947511853dd0b704fd0a98a0c92350c719 100644
--- a/stdlib/spin/theories/once/dune
+++ b/stdlib/spin/theories/once/dune
@@ -1,4 +1,5 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
+(package refinedrust-stdlib)
(name stdlib.spin.theories.once)
(theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust))
diff --git a/stdlib/vec/src/lib.rs b/stdlib/vec/src/lib.rs
index 9cbcccf03a995a046516deebdffb8b61bc438103..90d689e0e8294dc6bef24dc944c5c44425aa03da 100644
--- a/stdlib/vec/src/lib.rs
+++ b/stdlib/vec/src/lib.rs
@@ -3,7 +3,7 @@
#![feature(custom_inner_attributes)]
#![rr::include("option")]
#![rr::include("alloc")]
-
+#![rr::package("refinedrust-stdlib")]
#![feature(allocator_api)]
#![rr::coq_prefix("stdlib.alloc")]
diff --git a/dune-project b/theories/dune-project
similarity index 100%
rename from dune-project
rename to theories/dune-project
index b7bb9055b83f6636a6deccdf09ecdf4904cb6ab8..37243205590a2127c42094e162d0e07980ab46a8 100644
--- a/dune-project
+++ b/theories/dune-project
@@ -1,5 +1,5 @@
(lang dune 3.8)
+(using coq 0.8)
(name refinedrust)
(package (name refinedrust))
(package (name coq-caesium-config-no-align) (allow_empty))
-(using coq 0.8)
diff --git a/refinedrust.opam b/theories/refinedrust.opam
similarity index 66%
rename from refinedrust.opam
rename to theories/refinedrust.opam
index 3d3d7646f4c858539b0aceba3a3c12c70749b447..3488ac7ad81ae4a3dc608f98cbd594f51f35907f 100644
--- a/refinedrust.opam
+++ b/theories/refinedrust.opam
@@ -20,19 +20,7 @@ depends: [
"coq-lambda-rust" { = "dev" }
]
-depopts: [
- "coq-caesium-config-no-align"
-]
-
build: [
- [make "prepare-install-refinedrust"]
- [make "config"] {!coq-caesium-config-no-align:installed}
- [make "config-no-align"] {coq-caesium-config-no-align:installed}
["dune" "subst"] {pinned}
["dune" "build" "-p" name "-j" jobs]
]
-
-messages: [
- "with default configuration" {!coq-caesium-config-no-align:installed}
- "with no-align configuration" {coq-caesium-config-no-align:installed}
-]