diff options
| author | Alasdair Armstrong | 2018-03-20 17:57:20 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-22 18:58:59 +0000 |
| commit | e33c8546e005fba30ff882b188c86ca03d0917c8 (patch) | |
| tree | cf72fc3066962718d26a76baedd2d11a7be16946 /cheri/Makefile | |
| parent | 0860deb52e55b11e39e3470290e07f861f877483 (diff) | |
Fix C compilation for CHERI and MIPS
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
Diffstat (limited to 'cheri/Makefile')
| -rw-r--r-- | cheri/Makefile | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 88c5cf0d..3ccc14df 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -25,6 +25,9 @@ CHERI_MAIN:=$(MIPS_SAIL_DIR)/main.sail cheri: $(CHERI_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ +cheri.c: $(CHERI_SAILS) $(CHERI_MAIN) + $(SAIL) -memo_z3 -c $^ 1> $@ + cheri128: $(CHERI128_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ @@ -54,7 +57,7 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy clean: - rm -rf cheri cheri128 _sbuild inst_*.sail + rm -rf cheri cheri128 _sbuild inst_*.sail cheri.c EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^ //;1d;$$d' > inst_$1.sail extract: cheri_insts.sail @@ -67,7 +70,7 @@ extract: cheri_insts.sail $(call EXTRACT_INST,CGetSealed) $(call EXTRACT_INST,CGetPCC) $(call EXTRACT_INST,CGetPCCSetOffset) - $(call EXTRACT_INST,CGetCause) + $(call EXTRACT_INST,CGetCause $(call EXTRACT_INST,CSetCause) $(call EXTRACT_INST,CAndPerm) $(call EXTRACT_INST,CToPtr) |