Rules and supporting files for building aarch64_small monomorphised Isabelle

13 files changed, 177 insertions, 0 deletions

diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile
index 2606da05..2e7c1a7b 100644
--- a/aarch64_small/Makefile
+++ b/aarch64_small/Makefile
@@ -1,5 +1,6 @@
 SAIL:=../sail -Ofast_undefined
 LEM:=../../lem/lem
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
 
 default: all
 
@@ -17,6 +18,9 @@ SOURCES=prelude.sail\
   ../lib/regfp.sail\
   aarch64_regfp.sail
 
+MONO_SPLICES=$(wildcard mono-splices/*.sail)
+MONO_SPLICES_OPTS=$(foreach file,$(MONO_SPLICES),-splice $(file))
+
 all: armV8.lem for-rmem/armV8.lem for-rmem/armV8_toFromInterp2.ml for-rmem/armV8.defs
 
 armV8.lem: $(SOURCES)
@@ -39,10 +43,24 @@ for-rmem/armV8.defs: $(SOURCES)
 	mkdir -p $(dir $@)
 	$(SAIL) -marshal -o $(basename $@) $^
 
+mono/armV8.lem mono/armV8_types.lem mono/ArmV8_lemmas.thy: $(SOURCES) $(MONO_SPLICES)
+	$(SAIL) $(SAILFLAGS) -lem -lem_mwords -auto_mono -mono_rewrites -lem_lib ArmV8_extras_embed -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o armV8 ../lib/mono_rewrites.sail $(SOURCES) $(MONO_SPLICES_OPTS)
+
+mono/ArmV8.thy mono/ArmV8_mono.thy mono/ArmV8_extras_embed.thy: mono/armV8_types.lem mono/armV8.lem armV8_extras_embed.lem
+	cp armV8_extras_embed.lem mono/
+	$(LEM) -isa -lib Sail=../src/gen_lib -lib Sail=../src/lem_interp mono/armV8_types.lem mono/armV8.lem mono/armV8_extras_embed.lem
+
+.PHONY: mono-isa-build
+mono-isa-build: mono/ArmV8.thy
+	isabelle build -b -d $(LEM_ISA_LIB) -d ../lib/isabelle -D mono
+
 clean:
 	rm -f armV8.lem armV8.ml
 	rm -f armV8_embed*.lem armV8_toFromInterp.lem
 	rm -f for-rmem/*
+	rm -f mono/armV8_types.lem mono/armV8.lem mono/armV8_extras_embed.lem
+	rm -f mono/ArmV8_lemmas.thy mono/ArmV8_types_lemmas.thy
+	rm -f mono/ArmV8_types.thy mono/ArmV8.thy mono/ArmV8_extras_embed.thy
 
 ######################################################################
 ETCDIR=../etc
diff --git a/aarch64_small/mono-splices/ASR_C.sail b/aarch64_small/mono-splices/ASR_C.sail
new file mode 100644
index 00000000..0a47d8d7
--- /dev/null
+++ b/aarch64_small/mono-splices/ASR_C.sail
@@ -0,0 +1,8 @@
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bit) effect {escape}
+
+function ASR_C (x, shift) = {
+  result : bits('N) = sail_arith_shiftright(x, shift);
+  carry_out : bit = if shift > 'N then x['N - 1] else x[shift - 1];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/BigEndianReverse.sail b/aarch64_small/mono-splices/BigEndianReverse.sail
new file mode 100644
index 00000000..97893ed1
--- /dev/null
+++ b/aarch64_small/mono-splices/BigEndianReverse.sail
@@ -0,0 +1,8 @@
+val BigEndianReverse : forall 'W, 'W in {8,16,32,64,128}. bits('W) -> bits('W) effect pure
+
+function BigEndianReverse value_name = {
+  result : bits('W) = replicate_bits(0b0,'W);
+  foreach (i from 0 to ('W - 8) by 8)
+    result[i+7 .. i] = (value_name['W-i - 1 .. 'W-i - 8] : bits(8));
+  return result
+}
diff --git a/aarch64_small/mono-splices/CountLeadingSignBits.sail b/aarch64_small/mono-splices/CountLeadingSignBits.sail
new file mode 100644
index 00000000..7bbfd449
--- /dev/null
+++ b/aarch64_small/mono-splices/CountLeadingSignBits.sail
@@ -0,0 +1,3 @@
+val CountLeadingSignBits : forall 'N, 'N >= 2. bits('N) -> int
+
+function CountLeadingSignBits x = return(CountLeadingZeroBits((sail_shiftright(x, 1)) ^ (x & slice_mask(0,'N))))
diff --git a/aarch64_small/mono-splices/DecodeBitMasks.sail b/aarch64_small/mono-splices/DecodeBitMasks.sail
new file mode 100644
index 00000000..fc1d63fa
--- /dev/null
+++ b/aarch64_small/mono-splices/DecodeBitMasks.sail
@@ -0,0 +1,43 @@
+val DecodeBitMasks2 : forall 'M 'S 'd, 'M >= 'd + 1 & 'S >= 0 & 'd >= 0. (int, int('S), nat, int('d), int('M)) -> (bits('M), bits('M)) effect {escape}
+
+function DecodeBitMasks2(esize as 'E, S, R, d, M) = {
+  assert(constraint('E in {2,4,8,16,32,64} & 'M >= 'E & 'E >= 'd + 1));
+  assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
+  welem : bits('E) = ZeroExtend(Ones(S + 1));
+  telem : bits('E) = ZeroExtend(Ones(d + 1));
+  wmask = Replicate(M,ROR(welem, R));
+  tmask = Replicate(M,telem);
+  (wmask, tmask);
+}
+
+function DecodeBitMasks(M : int('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+  /* let M = (length((bit['M]) 0)) in { */
+  /* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
+  /* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
+  levels : bits(6) = Zeros(); /* ARM: uninitialized */
+
+  /* Compute log2 of element size */
+  /* 2^len must be in range [2, 'M] */
+  let len : range(0,6) = match HighestSetBit([immN]@(~(imms))) {
+    None() => { assert (false, "DecodeBitMasks: HighestSetBit returned None"); 0; },
+    Some(c) => c
+  };
+  if len < 1 then {ReservedValue(); exit()} else {
+  assert(M >= lsl(1, len));
+
+  /* Determine S, R and S - R parameters */
+  levels = ZeroExtend(Ones(len));
+
+  /* For logical immediates an all-ones value of S is reserved */
+  /* since it would generate a useless all-ones result (many times) */
+  if immediate & ((imms & levels) == levels) then
+    ReservedValue();
+
+  let S = UInt (imms & levels);
+  let R = UInt (immr & levels);
+  let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
+
+  let esize as int('E) = lsl(1, len);
+  let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
+  DecodeBitMasks2(esize, S, R, d, M);
+}}
diff --git a/aarch64_small/mono-splices/LSL_C.sail b/aarch64_small/mono-splices/LSL_C.sail
new file mode 100644
index 00000000..fb9b352c
--- /dev/null
+++ b/aarch64_small/mono-splices/LSL_C.sail
@@ -0,0 +1,8 @@
+val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bits(1)) effect pure
+
+function LSL_C (x, shift) = {
+  result : bits('N) = x << shift;
+  carry_out : bits(1) = if shift > 'N then 0b0 else [x['N - shift]];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/LSR_C.sail b/aarch64_small/mono-splices/LSR_C.sail
new file mode 100644
index 00000000..5fed8ad6
--- /dev/null
+++ b/aarch64_small/mono-splices/LSR_C.sail
@@ -0,0 +1,8 @@
+val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bit) effect pure
+
+function LSR_C (x, shift) = {
+  result : bits('N) = x >> shift;
+  carry_out : bit = if shift > 'N then bitzero else x[shift - 1];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/Poly32Mod2.sail b/aarch64_small/mono-splices/Poly32Mod2.sail
new file mode 100644
index 00000000..5162d607
--- /dev/null
+++ b/aarch64_small/mono-splices/Poly32Mod2.sail
@@ -0,0 +1,8 @@
+function Poly32Mod2 (data__arg, poly) = {
+  data = data__arg;
+  assert('N > 32, "(N > 32)");
+  let poly' : bits('N) = extzv(poly) in
+  foreach (i from ('N - 1) to 32 by 1 in dec)
+    if [data[i]] == 0b1 then data = data | (poly' << i - 32) else ();
+  return(slice(data, 0, 32))
+}
diff --git a/aarch64_small/mono-splices/Replicate.sail b/aarch64_small/mono-splices/Replicate.sail
new file mode 100644
index 00000000..a3c464e5
--- /dev/null
+++ b/aarch64_small/mono-splices/Replicate.sail
@@ -0,0 +1,6 @@
+function Replicate(N, x) = {
+  assert(N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = N / 'M;
+  assert(constraint('O * 'M == 'N));
+  return(replicate_bits(x, N / 'M))
+}
diff --git a/aarch64_small/mono-splices/SignExtend.sail b/aarch64_small/mono-splices/SignExtend.sail
new file mode 100644
index 00000000..6a263563
--- /dev/null
+++ b/aarch64_small/mono-splices/SignExtend.sail
@@ -0,0 +1,3 @@
+function SignExtend (N,x) = {
+  return(extsv(x))
+}
diff --git a/aarch64_small/mono-splices/ZeroExtend.sail b/aarch64_small/mono-splices/ZeroExtend.sail
new file mode 100644
index 00000000..9e55ee71
--- /dev/null
+++ b/aarch64_small/mono-splices/ZeroExtend.sail
@@ -0,0 +1,3 @@
+function ZeroExtend (N,x) = {
+  return(extzv(x))
+}
diff --git a/aarch64_small/mono-splices/_wMem.sail b/aarch64_small/mono-splices/_wMem.sail
new file mode 100644
index 00000000..8e37ca64
--- /dev/null
+++ b/aarch64_small/mono-splices/_wMem.sail
@@ -0,0 +1,57 @@
+function _wMem(write_buffer, desc, size, acctype, exclusive, value) = {
+  let s = write_buffer.size;
+  if s == 0 then {
+    struct { acctype = acctype,
+      exclusive = exclusive,
+      address = (desc.paddress).physicaladdress,
+      value = ZeroExtend(value),
+      size = size
+    }
+  } else {
+    assert(write_buffer.acctype == acctype);
+    assert(write_buffer.exclusive == exclusive);
+    assert((write_buffer.address + s) : bits(64) == (desc.paddress).physicaladdress);
+  assert((s * 8) + ('N * 8) <= 128);
+    value1 : bits(128) = sail_shiftleft(ZeroExtend(value), s * 8);
+    value1[((s * 8) - 1) .. 0] = (write_buffer.value)[((s * 8) - 1) .. 0];
+    { write_buffer with
+      value = value1,
+      size = s + size
+    }
+  }
+}
+
+val flush_write_buffer2 : forall 'n, 'n in {1,2,4,8,16}. (write_buffer_type, int('n)) -> unit effect {escape,wmv}
+
+function flush_write_buffer2 (write_buffer, s) ={
+  match write_buffer.acctype {
+    AccType_NORMAL   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_STREAM   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_UNPRIV   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ORDERED (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    _  => not_implemented("unrecognised memory access")
+  };
+}
+
+function flush_write_buffer(write_buffer) = {
+  assert(write_buffer.exclusive == false);
+  let s : range(0,16) = write_buffer.size;
+  assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
+  flush_write_buffer2(write_buffer, s);
+}
+
+val flush_write_buffer_exclusive2 : forall 'n, 'n in {1,2,4,8,16}. (write_buffer_type, int('n)) -> bool effect {escape, wmv}
+function flush_write_buffer_exclusive2(write_buffer, s) = {
+  match write_buffer.acctype {
+    AccType_ATOMIC   => wMem_Val_ATOMIC(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ATOMIC_ORDERED(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    _  => { not_implemented("unrecognised memory access"); false; }
+  };
+}
+
+function flush_write_buffer_exclusive(write_buffer) = {
+  assert(write_buffer.exclusive);
+  let s = write_buffer.size;
+  assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
+  flush_write_buffer_exclusive2(write_buffer, s);
+}
diff --git a/aarch64_small/mono/ROOT b/aarch64_small/mono/ROOT
new file mode 100644
index 00000000..9c65d37d
--- /dev/null
+++ b/aarch64_small/mono/ROOT
@@ -0,0 +1,4 @@
+session "Sail-AArch64-small" = "Sail" +
+  options [document = false]
+  theories
+    ArmV8_lemmas