From 2cbf746bc430767fc9890d37071e4aa2b501f7c0 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Wed, 2 Oct 2024 18:02:36 +0100 Subject: [PATCH 1/3] - Aligned cap_narrow_perms with the Asm instruction CLRPERM: bit-mask represents the permissions to clear - Added example illustrating how to convert masks between cap_narrow_perms and the Cheri C function cheri_perms_and - Adapted several examples - Tidying up _CoqProject files --- CoqMakefile | 989 -------------------------------- CoqMakefile.conf | 71 --- _CoqProject | 9 +- coq-cheri-capabilities.opam | 2 +- theories/Common/Capabilities.v | 15 +- theories/Morello/Capabilities.v | 205 +------ theories/Morello/MorelloTests.v | 62 +- 7 files changed, 62 insertions(+), 1291 deletions(-) delete mode 100644 CoqMakefile delete mode 100644 CoqMakefile.conf diff --git a/CoqMakefile b/CoqMakefile deleted file mode 100644 index 77081c3..0000000 --- a/CoqMakefile +++ /dev/null @@ -1,989 +0,0 @@ -########################################################################## -## # The Coq Proof Assistant / The Coq Development Team ## -## v # Copyright INRIA, CNRS and contributors ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=command time -f $(TIMEFMT) -else -ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=command time -endif -endif -else -STDTIME?=command time -f $(TIMEFMT) -endif - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQNATIVE ?= "$(COQBIN)coqnative" -COQDEP ?= "$(COQBIN)coqdep" -COQDOC ?= "$(COQBIN)coqdoc" -COQPP ?= "$(COQBIN)coqpp" -COQMKFILE ?= "$(COQBIN)coq_makefile" -OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack - -# DESTDIR is prepended to all installation paths -DESTDIR ?= - -# Debug builds, typically -g to OCaml, -debug to Coq. -CAMLDEBUG ?= -COQDEBUG ?= - -# Extra packages to be linked in (as in findlib -package) -CAMLPKGS ?= -FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) - -# Option for making timing files -TIMING?= -# Option for changing sorting of timing output file -TIMING_SORT_BY ?= auto -# Option for changing the fuzz parameter on the output file -TIMING_FUZZ ?= 0 -# Option for changing whether to use real or user time for timing tables -TIMING_REAL?= -# Option for including the memory column(s) -TIMING_INCLUDE_MEM?= -# Option for sorting by the memory column -TIMING_SORT_BY_MEM?= -# Output file names for timed builds -TIME_OF_BUILD_FILE ?= time-of-build.log -TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log -TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log -TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log -TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log -TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line - -TGTS ?= - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -# Substitution of the path by appending $(DESTDIR) if needed. -# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. -windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) -destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) - -# Installation paths of libraries and documentation. -COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) -COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) -COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) -COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? - -# findlib files installation -FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" -FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" - -# we need to move out of sight $(METAFILE) otherwise findlib thinks the -# package is already installed -findlib_install = \ - $(HIDE)if [ "$(METAFILE)" ]; then \ - $(FINDLIBPREINST) && \ - mv "$(METAFILE)" "$(METAFILE).skip" ; \ - "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ - rc=$$?; \ - mv "$(METAFILE).skip" "$(METAFILE)"; \ - exit $$rc; \ - fi -findlib_remove = \ - $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ - "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ - fi - - -########## End of parameters ################################################## -# What follows may be relevant to you only if you need to -# extend this Makefile. If so, look for 'Extension point' here and -# put in CoqMakefile.local double colon rules accordingly. -# E.g. to perform some work after the all target completes you can write -# -# post-all:: -# echo "All done!" -# -# in CoqMakefile.local -# -############################################################################### - - - - -# Flags ####################################################################### -# -# We define a bunch of variables combining the parameters. -# To add additional flags to coq, coqchk or coqdoc, set the -# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. -# To overwrite the default choice and set your own flags entirely, set the -# {COQ,COQCHK,COQDOC}FLAGS variable. - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) - -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -OPT?= - -# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d -ifeq '$(OPT)' '-byte' -USEBYTE:=true -DYNOBJ:=.cma -DYNLIB:=.cma -else -USEBYTE:= -DYNOBJ:=.cmxs -DYNLIB:=.cmxs -endif - -# these variables are meant to be overridden if you want to add *extra* flags -COQEXTRAFLAGS?= -COQCHKEXTRAFLAGS?= -COQDOCEXTRAFLAGS?= - -# Find the last argument of the form "-native-compiler FLAG" -COQUSERNATIVEFLAG:=$(strip \ -$(subst -native-compiler-,,\ -$(lastword \ -$(filter -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))))) - -COQFILTEREDEXTRAFLAGS:=$(strip \ -$(filter-out -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))) - -COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) - -ifeq '$(COQACTUALNATIVEFLAG)' 'yes' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="yes" -else -ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="no" -else - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" - COQDONATIVE="no" -endif -endif - -# these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) -COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) -COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) - -COQDOCLIBS?=$(COQLIBS_NOML) - -# The version of Coq being run and the version of coq_makefile that -# generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.18.0 - -# COQ_SRC_SUBDIRS is for user-overriding, usually to add -# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for -# Coq's own core libraries, which should be replaced by ocamlfind -# options at some point. -COQ_SRC_SUBDIRS?= -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -# ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -CAMLFLAGS+=$(OCAMLWARN) - -ifneq (,$(TIMING)) - ifeq (after,$(TIMING)) - TIMING_EXT=after-timing - else - ifeq (before,$(TIMING)) - TIMING_EXT=before-timing - else - TIMING_EXT=timing - endif - endif - TIMING_ARG=-time-file $<.$(TIMING_EXT) -else - TIMING_ARG= -endif - -# Files ####################################################################### -# -# We here define a bunch of variables about the files being part of the -# Coq project in order to ease the writing of build target and build rules - -VDFILE := .CoqMakefile.d - -ALLSRCFILES := \ - $(MLGFILES) \ - $(MLFILES) \ - $(MLPACKFILES) \ - $(MLLIBFILES) \ - $(MLIFILES) - -# helpers -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) -strip_dotslash = $(patsubst ./%,%,$(1)) - -# without this we get undefined variables in the expansion for the -# targets of the [deprecated,use-mllib-or-mlpack] rule -with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) - -VO = vo -VOS = vos - -VOFILES = $(VFILES:.v=.$(VO)) -GLOBFILES = $(VFILES:.v=.glob) -HTMLFILES = $(VFILES:.v=.html) -GHTMLFILES = $(VFILES:.v=.g.html) -BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(MLGFILES:.mlg=.cmo) \ - $(MLFILES:.ml=.cmo) \ - $(MLPACKFILES:.mlpack=.cmo) -CMXFILES = $(CMOFILES:.cmo=.cmx) -OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) -CMXAFILES = $(CMAFILES:.cma=.cmxa) -CMIFILES = \ - $(CMOFILES:.cmo=.cmi) \ - $(MLIFILES:.mli=.cmi) -# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .mlg file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) - -# files that are packed into a plugin (no extension) -PACKEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) -CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) -CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) -OBJFILES = $(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES = \ - $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmx) \ - $(OBJFILES:.o=.cmxs) -FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) - -# trick: wildcard filters out non-existing files, so that `install` doesn't show -# warnings and `clean` doesn't pass to rm a list of files that is too long for -# the shell. -NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) -FILESTOINSTALL = \ - $(VOFILES) \ - $(VFILES) \ - $(GLOBFILES) \ - $(NATIVEFILES) \ - $(CMXSFILES) # to be removed when we remove legacy loading -FINDLIBFILESTOINSTALL = \ - $(CMIFILESTOINSTALL) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) - -# Compilation targets ######################################################### - -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all - -all.timing.diff: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all.timing.diff - -ifeq (0,$(TIMING_REAL)) -TIMING_REAL_ARG := -TIMING_USER_ARG := --user -else -ifeq (1,$(TIMING_REAL)) -TIMING_REAL_ARG := --real -TIMING_USER_ARG := -else -TIMING_REAL_ARG := -TIMING_USER_ARG := -endif -endif - -ifeq (0,$(TIMING_INCLUDE_MEM)) -TIMING_INCLUDE_MEM_ARG := --no-include-mem -else -TIMING_INCLUDE_MEM_ARG := -endif - -ifeq (1,$(TIMING_SORT_BY_MEM)) -TIMING_SORT_BY_MEM_ARG := --sort-by-mem -else -TIMING_SORT_BY_MEM_ARG := -endif - -make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) -make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) -make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) - $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed -print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -ifeq (,$(BEFORE)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -ifeq (,$(AFTER)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -endif -endif -pretty-timed: - $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed -.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff - -# Extension points for actions to be performed before/after the all target -pre-all:: - @# Extension point - $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ - echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ - echo "W: while the current Coq version is $(COQ_VERSION)";\ - fi -.PHONY: pre-all - -post-all:: - @# Extension point -.PHONY: post-all - -real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) -.PHONY: real-all - -real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONY: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -vos: $(VOFILES:%.vo=%.vos) -.PHONY: vos - -vok: $(VOFILES:%.vo=%.vok) -.PHONY: vok - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ -.PHONY: validate - -only: $(TGTS) -.PHONY: only - -# Documentation targets ####################################################### - -html: $(GLOBFILES) $(VFILES) - $(SHOW)'COQDOC -d html $(GAL)' - $(HIDE)mkdir -p html - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -d $@' - $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -# FIXME: not quite right, since the output name is different -gallinahtml: GAL=-g -gallinahtml: html - -all-gal.ps: GAL=-g -all-gal.ps: all.ps - -all-gal.pdf: GAL=-g -all-gal.pdf: all.pdf - -# ? -beautify: $(BEAUTYFILES) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: beautify - -# Installation targets ######################################################## -# -# There rules can be extended in CoqMakefile.local -# Extensions can't assume when they run. - -# We use $(file) to avoid generating a very long command string to pass to the shell -# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) -# However Apple ships old make which doesn't have $(file) so we need a fallback -$(file >.hasfile,1) -HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) - -MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ - $(shell rm -f .filestoinstall) \ - $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) - -# findlib needs the package to not be installed, so we remove it before -# installing it (see the call to findlib_remove) -install: META - @$(MKFILESTOINSTALL) - $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ - if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ - done; exit $$code - $(HIDE)for f in $$(cat .filestoinstall); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - $(call findlib_remove) - $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) - $(HIDE)$(MAKE) install-extra -f "$(SELF)" - @rm -f .filestoinstall -install-extra:: - @# Extension point -.PHONY: install install-extra - -META: $(METAFILE) - $(HIDE)if [ "$(METAFILE)" ]; then \ - cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ - fi - -install-byte: - $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) - -install-doc:: html mlihtml - @# Extension point - $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(HIDE)for i in html/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done - $(HIDE)install -d \ - "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)for i in mlihtml/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done -.PHONY: install-doc - -uninstall:: - @# Extension point - @$(MKFILESTOINSTALL) - $(call findlib_remove) - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" ;\ - done - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ - (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ - done - @rm -f .filestoinstall - -.PHONY: uninstall - -uninstall-doc:: - @# Extension point - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true -.PHONY: uninstall-doc - -# Cleaning #################################################################### -# -# There rules can be extended in CoqMakefile.local -# Extensions can't assume when they run. - -clean:: - @# Extension point - $(SHOW)'CLEAN' - $(HIDE)rm -f $(CMOFILES) - $(HIDE)rm -f $(CMIFILES) - $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMXFILES) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(OFILES) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(HIDE)rm -f $(MLGFILES:.mlg=.ml) - $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) - $(HIDE)rm -f $(MLIFILES:.mli=.cmti) - $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)find . -name .coq-native -type d -empty -delete - $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(VOFILES:.vo=.vos) - $(HIDE)rm -f $(VOFILES:.vo=.vok) - $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) - $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex - $(HIDE)rm -f $(VFILES:.v=.glob) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)rm -f META - $(HIDE)rm -rf html mlihtml -.PHONY: clean - -cleanall:: clean - @# Extension point - $(SHOW)'CLEAN *.aux *.timing' - $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) - $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) - $(HIDE)rm -f .lia.cache .nia.cache -.PHONY: cleanall - -archclean:: - @# Extension point - $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) -.PHONY: archclean - - -# Compilation rules ########################################################### - -$(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -$(MLGFILES:.mlg=.ml): %.ml: %.mlg - $(SHOW)'COQPP $<' - $(HIDE)$(COQPP) $< - -# Stupid hack around a deficient syntax: we cannot concatenate two expansions -$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -# Same hack -$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack - $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -# This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx - $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -# can't make -# https://www.gnu.org/software/make/manual/make.html#Static-Pattern -# work with multiple target rules -# so use eval in a loop instead -# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets -# if available (GNU Make >= 4.3) -ifneq (,$(filter grouped-target,$(.FEATURES))) -define globvorule= - -# take care to $$ variables using $< etc - $(1).vo $(1).glob &: $(1).v | $(VDFILE) - $(SHOW)COQC $(1).v - $(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $(1).vo - $(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo -endif - -endef -else - -$(VOFILES): %.vo: %.v | $(VDFILE) - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $@ - $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ -endif - -# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets -$(GLOBFILES): %.glob: %.v - $(SHOW)'COQC $< (for .glob)' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -endif - -$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vos): %.vos: %.v - $(SHOW)COQC -vos $< - $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vok): %.vok: %.v - $(SHOW)COQC -vok $< - $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" - -$(BEAUTYFILES): %.v.beautified: %.v - $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< - -$(TEXFILES): %.tex: %.v - $(SHOW)'COQDOC -latex $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(GTEXFILES): %.g.tex: %.v - $(SHOW)'COQDOC -latex -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(SHOW)'COQDOC -html $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(SHOW)'COQDOC -html -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -# Dependency files ############################################################ - -ifndef MAKECMDGOALS - -include $(ALLDFILES) -else - ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -GENMLFILES:=$(MLGFILES:.mlg=.ml) -$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -# If this makefile is created using a _CoqProject we have coqdep get -# options from it. This avoids argument length limits for pathological -# projects. Note that extra options might be on the command line. -VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) - -$(VDFILE): _CoqProject $(VFILES) - $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) - -# Misc ######################################################################## - -byte: - $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" -.PHONY: byte - -opt: - $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt - -# This is deprecated. To extend this makefile use -# extension points and CoqMakefile.local -printenv:: - $(warning printenv is deprecated) - $(warning write extensions in CoqMakefile.local or include CoqMakefile.conf) - @echo 'COQLIB = $(COQLIB)' - @echo 'COQCORELIB = $(COQCORELIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIB = $(COQLIBS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' -.PHONY: printenv - -# Generate a .merlin file. If you need to append directives to this -# file you can extend the merlin-hook target in CoqMakefile.local -.merlin: - $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQCORELIB)' >> .merlin - $(HIDE)echo 'S $(COQCORELIB)' >> .merlin - $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ - echo 'B $(COQCORELIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) - $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" -.PHONY: merlin - -merlin-hook:: - @# Extension point -.PHONY: merlin-hook - -# prints all variables -debug: - $(foreach v,\ - $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ - $(.VARIABLES))),\ - $(info $(v) = $($(v)))) -.PHONY: debug - -.DEFAULT_GOAL := all - -# Users can create CoqMakefile.local-late to hook into double-colon rules -# or add other needed Makefile code, using defined -# variables if necessary. --include CoqMakefile.local-late - -# Local Variables: -# mode: makefile-gmake -# End: diff --git a/CoqMakefile.conf b/CoqMakefile.conf deleted file mode 100644 index e636402..0000000 --- a/CoqMakefile.conf +++ /dev/null @@ -1,71 +0,0 @@ -# This configuration file was generated by running: -# coq_makefile -f _CoqProject -o CoqMakefile - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif -COQMKFILE ?= "$(COQBIN)coq_makefile" - -############################################################################### -# # -# Project files. # -# # -############################################################################### - -COQMF_CMDLINE_VFILES := -COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES)) -COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES)) -COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES)) -COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES)) -COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES)) -COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES)) -COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES)) -COQMF_METAFILE = - -############################################################################### -# # -# Path directives (-I, -R, -Q). # -# # -############################################################################### - -COQMF_OCAMLLIBS = -COQMF_SRC_SUBDIRS = -COQMF_COQLIBS = -R theories CheriCaps -COQMF_COQLIBS_NOML = -R theories CheriCaps -COQMF_CMDLINE_COQLIBS = - -############################################################################### -# # -# Coq configuration. # -# # -############################################################################### - -COQMF_COQLIB=/home/ricardo/.opam/coq-cheri-capabilities/lib/coq/ -COQMF_COQCORELIB=/home/ricardo/.opam/coq-cheri-capabilities/lib/coq/../coq-core/ -COQMF_DOCDIR=/home/ricardo/.opam/coq-cheri-capabilities/share/doc/ -COQMF_OCAMLFIND=/home/ricardo/.opam/coq-cheri-capabilities/bin/ocamlfind -COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -COQMF_WARN=-warn-error +a-3 -COQMF_HASNATDYNLINK=true -COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax -COQMF_COQ_NATIVE_COMPILER_DEFAULT=no -COQMF_WINDRIVE= - -############################################################################### -# # -# Native compiler. # -# # -############################################################################### - -COQMF_COQPROJECTNATIVEFLAG = - -############################################################################### -# # -# Extra variables. # -# # -############################################################################### - -COQMF_OTHERFLAGS = -COQMF_INSTALLCOQDOCROOT = CheriCaps diff --git a/_CoqProject b/_CoqProject index 39beee4..6db547b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,8 +1,7 @@ -# To use _CoqProject with VS Code + VsCoq extension, from the root directory of this file run -## coq_makefile -f _CoqProject -o CoqMakefile -## make -f CoqMakefile -# and then code . +# This file is used by Coq IDEs (eg, VS Code with the VsCoq extension) -R theories CheriCaps -theories +# theories + +-Q _build/default/theories CheriCaps diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam index 6c94c98..7388adf 100644 --- a/coq-cheri-capabilities.opam +++ b/coq-cheri-capabilities.opam @@ -6,7 +6,7 @@ maintainer: ["ricardo.almeida@ed.ac.uk"] authors: ["Ricardo Almeida" "Vadim Zaliva"] license: "BSD-3-clause" homepage: "https://github.com/rems-project/coq-cheri-capabilities" -version: "20240917" +version: "20241002" bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues" depends: [ "dune" {>= "3.7"} diff --git a/theories/Common/Capabilities.v b/theories/Common/Capabilities.v index a890099..d8e2527 100644 --- a/theories/Common/Capabilities.v +++ b/theories/Common/Capabilities.v @@ -43,19 +43,6 @@ Module Type PERMISSIONS. (* User-defined permissions *) Parameter get_user_perms: t -> list bool. - (* Clearing permissions *) - Parameter perm_clear_global: t -> t. - Parameter perm_clear_execute: t -> t. - Parameter perm_clear_ccall: t -> t. - Parameter perm_clear_load: t -> t. - Parameter perm_clear_load_cap: t -> t. - Parameter perm_clear_seal: t -> t. - Parameter perm_clear_store: t -> t. - Parameter perm_clear_store_cap: t -> t. - Parameter perm_clear_store_local_cap: t -> t. - Parameter perm_clear_system_access: t -> t. - Parameter perm_clear_unseal: t -> t. - (** perform bitwise AND of user permissions *) Parameter perm_and_user_perms: t -> list bool -> t. @@ -219,7 +206,7 @@ Module Type CAPABILITY The input permissions should be the ones to be kept. Related instructions: - CAndPerm in RISC V - - In Morello, CLRPERM c mask = cap_narrow_perms c ~mask + - CLRPERM in Morello *) Parameter cap_narrow_perms: t -> P.t -> t. diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index 029a616..bf9e2fe 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -104,6 +104,9 @@ Module Permissions <: PERMISSIONS. end. Next Obligation. intros. rewrite eq. done. Defined. + (* Computes all permissions that are not in p. *) + Definition inv (p : t) := bv_not p. + Definition user_perms_len:nat := 4. Variant perm := Load_perm | Store_perm | Execute_perm | LoadCap_perm | StoreCap_perm | StoreLocalCap_perm | Seal_perm | Unseal_perm @@ -114,44 +117,25 @@ Module Permissions <: PERMISSIONS. let perms : (mword 64) := zero_extend permissions 64 in fun perm => CapPermsInclude perms perm. - Definition has_global_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_GLOBAL. - Definition has_executive_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_EXECUTIVE. - Definition has_execute_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_EXECUTE. - Definition has_load_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_LOAD. - Definition has_load_cap_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_LOAD_CAP. - Definition has_seal_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_SEAL. - Definition has_store_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_STORE. - Definition has_store_cap_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_STORE_CAP. - Definition has_store_local_cap_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_STORE_LOCAL. - Definition has_system_access_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_SYSTEM. - Definition has_unseal_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_UNSEAL. - Definition has_user1_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_USER1. - Definition has_user2_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_USER2. - Definition has_user3_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_USER3. - Definition has_user4_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_USER4. - Definition has_compartmentID_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_COMPARTMENT_ID. - Definition has_branch_sealed_pair_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_BRANCH_SEALED_PAIR. - Definition has_ccall_perm (permissions:t) : bool := - has_branch_sealed_pair_perm permissions. - Definition has_mutable_load_perm (permissions:t) : bool := - has_perm permissions CAP_PERM_MUTABLE_LOAD. + Definition has_global_perm (permissions:t) : bool := has_perm permissions CAP_PERM_GLOBAL. + Definition has_executive_perm (permissions:t) : bool := has_perm permissions CAP_PERM_EXECUTIVE. + Definition has_execute_perm (permissions:t) : bool := has_perm permissions CAP_PERM_EXECUTE. + Definition has_load_perm (permissions:t) : bool := has_perm permissions CAP_PERM_LOAD. + Definition has_load_cap_perm (permissions:t) : bool := has_perm permissions CAP_PERM_LOAD_CAP. + Definition has_seal_perm (permissions:t) : bool := has_perm permissions CAP_PERM_SEAL. + Definition has_store_perm (permissions:t) : bool := has_perm permissions CAP_PERM_STORE. + Definition has_store_cap_perm (permissions:t) : bool := has_perm permissions CAP_PERM_STORE_CAP. + Definition has_store_local_cap_perm (permissions:t) : bool := has_perm permissions CAP_PERM_STORE_LOCAL. + Definition has_system_access_perm (permissions:t) : bool := has_perm permissions CAP_PERM_SYSTEM. + Definition has_unseal_perm (permissions:t) : bool := has_perm permissions CAP_PERM_UNSEAL. + Definition has_user1_perm (permissions:t) : bool := has_perm permissions CAP_PERM_USER1. + Definition has_user2_perm (permissions:t) : bool := has_perm permissions CAP_PERM_USER2. + Definition has_user3_perm (permissions:t) : bool := has_perm permissions CAP_PERM_USER3. + Definition has_user4_perm (permissions:t) : bool := has_perm permissions CAP_PERM_USER4. + Definition has_compartmentID_perm (permissions:t) : bool := has_perm permissions CAP_PERM_COMPARTMENT_ID. + Definition has_branch_sealed_pair_perm (permissions:t) : bool := has_perm permissions CAP_PERM_BRANCH_SEALED_PAIR. + Definition has_ccall_perm (permissions:t) : bool := has_branch_sealed_pair_perm permissions. + Definition has_mutable_load_perm (permissions:t) : bool := has_perm permissions CAP_PERM_MUTABLE_LOAD. Definition get_user_perms (permissions:t) : list bool := [ has_user1_perm permissions; has_user2_perm permissions; @@ -226,8 +210,7 @@ Module Permissions <: PERMISSIONS. has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; has_load_perm perms ] _. Next Obligation. reflexivity. Defined. - Program Definition perm_p0 : t := - @of_list_bool (list_perm_to_list_bool []) _. + Program Definition perm_p0 : t := @of_list_bool (list_perm_to_list_bool []) _. Next Obligation. reflexivity. Defined. Definition perm_Universal : t := @@ -242,135 +225,6 @@ Module Permissions <: PERMISSIONS. Definition perm_alloc_fun : t := (make_permissions [ Load_perm; Execute_perm; LoadCap_perm ]). - Program Definition perm_clear_global (perms:t) : t := - @of_list_bool [ false; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_executive (perms:t) : t := - @of_list_bool [ has_global_perm perms; false; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_execute (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; false; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_load (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - false ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_load_cap (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; false; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_seal (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - false; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_store (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; false; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_store_cap (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; false; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_store_local_cap (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; false; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_system_access (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; false; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_unseal (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; false; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_branch_sealed_pair (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; false; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_ccall (perms:t) : t := - perm_clear_branch_sealed_pair perms. - - Program Definition perm_clear_mutable_load (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - false; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_compartment_ID (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; false; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_user1 (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; false; has_user2_perm perms; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_user2 (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; false; has_user3_perm perms; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_user3 (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; false; has_user4_perm perms; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - - Program Definition perm_clear_user4 (perms:t) : t := - @of_list_bool [ has_global_perm perms; has_executive_perm perms; has_user1_perm perms; has_user2_perm perms; has_user3_perm perms; false; - has_mutable_load_perm perms; has_compartmentID_perm perms; has_branch_sealed_pair_perm perms; has_system_access_perm perms; has_unseal_perm perms; - has_seal_perm perms; has_store_local_cap_perm perms; has_store_cap_perm perms; has_load_cap_perm perms; has_execute_perm perms; has_store_perm perms; - has_load_perm perms ] _. - Next Obligation. reflexivity. Defined. - Definition to_string (perms:t) : string := let s (f:bool) l := if f then l else "" in s (has_load_perm perms) "r" @@ -386,7 +240,6 @@ Module Permissions <: PERMISSIONS. Definition to_raw (perms:t) : Z := to_Z perms. Definition of_raw (z:Z) : t := of_Z z. - Definition to_list (perms:t) : list bool := bv_to_list_bool perms. @@ -752,16 +605,15 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou let ot : (mword (Z.of_N ObjType.len)) := ot in CapSetObjectType c (zero_extend ot 64). - (* [perms] must contain [1] for permissions to be kept and [0] for those to be cleared *) + (* [perms] must contain [1] for the permissions to be cleared and [0] for those to be kept *) Definition cap_narrow_perms (c:t) (perms:Permissions.t) : t := let perms_mw : (mword (Z.of_N Permissions.len)) := perms in let mask : (mword 64) := zero_extend perms_mw 64 in - let mask_inv : (mword 64) := invert_bits mask in - let new_cap := CapClearPerms c mask_inv in + let new_cap := CapClearPerms c mask in if (cap_is_sealed c) then (cap_invalidate new_cap) else new_cap. Definition cap_clear_global_perm (cap:t) : t := - cap_narrow_perms cap (Permissions.perm_clear_global (cap_get_perms cap)). + cap_narrow_perms cap (Permissions.make_permissions [Permissions.Global_perm]). Definition cap_set_bounds (c : t) (bounds : Bounds.t) (exact : bool) : t := (* CapSetBounds sets the lower bound to the value of the input cap, @@ -915,9 +767,10 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou let result:Z := Z.land (Z.add len nmask) mask in result. - Definition make_cap (value : AddressValue.t) (otype : ObjType.t) (bounds : Bounds.t) (perms_to_keep : Permissions.t) : t := + Definition make_cap (value : AddressValue.t) (otype : ObjType.t) (bounds : Bounds.t) (perms : Permissions.t) : t := let new_cap := cap_cU () in - let new_cap := cap_narrow_perms new_cap perms_to_keep in + let perms_to_clear := Permissions.inv perms in + let new_cap := cap_narrow_perms new_cap perms_to_clear in let new_cap := cap_narrow_bounds new_cap bounds in let new_cap := cap_set_value new_cap value in cap_set_objtype new_cap otype. diff --git a/theories/Morello/MorelloTests.v b/theories/Morello/MorelloTests.v index c9566cd..11d2cc0 100644 --- a/theories/Morello/MorelloTests.v +++ b/theories/Morello/MorelloTests.v @@ -73,50 +73,45 @@ Module test_cap_getters_and_setters. Proof. vm_compute. bv_solve. Qed. Example permissions_test_3 : - let mask : Permissions.t := perm_Load_Store in + let mask : t := inv perm_Load_Store in perm_Load_Store = cap_get_perms (cap_narrow_perms c1 mask). Proof. vm_compute. bv_solve. Qed. Example permissions_test_4 : - let mask : Permissions.t := perm_Load_Store in + let mask : t := inv perm_Load_Store in let cap := cap_narrow_perms c1 mask in - let mask : Permissions.t := perm_Load_Execute in + let mask : t := inv perm_Load_Execute in perm_Load = cap_get_perms (cap_narrow_perms cap mask). Proof. vm_compute. bv_solve. Qed. Example permissions_test_5 : - let mask : Permissions.t := make_permissions [Load_perm; Execute_perm] in - let capA := (cap_narrow_perms c1 mask) in - let perms : Permissions.t := Permissions.perm_Universal in - let perms := perm_clear_store_cap perms in - let perms := perm_clear_store perms in - let perms := perm_clear_global perms in - let perms := perm_clear_executive perms in - let perms := perm_clear_seal perms in - let perms := perm_clear_load_cap perms in - let perms := perm_clear_store_local_cap perms in - let perms := perm_clear_system_access perms in - let perms := perm_clear_unseal perms in - let perms := perm_clear_branch_sealed_pair perms in - let perms := perm_clear_mutable_load perms in - let perms := perm_clear_compartment_ID perms in - let perms := perm_clear_user4 perms in - let perms := perm_clear_user3 perms in - let perms := perm_clear_user2 perms in - let perms := perm_clear_user1 perms in - let capB := (cap_narrow_perms c1 perms) in - capA = capB. - Proof. vm_compute. reflexivity. Qed. - + let mask1 : t := make_permissions [Load_perm; LoadCap_perm; Execute_perm; MutableLoad_perm; User1_perm; User2_perm; Seal_perm; CompartmentID_perm; Executive_perm] in + let mask2 : t := make_permissions [Store_perm; StoreCap_perm; StoreLocalCap_perm; System_perm; User3_perm; User4_perm; Unseal_perm; BranchSealedPair_perm; Global_perm] in + mask1 = inv mask2. + Proof. vm_compute. bv_solve. Qed. + Example permissions_test_6 : - let perms := perm_clear_global (cap_get_perms c1) in - perms = cap_get_perms c9 /\ perms ≠ cap_get_perms c1. + let perms := cap_get_perms (cap_narrow_perms c1 (make_permissions [Global_perm])) in + perms = cap_get_perms c9 ∧ perms ≠ cap_get_perms c1. Proof. vm_compute. split. bv_solve. discriminate. Qed. Example permissions_test_7 : Permissions.of_Z (Permissions.to_Z perm_Load_Store) = perm_Load_Store. Proof. reflexivity. Qed. + Example permissions_test_8 : + let cheri_perms_and (c:Capability.t) (mask:bv 64) : Capability.t := + let tag : bv 1 := bv_extract 128 1 c in + let perms : bv 18 := bv_extract 110 18 c in + let rem : bv 110 := bv_extract 0 110 c in + bv_concat 129 (bv_concat 19 tag (bv_and perms (bv_extract 0 18 mask))) rem in + let store_perms : bv 18 := make_permissions [Store_perm; StoreCap_perm; StoreLocalCap_perm] in + let store_mask : bv 64 := bv_not (bv_zero_extend 64 store_perms) in + bv_to_Z_unsigned store_mask = 0xfffffffffffecfff ∧ + store_perms = bv_not (bv_extract 0 18 (Z_to_bv 64 0xfffffffffffecfff)) ∧ + Capability.cap_narrow_perms c1 store_perms = cheri_perms_and c1 store_mask. + Proof. vm_compute. repeat split; bv_solve. Qed. + Example get_and_user_perms_test_1 : let user_perms_A : (list bool) := get_user_perms (cap_get_perms (cap_cU ())) in let user_perms_A := [ nth 0 user_perms_A false; negb (nth 1 user_perms_A false); @@ -128,7 +123,7 @@ Module test_cap_getters_and_setters. Proof. vm_compute. split. reflexivity. reflexivity. Qed. Example eqb_and_narrow_perm_test_1 : - let mask : Permissions.t := perm_Load_Store in + let mask : Permissions.t := inv perm_Load_Store in (c2 = (cap_narrow_perms c1 mask))%stdpp. Proof. vm_compute. reflexivity. Qed. @@ -150,12 +145,9 @@ Module test_cap_getters_and_setters. (* We can see new_bounds can be represented exactly from cap5: https://www.morello-project.org/capinfo?c=0x1%3Afb00000034473337%3A1011111111113333 *) let new_cap := cap_narrow_bounds_exact c5 (new_base,new_limit) in let result := cap_get_bounds new_cap in - (* isExpValid = true /\ (base_set =? new_base) = true /\ *) - (* (limit_set =? new_limit) = true *) - (cap_is_valid c5) = true /\ (cap_is_valid new_cap) = true - /\ cap_get_bounds_ new_cap = (new_base,new_limit,true). - Proof. vm_compute. split. reflexivity. split. reflexivity. (* split. reflexivity. - split. reflexivity. *) reflexivity. Qed. + (cap_is_valid c5) = true ∧ (cap_is_valid new_cap) = true + ∧ cap_get_bounds_ new_cap = (new_base,new_limit,true). + Proof. vm_compute. split. reflexivity. split. reflexivity. reflexivity. Qed. Example seal_and_unseal_test_1 : (* c6 has Seal and Unseal permissions and its value is <= the largest objtype. *) From 8523bf920f12b38597f18c06c59a8987fbd4a287 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Wed, 2 Oct 2024 18:54:07 +0100 Subject: [PATCH 2/3] New example converting masks for clearing permissions --- theories/Morello/MorelloTests.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/theories/Morello/MorelloTests.v b/theories/Morello/MorelloTests.v index 11d2cc0..3a37968 100644 --- a/theories/Morello/MorelloTests.v +++ b/theories/Morello/MorelloTests.v @@ -112,6 +112,24 @@ Module test_cap_getters_and_setters. Capability.cap_narrow_perms c1 store_perms = cheri_perms_and c1 store_mask. Proof. vm_compute. repeat split; bv_solve. Qed. + Example permissions_test_9 : + let store_and_mask : list bool := [true; true; true; true; true; true; true; true; true; true; true; true; false; false; true; true; false; true; true; true; true; true; + true; true; true; true; true; true; true; true; true; true; true; + true; true; true; true; true; true; true; true; true; true; true; + true; true; true; true; true; true; true; true; true; true; true; + true; true; true; true; true; true; true; true; true] in + let store_perms := list.take 18 store_and_mask in + let store_perms := List.map negb store_perms in + match (Permissions.of_list store_perms) with + | Some perms => + let new_cap := Capability.cap_narrow_perms c1 perms in + Capability.cap_permits_store c1 = true ∧ Capability.cap_permits_store_cap c1 = true ∧ Capability.cap_permits_store_local_cap c1 = true ∧ + Capability.cap_permits_store new_cap = false ∧ Capability.cap_permits_store_cap new_cap = false ∧ Capability.cap_permits_store_local_cap new_cap = false ∧ + Permissions.to_string (Capability.cap_get_perms new_cap) = "rxRE" + | None => False + end. + Proof. vm_compute. tauto. Qed. + Example get_and_user_perms_test_1 : let user_perms_A : (list bool) := get_user_perms (cap_get_perms (cap_cU ())) in let user_perms_A := [ nth 0 user_perms_A false; negb (nth 1 user_perms_A false); From f517b3b1d9602f2b302d73b30607f4ca2144f0ea Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Wed, 2 Oct 2024 18:56:10 +0100 Subject: [PATCH 3/3] removing comment --- _CoqProject | 2 -- 1 file changed, 2 deletions(-) diff --git a/_CoqProject b/_CoqProject index 6db547b..ec30549 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,4 @@ -R theories CheriCaps -# theories - -Q _build/default/theories CheriCaps