Merge pull request #210 from rems-project/revocation

CHERI Revocation

Makefile

@@ -17,14 +17,10 @@ endif
 # To enable the printing of commands, use [make Q= ...],
 Q = @
 
-# parse the -j flag if present, set jobs to "auto" oterwise
-JFLAGVALUE=$(patsubst -j%,%,$(filter -j%,$(MFLAGS)))
-JOBS=$(if $(JFLAGVALUE),$(JFLAGVALUE),"auto")
-
 ifdef PROFILING
-    DUNEFLAGS=--workspace=dune-workspace.profiling -j $(JOBS)
+    DUNEFLAGS=--workspace=dune-workspace.profiling
 else
-    DUNEFLAGS=-j $(JOBS)
+    DUNEFLAGS=
 endif
 
 .PHONY: normal
@@ -85,7 +81,7 @@ cn: prelude-src
 
 cheri: prelude-src
 	@echo "[DUNE] cerberus-cheri"
-	$(Q)./tools/cheribuild_hack.sh "dune build $(DUNEFLAGS) cerberus-cheri.install"
+	$(Q)dune build $(DUNEFLAGS) cerberus-cheri.install
 
 
 # .PHONY: cerberus-ocaml ocaml
@@ -293,7 +289,7 @@ install: cerberus
 .PHONY: install-cheri
 install-cheri:
 	@echo "[DUNE] install cerberus-cheri"
-	$(Q)./tools/cheribuild_hack.sh "dune build -p cerberus-cheri --profile=release -j $(JOBS) @install"
+	$(Q)dune install cerberus-cheri
 
 .PHONY: install_cn
 install_cn: cn

backend/common/pipeline.ml

@@ -520,8 +520,10 @@ let print_core (conf, io) ~filename core_file =
 let core_passes (conf, io) ~filename core_file =
   (* If using the switch making load() returning unspecified value undefined, then
      we remove from the Core the code dealing with them. *)
+  (* This is disabled for CHERI because some of the CHERI_intrinsics can
+     return an unspecified value *)
   let core_file =
-    if Switches.(has_switch SW_strict_reads) then
+    if Switches.(has_switch SW_strict_reads && not (is_CHERI ())) then
       Remove_unspecs.rewrite_file core_file
     else
       core_file in

cerberus-cheri.opam

@@ -46,6 +46,16 @@ depends: [
 
 build: [
   ["dune" "subst"] {pinned}
-  [ make "-j" jobs "install-cheri" ]
+  ["dune"
+    "build"
+    "-p"
+    name
+    "--profile=release"
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
 dev-repo: "git+https://github.com/rems-project/cerberus.git"

coq/CheriMemory/CerbSwitches.v

@@ -3,6 +3,6 @@ Require Import CoqSwitches.
 
 Module Type CerbSwitchesDefs.
 
-  Parameter get_swtiches: unit -> cerb_switches_t.
+  Parameter get_switches: unit -> cerb_switches_t.
 
 End CerbSwitchesDefs.