From aeb0f82f67ff829cd7a4b57c638b44a07d39ba3b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 19:53:59 +0000 Subject: Don't require manual set up of Isabelle session directories Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more. --- test/isabelle/Makefile | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'test') diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile index 43028fed..5df82977 100644 --- a/test/isabelle/Makefile +++ b/test/isabelle/Makefile @@ -1,7 +1,8 @@ -CHERI_DIR = ../../cheri -AARCH64_DIR = ../../aarch64 +ISA_LIB_DIR = ../../lib/isabelle +CHERI_DIR ?= ../../../sail-cheri-mips/cheri +AARCH64_DIR ?= ../../aarch64 TGTS = run_cheri.native run_aarch64.native -SESSION_DIRS = -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . +SESSION_DIRS = -d $(ISA_LIB_DIR) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . .PHONY: all clean -- cgit v1.2.3 From 365cf2015c77551e37d31336220497f6ca84794c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 23:16:47 +0000 Subject: Pass Lem library path to Isabelle --- test/isabelle/Makefile | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile index 5df82977..1f488db1 100644 --- a/test/isabelle/Makefile +++ b/test/isabelle/Makefile @@ -1,8 +1,13 @@ -ISA_LIB_DIR = ../../lib/isabelle +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) +$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + +SAIL_ISA_LIB = ../../lib/isabelle CHERI_DIR ?= ../../../sail-cheri-mips/cheri AARCH64_DIR ?= ../../aarch64 TGTS = run_cheri.native run_aarch64.native -SESSION_DIRS = -d $(ISA_LIB_DIR) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . +SESSION_DIRS = -d $(LEM_ISA_LIB) -d $(SAIL_ISA_LIB) -d $(CHERI_DIR) -d $(AARCH64_DIR) -d . .PHONY: all clean -- cgit v1.2.3 From 93ac9f1762771d601c2b9eed9014ff471093358b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 22 Jan 2019 18:35:50 +0000 Subject: Add some more test cases --- test/c/nonexistent_pragma.expect | 1 + test/c/nonexistent_pragma.sail | 12 ++++++++++ test/c/unroll.expect | 6 +++++ test/c/unroll.sail | 37 +++++++++++++++++++++++++++++ test/typecheck/pass/nonexistent_pragma.sail | 12 ++++++++++ 5 files changed, 68 insertions(+) create mode 100644 test/c/nonexistent_pragma.expect create mode 100644 test/c/nonexistent_pragma.sail create mode 100644 test/c/unroll.expect create mode 100644 test/c/unroll.sail create mode 100644 test/typecheck/pass/nonexistent_pragma.sail (limited to 'test') diff --git a/test/c/nonexistent_pragma.expect b/test/c/nonexistent_pragma.expect new file mode 100644 index 00000000..9daeafb9 --- /dev/null +++ b/test/c/nonexistent_pragma.expect @@ -0,0 +1 @@ +test diff --git a/test/c/nonexistent_pragma.sail b/test/c/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/c/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + diff --git a/test/c/unroll.expect b/test/c/unroll.expect new file mode 100644 index 00000000..355943c1 --- /dev/null +++ b/test/c/unroll.expect @@ -0,0 +1,6 @@ +fac(4) = 24 +fac(5) = 120 +fac(6) = 720 +fac2(4) = 24 +fac2(5) = 120 +fac2(6) = 720 diff --git a/test/c/unroll.sail b/test/c/unroll.sail new file mode 100644 index 00000000..c68bb49d --- /dev/null +++ b/test/c/unroll.sail @@ -0,0 +1,37 @@ +default Order dec + +$include + +/* It's hard to test that this optimization does the right thing, but +we can at least test that it doesn't do the wrong thing. */ + +$optimize unroll 20 +val fac : forall 'n, 'n >= 0. int('n) -> int +function fac(n) = { + if n == 0 then { + 1 + } else { + n * fac(n - 1) + } +} + +$optimize unroll 2 +val fac2 : forall 'n, 'n >= 0. int('n) -> int +function fac2(n) = { + if n == 0 then { + 1 + } else { + n * fac2(n - 1) + } +} + +val "print_int" : (string, int) -> unit + +function main((): unit) -> unit = { + print_int("fac(4) = ", fac(4)); + print_int("fac(5) = ", fac(5)); + print_int("fac(6) = ", fac(6)); + print_int("fac2(4) = ", fac2(4)); + print_int("fac2(5) = ", fac2(5)); + print_int("fac2(6) = ", fac2(6)) +} \ No newline at end of file diff --git a/test/typecheck/pass/nonexistent_pragma.sail b/test/typecheck/pass/nonexistent_pragma.sail new file mode 100644 index 00000000..da4b99f7 --- /dev/null +++ b/test/typecheck/pass/nonexistent_pragma.sail @@ -0,0 +1,12 @@ +default Order dec + +$include + +$not_a_valid_pragma test + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + print_endline("test") +} + -- cgit v1.2.3