diff options
Diffstat (limited to 'aarch64_small')
29 files changed, 289 insertions, 4 deletions
diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile index fe4c5841..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,12 +18,18 @@ 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) # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem $(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^ +armV8.smt_model: $(SOURCES) + $(SAIL) $(SAILFLAGS) -smt_serialize -o armV8 $^ + for-rmem/armV8.lem: $(SOURCES) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them @@ -36,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/armV8.sail b/aarch64_small/armV8.sail index d8ee0bbe..5754b159 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -2142,10 +2142,12 @@ function clause execute ( Reverse((d,n,datasize as int('R),op)) ) = { assert (vsize > 0); /* FIXME: CP adding assertion to make typecheck */ foreach (base from 0 to (datasize - 1) by (2 * vsize)) { /* ARM: while base < datasize do */ assert (base+vsize*2 - 1 < datasize); /* FIXME: CP adding assertion to make typecheck */ - let a = tmp[(base+(2*vsize) - 1)..(base+vsize)]; +/* let a = tmp[(base+(2*vsize) - 1)..(base+vsize)]; result[((base+vsize) - 1)..base] = a; let b = tmp[(base+vsize - 1)..base]; - result[(base+(2*vsize) - 1)..(base+vsize)] = b; + result[(base+(2*vsize) - 1)..(base+vsize)] = b;*/ + result[((base+vsize) - 1)..base] = tmp[(base+(2*vsize) - 1)..(base+vsize)]; + result[(base+(2*vsize) - 1)..(base+vsize)] = tmp[(base+vsize - 1)..base]; /* ARM: base = base + (2 * vsize); */ }; }; diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail index 8c684fc7..8b32e09f 100644 --- a/aarch64_small/armV8_A64_lib.sail +++ b/aarch64_small/armV8_A64_lib.sail @@ -799,7 +799,7 @@ function ExtendReg (N, _reg, etype, shift) = { let len = uMin(len, length(_val) - shift); assert( len >= 1 & 'S + len < 'N); - let a = (_val[(len - 1)..0]); +/* let a = (_val[(len - 1)..0]);*/ /* Zeros() */ Extend((_val[(len - 1)..0]) @ (Zeros() : bits('S)), _unsigned) } diff --git a/aarch64_small/gen/ast.hgen b/aarch64_small/gen/ast.hgen index 98148a5c..3f0ce79d 100644 --- a/aarch64_small/gen/ast.hgen +++ b/aarch64_small/gen/ast.hgen @@ -43,3 +43,5 @@ | `AArch64TestBitAndBranch of inst_reg*reg_size*uinteger*bit*bit64 (* t,datasize,bit_pos,bit_val,offset *) | `AArch64MoveSystemRegister of inst_reg*uinteger*uinteger*uinteger*uinteger*uinteger*boolean (* t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read *) | `AArch64MoveSystemImmediate of bit4*pSTATEField (* operand,field *) + | `AArch64DataCache of inst_reg*dCOp + | `AArch64InstructionCache of inst_reg*iCOp diff --git a/aarch64_small/gen/fold.hgen b/aarch64_small/gen/fold.hgen index fbe52794..411262e5 100644 --- a/aarch64_small/gen/fold.hgen +++ b/aarch64_small/gen/fold.hgen @@ -43,3 +43,5 @@ | `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> fold_reg t (y_reg, y_sreg) | `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> fold_reg t (y_reg, y_sreg) | `AArch64MoveSystemImmediate (operand,field) -> (y_reg, y_sreg) +| `AArch64DataCache (t, dc_op) -> fold_reg t (y_reg, y_sreg) +| `AArch64InstructionCache (t, ic_op) -> fold_reg t (y_reg, y_sreg) diff --git a/aarch64_small/gen/lexer.hgen b/aarch64_small/gen/lexer.hgen index 6ff24317..e0550dd0 100644 --- a/aarch64_small/gen/lexer.hgen +++ b/aarch64_small/gen/lexer.hgen @@ -223,6 +223,9 @@ "MRS" , MRS {txt="MRS"} ; "MSR" , MSR {txt="MSR"} ; + "DC" , DC {txt="DC"} ; + "IC" , IC {txt="IC"} ; + (*** instructions/operands ***) @@ -307,3 +310,17 @@ "SPSel" , PSTATEFIELD (PSTATEField_SP) ; "DAIFSet" , PSTATEFIELD (PSTATEField_DAIFSet) ; "DAIFClr" , PSTATEFIELD (PSTATEField_DAIFClr) ; + + "IVAC" , DCOP (IVAC) ; + "ISW" , DCOP (ISW) ; + "CSW" , DCOP (CSW) ; + "CISW" , DCOP (CISW) ; + "ZVA" , DCOP (ZVA) ; + "CVAC" , DCOP (CVAC) ; + "CVAU" , DCOP (CVAU) ; + "CIVAC" , DCOP (CIVAC) ; + + "IALLUIS" , ICOP (IALLUIS) ; + "IALLU" , ICOP (IALLU) ; + "IVAU" , ICOP (IVAU) ; + diff --git a/aarch64_small/gen/map.hgen b/aarch64_small/gen/map.hgen index 3d5419b4..1957a03d 100644 --- a/aarch64_small/gen/map.hgen +++ b/aarch64_small/gen/map.hgen @@ -43,3 +43,5 @@ | `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> `AArch64TestBitAndBranch (map_reg t,datasize,bit_pos,bit_val,offset) | `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> `AArch64MoveSystemRegister (map_reg t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) | `AArch64MoveSystemImmediate (operand,field) -> `AArch64MoveSystemImmediate (operand,field) +| `AArch64DataCache (t, dc_op) -> `AArch64DataCache (map_reg t, dc_op) +| `AArch64InstructionCache (t, ic_op) -> `AArch64InstructionCache (map_reg t, ic_op) diff --git a/aarch64_small/gen/parser.hgen b/aarch64_small/gen/parser.hgen index 53fc1c8f..685dc218 100644 --- a/aarch64_small/gen/parser.hgen +++ b/aarch64_small/gen/parser.hgen @@ -1401,3 +1401,15 @@ | MSR SYSREG COMMA xreg { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <systemreg>, <Xt>") else `AArch64MoveSystemRegister($4,$2.sys_op0,$2.sys_op1,$2.sys_op2,$2.sys_crn,$2.sys_crm,false) } + + /* DC */ + + | DC DCOP COMMA xreg + { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <dc_op>, <Xt>") + else `AArch64DataCache($4,$2) } + + /* IC */ + + | IC ICOP COMMA xreg + { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <ic_op>, <Xt>") + else `AArch64InstructionCache($4,$2) } diff --git a/aarch64_small/gen/pretty.hgen b/aarch64_small/gen/pretty.hgen index b412fdda..998e58ad 100644 --- a/aarch64_small/gen/pretty.hgen +++ b/aarch64_small/gen/pretty.hgen @@ -394,3 +394,9 @@ | `AArch64MoveSystemImmediate (operand,field) -> sprintf "MSR %s,%s" (pp_pstatefield field) (pp_imm operand) + +| `AArch64DataCache (t, dc_op) -> + sprintf "DC %s,%s" (pp_dcop dc_op) (pp_regzr Set64 t) + +| `AArch64InstructionCache (t, ic_op) -> + sprintf "IC %s,%s" (pp_icop ic_op) (pp_regzr Set64 t) diff --git a/aarch64_small/gen/regs_out_in.hgen b/aarch64_small/gen/regs_out_in.hgen index bab53be7..72b1ac3c 100644 --- a/aarch64_small/gen/regs_out_in.hgen +++ b/aarch64_small/gen/regs_out_in.hgen @@ -154,3 +154,9 @@ | `AArch64MoveSystemImmediate (_operand,_field) -> ([], [], [], [Next]) + +| `AArch64DataCache (_t, _dc_op) -> + failwith "is anyone using this?" + +| `AArch64InstructionCache (_t, _ic_op) -> + failwith "is anyone using this?" diff --git a/aarch64_small/gen/sail_trans_out.hgen b/aarch64_small/gen/sail_trans_out.hgen index 0399fa8b..9f84411b 100644 --- a/aarch64_small/gen/sail_trans_out.hgen +++ b/aarch64_small/gen/sail_trans_out.hgen @@ -326,3 +326,11 @@ | "MoveSystemImmediate", [operand; field] -> `AArch64MoveSystemImmediate ( translate_out_int operand, translate_out_pSTATEField field) + +| "DataCache", [t; dc_op] -> + `AArch64DataCache ( translate_out_regzr Set64 t, + translate_out_dCOp dc_op) + +| "InstructionCache", [t; ic_op] -> + `AArch64InstructionCache (translate_out_regzr Set64 t, + translate_out_iCOp ic_op) diff --git a/aarch64_small/gen/token_types.hgen b/aarch64_small/gen/token_types.hgen index 411dddf9..bf17cd13 100644 --- a/aarch64_small/gen/token_types.hgen +++ b/aarch64_small/gen/token_types.hgen @@ -69,6 +69,8 @@ type token_RET = {txt : string} type token_TST = {txt : string} type token_MRS = {txt : string} type token_MSR = {txt : string} +type token_DC = {txt : string} +type token_IC = {txt : string} (*** instructions/operands ***) @@ -83,3 +85,5 @@ type token_BARROP = {domain : mBReqDomain; types : mBReqTypes} type token_PRFOP = inst_reg (* this is an int that is encoded in a reg field *) type token_SYSREG = {sys_op0 : uinteger; sys_op1 : uinteger; sys_op2 : uinteger; sys_crn : uinteger; sys_crm : uinteger} type token_PSTATEFIELD = pSTATEField +type token_DCOP = dCOp +type token_ICOP = iCOp diff --git a/aarch64_small/gen/tokens.hgen b/aarch64_small/gen/tokens.hgen index bf49e463..18142bc7 100644 --- a/aarch64_small/gen/tokens.hgen +++ b/aarch64_small/gen/tokens.hgen @@ -62,6 +62,8 @@ %token <AArch64HGenBase.token_TST> TST %token <AArch64HGenBase.token_MRS> MRS %token <AArch64HGenBase.token_MSR> MSR +%token <AArch64HGenBase.token_DC> DC +%token <AArch64HGenBase.token_IC> IC /*** instructions/operands ***/ @@ -75,4 +77,5 @@ %token <AArch64HGenBase.token_PRFOP> PRFOP %token <AArch64HGenBase.token_SYSREG> SYSREG %token <AArch64HGenBase.token_PSTATEFIELD> PSTATEFIELD - +%token <AArch64HGenBase.token_DCOP> DCOP +%token <AArch64HGenBase.token_ICOP> ICOP diff --git a/aarch64_small/gen/trans_sail.hgen b/aarch64_small/gen/trans_sail.hgen index df2ed81c..7ad837d9 100644 --- a/aarch64_small/gen/trans_sail.hgen +++ b/aarch64_small/gen/trans_sail.hgen @@ -379,3 +379,15 @@ [translate_bit4 "operand" operand; translate_pSTATEField "field" field], []) + +| `AArch64DataCache (t, dc_op) -> + ("DataCache", + [translate_reg "t" t; + translate_dCOp "dc_op" dc_op], + []) + +| `AArch64InstructionCache (t, ic_op) -> + ("InstructionCache", + [translate_reg "t" t; + translate_iCOp "ic_op" ic_op], + []) diff --git a/aarch64_small/gen/types.hgen b/aarch64_small/gen/types.hgen index d581a233..c2a9c3e0 100644 --- a/aarch64_small/gen/types.hgen +++ b/aarch64_small/gen/types.hgen @@ -88,3 +88,7 @@ type revOp = RevOp_RBIT | RevOp_REV16 | RevOp_REV32 | RevOp_REV64 type pSTATEField = PSTATEField_DAIFSet | PSTATEField_DAIFClr | PSTATEField_SP + +type dCOp = IVAC | ISW | CSW | CISW | ZVA | CVAC | CVAU | CIVAC + +type iCOp = IALLUIS | IALLU | IVAU diff --git a/aarch64_small/gen/types_sail_trans_out.hgen b/aarch64_small/gen/types_sail_trans_out.hgen index 082a5464..89fbad42 100644 --- a/aarch64_small/gen/types_sail_trans_out.hgen +++ b/aarch64_small/gen/types_sail_trans_out.hgen @@ -187,3 +187,22 @@ let translate_out_pSTATEField inst = | 1 -> PSTATEField_DAIFClr | 2 -> PSTATEField_SP | _ -> assert false + +let translate_out_dCOp inst = + match translate_out_enum inst with + | 0 -> IVAC + | 1 -> ISW + | 2 -> CSW + | 3 -> CISW + | 4 -> ZVA + | 5 -> CVAC + | 6 -> CVAU + | 7 -> CIVAC + | _ -> assert false + +let translate_out_iCOp inst = + match translate_out_enum inst with + | 0 -> IALLUIS + | 1 -> IALLU + | 2 -> IVAU + | _ -> assert false diff --git a/aarch64_small/gen/types_trans_sail.hgen b/aarch64_small/gen/types_trans_sail.hgen index 7f2d5fe7..8081e316 100644 --- a/aarch64_small/gen/types_trans_sail.hgen +++ b/aarch64_small/gen/types_trans_sail.hgen @@ -117,3 +117,9 @@ let translate_revOp = let translate_pSTATEField = translate_enum [PSTATEField_DAIFSet; PSTATEField_DAIFClr; PSTATEField_SP] + +let translate_dCOp = + translate_enum [IVAC; ISW; CSW; CISW; ZVA; CVAC; CVAU; CIVAC] + +let translate_iCOp = + translate_enum [IALLUIS; IALLU; IVAU] 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 |