From 3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 3 May 2018 15:30:55 +0100 Subject: Flow typing and l-expression changes for ASL parser 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ --- aarch64/no_vector/spec.sail | 343 ++++++++++++++++------------------- aarch64/prelude.sail | 38 +--- editors/sail2-mode.el | 1 + language/sail.ott | 1 + lib/smt.sail | 4 + src/ast_util.ml | 11 +- src/initial_check.ml | 60 +++--- src/interpreter.ml | 4 + src/parse_ast.ml | 1 + src/pretty_print_sail.ml | 1 + src/rewriter.ml | 11 +- src/rewriter.mli | 3 +- src/rewrites.ml | 32 ++-- src/sail.ml | 3 + src/type_check.ml | 267 +++++++++++++-------------- src/type_check.mli | 9 +- src/value.ml | 5 + test/arm/run_tests.sh | 4 +- test/ocaml/bitfield/bitfield.sail | 7 - test/ocaml/lsl/lsl.sail | 3 - test/ocaml/prelude.sail | 290 +---------------------------- test/ocaml/string_of_struct/sos.sail | 5 - test/ocaml/types/types.sail | 2 - test/ocaml/vec_32_64/vec_32_64.sail | 5 - test/typecheck/pass/nzcv.sail | 2 +- test/typecheck/pass/while_PM.sail | 6 +- 26 files changed, 409 insertions(+), 709 deletions(-) diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index ccf8aba1..024393ad 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -1702,9 +1702,9 @@ function ExternalInvasiveDebugEnabled () = return(DBGEN == HIGH) val ConstrainUnpredictableInteger : (int, int, Unpredictable) -> (Constraint, int) effect {undef} -function ConstrainUnpredictableInteger (low, high, which) = { +function ConstrainUnpredictableInteger ('low, 'high, which) = { c : Constraint = ConstrainUnpredictable(which); - if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined : int)) + if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined)) } val ConstrainUnpredictableBool : Unpredictable -> bool effect {escape} @@ -1803,7 +1803,7 @@ function LookUpRIndex ('n, mode) = { return(result) } -val HighestSetBit : forall ('N : Int), 'N >= 2. bits('N) -> int +val HighestSetBit : forall ('N : Int), 'N >= 0. bits('N) -> int function HighestSetBit x = { foreach (i from ('N - 1) to 0 by 1 in dec) @@ -1819,12 +1819,13 @@ val CountLeadingSignBits : forall ('N : Int), 'N >= 3. bits('N) -> int function CountLeadingSignBits x = return(CountLeadingZeroBits(x[(('N - 1) - 1) + 1 .. 1] ^ x[('N - 1) - 1 .. 0])) -val BitReverse : forall ('N : Int), 'N >= 2. bits('N) -> bits('N) effect {undef} +val BitReverse : forall ('N : Int), 'N >= 0 & 'N >= 0. + bits('N) -> bits('N) effect {undef} function BitReverse data = { result : bits('N) = undefined; foreach (i from 0 to ('N - 1) by 1 in inc) - result[('N - i) - 1 .. ('N - i) - 1] = [data[i]]; + result = __SetSlice_bits('N, 1, result, ('N - i) - 1, [data[i]]); return(result) } @@ -2063,9 +2064,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0. function Replicate x = { assert('N % 'M == 0, "((N MOD M) == 0)"); - let 'p = ex_int('N / 'M); - assert(constraint('N = 'p * 'M)); - return(replicate_bits(x, p)) + return(replicate_bits(x, 'N / 'M)) } val Zeros__0 : forall ('N : Int), 'N >= 0. atom('N) -> bits('N) @@ -2306,7 +2305,7 @@ val ConstrainUnpredictableBits : forall ('width : Int), 'width >= 0. function ConstrainUnpredictableBits which = { c : Constraint = ConstrainUnpredictable(which); - if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined : bits('width))) + if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined)) } val AArch64_SysInstrWithResult : (int, int, int, int, int) -> bits(64) effect {escape} @@ -2741,17 +2740,15 @@ function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) aset_X(d, result) } -val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, wreg, undef, rreg} +val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, rreg, undef, wreg} -function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = { +function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint('container_size >= 0 + 1)); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); operand : bits('datasize) = aget_X(n); result : bits('datasize) = undefined; - let 'containers : int = datasize / container_size; - assert(constraint('containers * 'container_size = 'datasize)); - let 'elements_per_container : int = container_size / 8; - assert(constraint('elements_per_container * 8 = 'container_size)); + containers : int = datasize / container_size; + elements_per_container : int = container_size / 8; index : int = 0; rev_index : int = undefined; foreach (c from 0 to (containers - 1) by 1 in inc) { @@ -2928,7 +2925,7 @@ function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflag nzcv : bits(4) = undefined; if sub_op then operand2 = ~(operand2) else (); (result, nzcv) = AddWithCarry(operand1, operand2, PSTATE.C); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); aset_X(d, result) } @@ -3102,7 +3099,7 @@ function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, LogicalOp_ORR => result = operand1 | operand2, LogicalOp_EOR => result = operand1 ^ operand2 }; - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); aset_X(d, result) } @@ -3121,7 +3118,7 @@ function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, se carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); aset_X(d, result) } @@ -3254,7 +3251,7 @@ function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) LogicalOp_ORR => result = operand1 | operand2, LogicalOp_EOR => result = operand1 ^ operand2 }; - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3274,7 +3271,7 @@ function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, set carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3293,7 +3290,7 @@ function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_ty carry_in = 0b1 } else carry_in = 0b0; (result, nzcv) = AddWithCarry(operand1, operand2, carry_in); - if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else (); + if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else (); if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result) } @@ -3972,7 +3969,7 @@ function FPToFixedJS (op, fpcr, Is64) = { } else (); if sign == 0b1 & value_name == 0.0 then Z = 0b0 else (); if typ == FPType_Infinity then result = 0 else (); - if Is64 then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00); + if Is64 then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00); return(__GetSlice_int(32, result, 0)) } @@ -4479,11 +4476,11 @@ function Halt reason = { else assert([EDSCR[16]] == 0b1, "((EDSCR).SDD == '1')"); EDSCR[20 .. 20] = 0b0; if UsingAArch32() then { - (PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(4); + (PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(4); PSTATE.IT = 0x00; PSTATE.T = 0b1 } else - (PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(5); + (PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(5); PSTATE.IL = 0b0; StopInstructionPrefetchAndEnableITR(); EDSCR[5 .. 0] = reason; @@ -4915,7 +4912,7 @@ function aarch64_integer_conditional_compare_register (condition, 'datasize, fla } else (); (__anon1, flags) = AddWithCarry(operand1, operand2, carry_in) } else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val integer_conditional_compare_register_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, rreg, undef, wreg} @@ -4949,7 +4946,7 @@ function aarch64_integer_conditional_compare_immediate (condition, datasize, fla } else (); (__anon1, flags) = AddWithCarry(operand1, operand2, carry_in) } else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val integer_conditional_compare_immediate_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, wreg, undef, rreg} @@ -6004,13 +6001,13 @@ function AArch64_TranslateAddressS1Off (vaddress, acctype, iswrite) = { return(result) } -val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {wreg, undef, rreg, escape} +val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {escape, rreg, undef, wreg} function AArch64_MaybeZeroRegisterUppers () = { assert(UsingAArch32(), "UsingAArch32()"); include_R15_name : bool = undefined; - last : range(14, 30) = undefined; - first : atom(0) = 0; + last : int = undefined; + first : int = undefined; if PSTATE.EL == EL0 & ~(ELUsingAArch32(EL1)) then { first = 0; last = 14; @@ -6025,9 +6022,9 @@ function AArch64_MaybeZeroRegisterUppers () = { include_R15_name = true }; foreach (n from first to last by 1 in inc) - if (n : int != 15 : int | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then { + if (n != 15 | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then { __tmp_3 : bits(64) = _R[n]; - __tmp_3[63 .. 32] = Zeros(32); + __tmp_3 = __SetSlice_bits(64, 32, __tmp_3, 32, Zeros()); _R[n] = __tmp_3 } else (); () @@ -6800,9 +6797,21 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb return((priv_match & security_state_match) & (~(linked) | linked_match)) } -val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool +val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool effect {escape, rreg, undef} -function AArch64_WatchpointMatch (n, vaddress, size, ispriv, iswrite) = false +function AArch64_WatchpointMatch ('n, vaddress, 'size, ispriv, iswrite) = { + assert(~(ELUsingAArch32(S1TranslationRegime())), "!(ELUsingAArch32(S1TranslationRegime()))"); + assert(n <= UInt(slice(ID_AA64DFR0_EL1, 20, 4)), "(n <= UInt((ID_AA64DFR0_EL1).WRPs))"); + enabled : bool = [DBGWCR_EL1[n][0]] == 0b1; + linked : bool = [DBGWCR_EL1[n][20]] == 0b1; + isbreakpnt : bool = false; + state_match : bool = AArch64_StateMatch(slice(DBGWCR_EL1[n], 14, 2), [DBGWCR_EL1[n][13]], slice(DBGWCR_EL1[n], 1, 2), linked, slice(DBGWCR_EL1[n], 16, 4), isbreakpnt, ispriv); + ls_match : bool = [slice(DBGWCR_EL1[n], 3, 2)[if iswrite then 1 else 0]] == 0b1; + value_match_name : bool = false; + foreach (byte from 0 to (size - 1) by 1 in inc) + value_match_name = value_match_name | AArch64_WatchpointByteMatch(n, vaddress + byte); + return(((value_match_name & state_match) & ls_match) & enabled) +} val AArch64_BreakpointMatch : (int, bits(64), int) -> bool effect {escape, rreg, undef} @@ -6955,7 +6964,7 @@ function AArch64_TakeReset cold_reset = { else PSTATE.EL = EL1; AArch64_ResetControlRegisters(cold_reset); PSTATE.SP = 0b1; - (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF; + (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF; PSTATE.SS = 0b0; PSTATE.IL = 0b0; AArch64_ResetGeneralRegisters(); @@ -6991,11 +7000,18 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return if from_32 then AArch64_MaybeZeroRegisterUppers() else (); if UInt(target_el) > UInt(PSTATE.EL) then { lower_32 : bool = undefined; - if target_el == EL3 then if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2) else lower_32 = ELUsingAArch32(EL1) else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then lower_32 = ELUsingAArch32(EL0) else lower_32 = ELUsingAArch32(target_el - 1); + if target_el == EL3 then + if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2) + else lower_32 = ELUsingAArch32(EL1) + else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then + lower_32 = ELUsingAArch32(EL0) + else lower_32 = ELUsingAArch32(target_el - 1); vect_offset = vect_offset + (if lower_32 then 1536 else 1024) - } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512 else (); + } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512 + else (); spsr : bits(32) = GetPSRFromPSTATE(); - if HaveUAOExt() then PSTATE.UAO = 0b0 else (); + if HaveUAOExt() then PSTATE.UAO = 0b0 + else (); if ~(exception.typ == Exception_IRQ | exception.typ == Exception_FIQ) then AArch64_ReportException(exception, target_el) else (); PSTATE.EL = target_el; PSTATE.nRW = 0b0; @@ -7003,13 +7019,15 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return aset_SPSR(spsr); aset_ELR(preferred_exception_return); PSTATE.SS = 0b0; - (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF; + (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF; PSTATE.IL = 0b0; if from_32 then { PSTATE.IT = 0x00; PSTATE.T = 0b0 } else (); - if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then PSTATE.PAN = 0b1 else (); + if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then + PSTATE.PAN = 0b1 + else (); BranchTo(slice(aget_VBAR(), 11, 53) @ __GetSlice_int(11, vect_offset, 0), BranchType_EXCEPTION); iesb_req : bool = undefined; if HaveRASExt() & [aget_SCTLR()[21]] == 0b1 then { @@ -7960,7 +7978,7 @@ function AArch32_EnterMode (target_mode, preferred_exception_return, 'lr_offset, aset_R(14, preferred_exception_return + lr_offset); PSTATE.T = [SCTLR[30]]; PSTATE.SS = 0b0; - if target_mode == M32_FIQ then (PSTATE.A, PSTATE.I, PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A, PSTATE.I) = 0b11 else PSTATE.I = 0b1; + if target_mode == M32_FIQ then (PSTATE.A @ PSTATE.I @ PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A @ PSTATE.I) = 0b11 else PSTATE.I = 0b1; PSTATE.E = [SCTLR[25]]; PSTATE.IL = 0b0; PSTATE.IT = 0x00; @@ -8120,7 +8138,7 @@ function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_ CheckFPAdvSIMDEnabled64(); operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR) + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR) } val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit effect {escape, rreg, undef, wreg} @@ -8133,7 +8151,7 @@ function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, s operand1 : bits('datasize) = aget_V(n); operand2 : bits('datasize) = aget_V(m); if ConditionHolds(condition) then flags = FPCompare(operand1, operand2, signal_all_nans, FPCR) else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags } val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect {escape, rreg, undef, wreg} @@ -8585,11 +8603,11 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo } else () } -val aarch64_memory_single_simdfp_register : forall ('datasize : Int). - (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg} +val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type, m, memop, n, postindex, shift, t, wback) = { +function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); offset : bits(64) = ExtendReg(m, extend_type, shift); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; @@ -8598,32 +8616,28 @@ function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type, CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint(8 * 'dq8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_simdfp_immediate_signed_postidx : forall ('datasize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg} +val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, t, wback) = { +function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8631,32 +8645,28 @@ function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasiz CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint('dq8 * 8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_simdfp_immediate_signed_offset_normal : forall ('datasize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, t, wback) = { +function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; data : bits('datasize) = undefined; @@ -8664,23 +8674,19 @@ function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, d CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); - let 'dq8 = ex_int(datasize / 8); - assert(constraint(8 * 'dq8 = 'datasize)); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { data = aget_V(t); - aset_Mem(address, dq8, acctype, data) + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dq8, acctype); + data = aget_Mem(address, datasize / 8, acctype); aset_V(t, data) } }; if wback then { - if postindex then address = address + offset - else (); + if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } @@ -8807,41 +8813,39 @@ function memory_literal_general_decode (opc, V, imm19, Rt) = { aarch64_memory_literal_general(memop, offset, signed, size, t) } -val aarch64_memory_atomicops_swp : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_swp : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_swp (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint"); +function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + assert(constraint('regsize >= 0), "regsize constraint"); + let 'dbytes = ex_int(datasize / 8); + assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); address : bits(64) = undefined; data : bits('datasize) = undefined; - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - aset_Mem(address, dbytes, stacctype, aget_X(s)); + data = aget_Mem(address, datasize / 8, ldacctype); + aset_Mem(address, datasize / 8, stacctype, aget_X(s)); aset_X(t, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_st : forall ('datasize : Int). - (atom('datasize), AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype) = { +function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = let 'dbytes = ex_int(datasize / 8) in { assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; result : bits('datasize) = undefined; value_name = aget_X(s); - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); + data = aget_Mem(address, datasize / 8, ldacctype); match op { MemAtomicOp_ADD => result = data + value_name, MemAtomicOp_BIC => result = data & ~(value_name), @@ -8852,26 +8856,26 @@ function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype) MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name, MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data }; - aset_Mem(address, dbytes, stacctype, result) + aset_Mem(address, datasize / 8, stacctype, result) } -val aarch64_memory_atomicops_ld : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, MemAtomicOp, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_ld : (int, AccType, int, MemAtomicOp, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, stacctype, t) = { - assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint"); +function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's, stacctype, 't) = { + assert(constraint('regsize >= 0), "regsize constraint"); + let 'dbytes = ex_int(datasize / 8); + assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); address : bits(64) = undefined; value_name : bits('datasize) = undefined; data : bits('datasize) = undefined; result : bits('datasize) = undefined; value_name = aget_X(s); - let 'dbytes = ex_int(datasize / 8); - assert(constraint(8 * 'dbytes = 'datasize)); if n == 31 then { CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); + data = aget_Mem(address, datasize / 8, ldacctype); match op { MemAtomicOp_ADD => result = data + value_name, MemAtomicOp_BIC => result = data & ~(value_name), @@ -8882,15 +8886,14 @@ function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, st MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name, MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data }; - aset_Mem(address, dbytes, stacctype, result); + aset_Mem(address, datasize / 8, stacctype, result); aset_X(t, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_cas_single : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_cas_single : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -8904,19 +8907,18 @@ function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else (); + data = aget_Mem(address, datasize / 8, ldacctype); + if data == comparevalue then aset_Mem(address, datasize / 8, stacctype, newvalue) else (); aset_X(s, ZeroExtend(data, regsize)) } -val aarch64_memory_atomicops_cas_pair : forall ('datasize : Int) ('regsize : Int). - (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem} +val aarch64_memory_atomicops_cas_pair : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s, stacctype, t) = { - assert(constraint('regsize >= 0), "destsize constraint"); - let 'dbytes = ex_int((2 * datasize) / 8); +function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = { + assert(constraint('regsize >= 0), "regsize constraint"); + let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); - assert(constraint(4 * 'dbytes = 'datasize), "dbytes constraint"); + assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); address : bits(64) = undefined; comparevalue : bits(2 * 'datasize) = undefined; newvalue : bits(2 * 'datasize) = undefined; @@ -8931,8 +8933,8 @@ function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s, CheckSPAlignment(); address = aget_SP() } else address = aget_X(n); - data = aget_Mem(address, dbytes, ldacctype); - if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else (); + data = aget_Mem(address, (2 * datasize) / 8, ldacctype); + if data == comparevalue then aset_Mem(address, (2 * datasize) / 8, stacctype, newvalue) else (); if BigEndian() then { aset_X(s, ZeroExtend(slice(data, datasize, datasize), regsize)); aset_X(s + 1, ZeroExtend(slice(data, 0, datasize), regsize)) @@ -9051,15 +9053,15 @@ function SetPSTATEFromPSR spsr__arg = { } }; if PSTATE.IL == 0b1 & PSTATE.nRW == 0b1 then if ConstrainUnpredictableBool(Unpredictable_ILZEROT) then spsr = __SetSlice_bits(32, 1, spsr, 5, 0b0) else () else (); - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = slice(spsr, 28, 4); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = slice(spsr, 28, 4); if PSTATE.nRW == 0b1 then { PSTATE.Q = [spsr[27]]; PSTATE.IT = RestoredITBits(spsr); PSTATE.GE = slice(spsr, 16, 4); PSTATE.E = [spsr[9]]; - (PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 3); + (PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 3); PSTATE.T = [spsr[5]] - } else (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 4); + } else (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 4); if HavePANExt() then PSTATE.PAN = [spsr[22]] else (); if HaveUAOExt() then PSTATE.UAO = [spsr[23]] else (); () @@ -9072,13 +9074,13 @@ function DRPSInstruction () = { if (HaveRASExt() & [aget_SCTLR()[21]] == 0b1) & ConstrainUnpredictableBool(Unpredictable_IESBinDebug) then ErrorSynchronizationBarrier(MBReqDomain_FullSystem, MBReqTypes_All) else (); SetPSTATEFromPSR(aget_SPSR()); if UsingAArch32() then { - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.Q, PSTATE.GE, PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(13); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.Q @ PSTATE.GE @ PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(13); PSTATE.IT = 0x00; PSTATE.T = 0b1; DLR = undefined : bits(32); DSPSR = undefined : bits(32) } else { - (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(9); + (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(9); DLR_EL0 = undefined : bits(64); DSPSR_EL0 = undefined : bits(32) }; @@ -9191,11 +9193,10 @@ function system_exceptions_runtime_hvc_decode (opc, imm16, op2, LL) = { aarch64_system_exceptions_runtime_hvc(imm) } -val aarch64_memory_single_general_register : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, atom('regsize), int, bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_register (acctype, datasize, extend_type, m, memop, n, postindex, regsize, shift, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'regsize, 'shift, signed, 't, wback__arg) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -9230,33 +9231,28 @@ function aarch64_memory_single_general_register (acctype, datasize, extend_type, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_unsigned : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem} +val aarch64_memory_single_general_immediate_unsigned : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -9290,33 +9286,28 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, me if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_signed_postidx : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem} +val aarch64_memory_single_general_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -9350,24 +9341,20 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasi if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } @@ -9404,11 +9391,10 @@ function aarch64_memory_single_general_immediate_signed_pac ('n, offset, 't, use } else () } -val aarch64_memory_single_general_immediate_signed_offset_unpriv : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_immediate_signed_offset_unpriv : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -9442,33 +9428,28 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } -val aarch64_memory_single_general_immediate_signed_offset_normal : forall ('datasize : Int) ('regsize : Int). - (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem} +val aarch64_memory_single_general_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg} -function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = { - assert(constraint('regsize >= 0), "destsize constraint"); +function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = { + assert(constraint('regsize >= 0), "regsize constraint"); let 'dbytes = ex_int(datasize / 8); assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint"); assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint"); @@ -9502,24 +9483,20 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, if memop != MemOp_PREFETCH then CheckSPAlignment() else (); address = aget_SP() } else address = aget_X(n); - if ~(postindex) then address = address + offset - else (); + if ~(postindex) then address = address + offset else (); match memop { MemOp_STORE => { - if rt_unknown then data = undefined - else data = aget_X(t); - aset_Mem(address, dbytes, acctype, data) + if rt_unknown then data = undefined else data = aget_X(t); + aset_Mem(address, datasize / 8, acctype, data) }, MemOp_LOAD => { - data = aget_Mem(address, dbytes, acctype); + data = aget_Mem(address, datasize / 8, acctype); if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize)) }, MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0)) }; if wback then { - if wb_unknown then address = undefined - else if postindex then address = address + offset - else (); + if wb_unknown then address = undefined else if postindex then address = address + offset else (); if n == 31 then aset_SP(address) else aset_X(n, address) } else () } diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 5cf4ce48..097dc7d9 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -1,7 +1,7 @@ default Order dec $include -$include +$include type bits ('n : Int) = vector('n, dec, bit) @@ -202,11 +202,6 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power"} : overload operator ^ = {xor_vec, int_power, real_power} -val add_range = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int - val add_vec = { ocaml: "add_vec", lem: "add_vec", @@ -221,12 +216,7 @@ val add_vec_int = { val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real"} : (real, real) -> real -overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} - -val sub_range = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : (int, int) -> int +overload operator + = {add_vec, add_vec_int, add_real} val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -238,24 +228,15 @@ val sub_vec_int = { val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real"} : (real, real) -> real -val negate_range = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) - -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : int -> int - val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real"} : real -> real -overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} +overload operator - = {sub_vec, sub_vec_int, sub_real} -overload negate = {negate_range, negate_int, negate_real} - -val mult_range = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) - -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : (int, int) -> int +overload negate = {negate_real} val mult_real = {ocaml: "mult_real", lem: "realMult", c: "mult_real"} : (real, real) -> real -overload operator * = {mult_range, mult_int, mult_real} +overload operator * = {mult_real} val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real"} : real -> real @@ -279,11 +260,9 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down"} : real val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up"} : real -> int -val abs_int = "abs_int" : int -> int - val abs_real = "abs_real" : real -> real -overload abs = {abs_atom, abs_int, abs_real} +overload abs = {abs_atom, abs_real} val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (nat, nat) -> nat @@ -299,10 +278,6 @@ overload operator % = {modulus} val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> real -val shl_int = "shl_int" : (int, int) -> int - -val shr_int = "shr_int" : (int, int) -> int - val min_nat = {ocaml: "min_int", lem: "min", c: "max_int"} : (nat, nat) -> nat val min_int = {ocaml: "min_int", lem: "min", c: "max_int"} : (int, int) -> int @@ -355,7 +330,6 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) -val print_int = "print_int" : (string, int) -> unit val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit val break : unit -> unit diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index 4b1fa7a2..b8683a1b 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -29,6 +29,7 @@ (,(regexp-opt sail2-types 'symbols) . font-lock-type-face) (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face) ("~" . font-lock-negation-char-face) + ("@" . font-lock-preprocessor-face) ("<->" . font-lock-negation-char-face) ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face) ("\\([a-zA-Z0-9_]+\\)(" 1 font-lock-function-name-face) diff --git a/language/sail.ott b/language/sail.ott index ce05797f..8469e029 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -830,6 +830,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} | ( typ ) id :: :: cast {{ com cast }} | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} + | lexp1 @ ... @ lexpn :: :: vector_concat {{ com vector concatenation L-exp }} | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too diff --git a/lib/smt.sail b/lib/smt.sail index f8521a4a..ae672947 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -10,6 +10,8 @@ val div = { c: "div_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)} +overload operator / = {div} + val mod = { smt: "mod", ocaml: "modulus", @@ -17,6 +19,8 @@ val mod = { c: "mod_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} +overload operator % = {mod} + val abs_atom = { smt : "abs", ocaml: "abs_int", diff --git a/src/ast_util.ml b/src/ast_util.ml index 2f2d27d8..f7574b9d 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -449,6 +449,7 @@ and map_lexp_annot_aux f = function | LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps) | LEXP_cast (typ, id) -> LEXP_cast (typ, id) | LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps) + | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (map_lexp_annot f) lexps) | LEXP_vector (lexp, exp) -> LEXP_vector (map_lexp_annot f lexp, map_exp_annot f exp) | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2) | LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id) @@ -645,8 +646,8 @@ let rec string_of_exp (E_aux (exp, _)) = | E_try (exp, cases) -> "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}" | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp - | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind - | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp + | E_assign (lexp, bind) -> string_of_lexp lexp ^ " = " ^ string_of_exp bind + | E_cast (typ, exp) -> string_of_exp exp ^ " : " ^ string_of_typ typ | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]" | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]" | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]" @@ -702,7 +703,7 @@ and string_of_pat (P_aux (pat, l)) = | P_wild -> "_" | P_id v -> string_of_id v | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat - | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat + | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2 @@ -719,7 +720,9 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" | LEXP_vector_range (lexp, exp1, exp2) -> - string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]" + string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ " .. " ^ string_of_exp exp2 ^ "]" + | LEXP_vector_concat lexps -> + string_of_list " @ " string_of_lexp lexps | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" and string_of_letbind (LB_aux (lb, l)) = diff --git a/src/initial_check.ml b/src/initial_check.ml index 62c1af02..1ba1b9e6 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -539,35 +539,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = - LEXP_aux( - (match exp with - | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) - | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp) - | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> - LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) - | Parse_ast.E_tuple(tups) -> + let lexp = match exp with + | Parse_ast.E_id id -> LEXP_id (to_ast_id id) + | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp) + | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) -> + LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id) + | Parse_ast.E_tuple tups -> let ltups = List.map (to_ast_lexp k_env def_ord) tups in - let is_ok_in_tup (LEXP_aux (le,(l,_))) = + let is_ok_in_tup (LEXP_aux (le, (l, _))) = match le with - | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () + | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () | LEXP_memory _ | LEXP_deref _ -> - typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in + typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None + in List.iter is_ok_in_tup ltups; - LEXP_tup(ltups) - | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> - (match f with - | Parse_ast.Id(id) -> - (match List.map (to_ast_exp k_env def_ord) args with - | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[]) - | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps) - | args -> LEXP_memory(to_ast_id f', args)) - | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) - | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> - LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id) - | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None) - , (l,())) + LEXP_tup ltups + | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) -> + begin match f with + | Parse_ast.Id(id) -> + (match List.map (to_ast_exp k_env def_ord) args with + | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', []) + | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps) + | args -> LEXP_memory(to_ast_id f', args)) + | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None + end + | Parse_ast.E_vector_append (exp1, exp2) -> + LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2) + | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) + | Parse_ast.E_vector_subrange (vexp, exp1, exp2) -> + LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) + | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id) + | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None + in + LEXP_aux (lexp, (l, ())) + +and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) = + match exp_aux with + | Parse_ast.E_vector_append (exp1, exp2) -> + to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2 + | _ -> [to_ast_lexp k_env def_ord exp] and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp = match pex with diff --git a/src/interpreter.ml b/src/interpreter.ml index 87439e83..e62fcfc3 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -505,6 +505,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment" + | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment" (* let values = coerce_tuple (value_of_exp exp) in wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values)) @@ -556,6 +557,9 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps)) | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp)) | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2)) + | LEXP_vector_concat [] -> failwith "Empty LEXP_vector_concat node in exp_of_lexp" + | LEXP_vector_concat [lexp] -> exp_of_lexp lexp + | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps)))) | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) and pattern_match env (P_aux (p_aux, _) as pat) value = diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 826d8eb1..55ed57d2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -517,6 +517,7 @@ lexp_aux = (* lvalue expression, can't occur out of the parser *) | LEXP_mem of id * (exp) list | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) + | LEXP_vector_concat of lexp list | LEXP_field of lexp * id (* struct field *) and lexp = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c0658a83..5a26cb42 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -418,6 +418,7 @@ and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LEXP_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps) | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) | _ -> parens (doc_lexp lexp) and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace diff --git a/src/rewriter.ml b/src/rewriter.ml index 203e8a58..82e3ab05 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -197,6 +197,8 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with | LEXP_memory (_,es) -> union_eff_exps es | LEXP_tup les -> List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les + | LEXP_vector_concat les -> + List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) | LEXP_vector_range (lexp,e1,e2) -> union_effects (effect_of_lexp lexp) @@ -384,6 +386,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters exp1, rewriters.rewrite_exp rewriters exp2)) + | LEXP_vector_concat lexps -> rewrap (LEXP_vector_concat (List.map (rewriters.rewrite_lexp rewriters) lexps)) | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id)) let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = @@ -556,6 +559,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -635,7 +639,8 @@ and fold_lexp_aux alg = function | LEXP_vector (lexp,e) -> alg.lEXP_vector (fold_lexp alg lexp, fold_exp alg e) | LEXP_vector_range (lexp,e1,e2) -> alg.lEXP_vector_range (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2) - | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) + | LEXP_vector_concat les -> alg.lEXP_vector_concat (List.map (fold_lexp alg) les) + | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) and fold_lexp alg (LEXP_aux (lexp_aux,annot)) = alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot) and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e) @@ -706,6 +711,7 @@ let id_exp_alg = ; lEXP_tup = (fun tups -> LEXP_tup tups) ; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2)) ; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3)) + ; lEXP_vector_concat = (fun lexps -> LEXP_vector_concat lexps) ; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id)) ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot)) ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e)) @@ -813,6 +819,9 @@ let compute_exp_alg bot join = ; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2))) ; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) -> (join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3))) + ; lEXP_vector_concat = (fun ls -> + let (vs,ls) = List.split ls in + (join_list vs, LEXP_vector_concat ls)) ; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id))) ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot))) ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e))) diff --git a/src/rewriter.mli b/src/rewriter.mli index f8982d69..ccc1f951 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -155,6 +155,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -167,7 +168,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } diff --git a/src/rewrites.ml b/src/rewrites.ml index cfeae1e3..a61f2622 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -127,7 +127,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local lexp env @@ -136,7 +136,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_unbound id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env @@ -281,7 +281,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = scope. *) | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) -> let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in - Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) + Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) | _ -> begin match destruct_vector env typ with @@ -293,12 +293,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with | Nexp_sum (n1, n2) -> - mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2])) | Nexp_minus (n1, n2) -> - mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2])) | Nexp_times (n1, n2) -> - mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2])) - | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp])) + mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2])) + | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp])) | _ -> mk_exp (E_sizeof nexp) in let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) = @@ -487,6 +487,7 @@ let rewrite_sizeof (Defs defs) = ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2'))) ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3'))) + ; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps')) ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id))) ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot))) ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e'))) @@ -2281,11 +2282,11 @@ let rewrite_simple_types (Defs defs) = let defs = Defs (List.map simple_def defs) in rewrite_defs_base simple_defs defs -let rewrite_tuple_vector_assignments defs = +let rewrite_vector_concat_assignments defs = let assign_tuple e_aux annot = let env = env_of_annot annot in match e_aux with - | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) -> + | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) -> let typ = Env.base_typ_of env (typ_of exp) in if is_vector_typ typ then (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) @@ -2518,8 +2519,11 @@ let rewrite_defs_letbind_effects = | LEXP_vector_range (lexp,e1,e2) -> n_lexp lexp (fun lexp -> n_exp_name e1 (fun e1 -> - n_exp_name e2 (fun e2 -> + n_exp_name e2 (fun e2 -> k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) + | LEXP_vector_concat es -> + n_lexpL es (fun es -> + k (fix_eff_lexp (LEXP_aux (LEXP_vector_concat es,annot)))) | LEXP_field (lexp,id) -> n_lexp lexp (fun lexp -> k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) @@ -3198,7 +3202,7 @@ let merge_funcls (Defs defs) = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem = [ - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3233,7 +3237,7 @@ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3252,7 +3256,7 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3268,7 +3272,7 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); diff --git a/src/sail.ml b/src/sail.ml index 4d32fb94..f459d774 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -157,6 +157,9 @@ let options = Arg.align ([ ( "-enum_casts", Arg.Set Initial_check.opt_enum_casts, " allow enumerations to be automatically casted to numeric range types"); + ( "-no_lexp_bounds_check", + Arg.Set Type_check.opt_no_lexp_bounds_check, + " turn off bounds checking for vector assignments in l-expressions"); ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); diff --git a/src/type_check.ml b/src/type_check.ml index de4c22c3..65d07859 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -63,6 +63,10 @@ let opt_tc_debug = ref 0 re-writer passes, so it should only be used for debugging. *) let opt_no_effects = ref false +(* opt_no_lexp_bounds_check turns of the bounds checking in vector + assignments in l-expressions *) +let opt_no_lexp_bounds_check = ref false + let depth = ref 0 let rec indent n = match n with @@ -314,6 +318,7 @@ module Env : sig val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t val get_flow : id -> t -> typ -> typ + val remove_flow : id -> t -> t val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t @@ -346,7 +351,7 @@ module Env : sig val add_cast : id -> t -> t val allow_polymorphic_undefineds : t -> t val polymorphic_undefineds : t -> bool - val lookup_id : id -> t -> lvar + val lookup_id : ?raw:bool -> id -> t -> lvar val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val canonicalize : t -> typ -> typ @@ -856,10 +861,12 @@ end = struct | Not_found -> fun typ -> typ let add_flow id f env = - begin - typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); - { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } - end + typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } + + let remove_flow id env = + typ_print (lazy ("Removing flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.remove id env.flow } let is_register id env = Bindings.mem id env.registers @@ -898,11 +905,11 @@ end = struct let get_locals env = env.locals - let lookup_id id env = + let lookup_id ?raw:(raw=false) id env = try let (mut, typ) = Bindings.find id env.locals in let flow = get_flow id env in - Local (mut, flow typ) + Local (mut, if raw then typ else flow typ) with | Not_found -> begin @@ -943,12 +950,11 @@ end = struct let add_constraint (NC_aux (nc_aux, l) as constr) env = wf_constraint env constr; - begin - typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); - match nc_aux with - | NC_true -> env - | _ -> { env with constraints = constr :: env.constraints } - end + match nc_aux with + | NC_true -> env + | _ -> + typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); + { env with constraints = constr :: env.constraints } let get_ret_typ env = env.ret_typ @@ -1095,6 +1101,12 @@ let destruct_numeric env typ = Some ([kid], nc_true, nvar kid) | _, _ -> None +let bind_numeric l typ env = + match destruct_numeric env typ with + | Some (kids, nc, nexp) -> + nexp, add_existential kids nc env + | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric") + (** Pull an (potentially)-existentially qualified type into the global typing environment **) let bind_existential typ env = @@ -1224,7 +1236,7 @@ let prove_z3' env constr = | Constraint.Unknown -> typ_debug (lazy "unknown"); false let prove_z3 env nc = - typ_print (lazy ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); + typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc)) let solve env nexp = @@ -1743,7 +1755,10 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with | Some (kids, nc, typ1), _ -> let env = add_existential kids nc env in subtyp l env typ1 typ2 + (* | None, ([], _, typ2) -> + typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *) | None, (kids, nc, typ2) -> + typ_debug (lazy "Subtype check with unification"); let env = add_typ_vars kids env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in let unifiers, existential_kids, existential_nc = @@ -1913,6 +1928,10 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) +let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot) + (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with @@ -2096,7 +2115,7 @@ let rec filter_casts env from_typ to_typ casts = let crule r env exp typ = incr depth; - typ_print (lazy ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); + typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); try let checked_exp = r env exp typ in decr depth; checked_exp @@ -2107,7 +2126,7 @@ let irule r env exp = incr depth; try let inferred_exp = r env exp in - typ_print (lazy ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); + typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); decr depth; inferred_exp with @@ -2695,7 +2714,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in annot_assign tlexp checked_exp, env' | LEXP_id v when has_typ v env -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Mutable, vtyp) | Register vtyp -> let checked_exp = crule check_exp env exp vtyp in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in @@ -2708,9 +2727,26 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign tlexp inferred_exp, env' and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = + typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ)); let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in match lexp_aux with + | LEXP_cast (typ_annot, v) -> + begin match Env.lookup_id ~raw:true v env with + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Mutable, vtyp) -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + | Register vtyp -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env + | Unbound -> + subtyp l env typ typ_annot; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + end | LEXP_deref exp -> let inferred_exp = infer_exp env exp in begin match typ_of inferred_exp with @@ -2719,39 +2755,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env | _ -> - typ_error l (string_of_typ typ ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")") + typ_error l (string_of_typ typ ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")") end | LEXP_id v -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Immutable, _) | Enum _ -> typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end - | LEXP_cast (typ_annot, v) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - | Register vtyp -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env - end - | Unbound -> - begin - subtyp l env typ typ_annot; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - end | LEXP_tup lexps -> begin let typ = Env.expand_synonyms env typ in @@ -2766,99 +2779,85 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length" in annot_lexp (LEXP_tup tlexps) typ, env - (* This case is pretty much just for the PSTATE. := vector pattern which is really common in ASL. *) - (* Maybe this code can be made not horrible? *) - | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 -> - begin - match destruct_vector env typ with - | Some (vec_len, _, _) -> - let bind_bits_tuple lexp (tlexps, env, llen) = - match lexp with - | LEXP_aux (LEXP_id v, _) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Unbound -> - typ_error l "Unbound variable in vector tuple assignment" - | Local (Mutable, vtyp) | Register vtyp -> - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - end - | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) -> - (* FIXME: will only work for ASL *) - let rec_id = - match Env.lookup_id v env with - | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id - | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") - in - let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - | _ -> typ_error l "bit vector assignment must only contain identifiers" - in - let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in - if prove env (nc_eq vec_len lexp_len) - then annot_lexp (LEXP_tup tlexps) typ, env - else typ_error l "Vector and tuple length must be the same in assignment" - | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ) + | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ) + end + | _ -> + let inferred_lexp = infer_lexp env lexp in + subtyp l env typ (lexp_typ_of inferred_lexp); + inferred_lexp, env + +and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = + let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in + let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in + match lexp_aux with + | LEXP_id v -> + begin match Env.lookup_id v env with + | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ + (* Probably need to remove flows here *) + | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]) + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Unbound -> + typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp) + end + | LEXP_vector_range (v_lexp, exp1, exp2) -> + begin + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp1 = infer_exp env exp1 in + let inferred_exp2 = infer_exp env exp2 in + let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in + let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in + begin match ord with + | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp) end - | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ) + | _ -> typ_error l "Cannot assign slice of non vector type" end - | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) -> + | LEXP_vector (v_lexp, exp) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in - let inferred_exp1, inferred_exp2 = match access with - | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2 - | _ -> assert false - in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp = infer_exp env exp in + let nexp, env = bind_numeric l (typ_of inferred_exp) env in + if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then + annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ + else + typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp) + | _ -> typ_error l "Cannot assign vector element of non vector type" end - (* Not sure about this case... can the left lexp be anything other than an identifier? *) - | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) -> + | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression" + | LEXP_vector_concat (v_lexp :: v_lexps) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in - let inferred_exp = match access with - | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp - | _ -> assert false + let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) = + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord -> + typ_equality l env elem_typ first_elem_typ; + nsum acc len + | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order" in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let inferred_v_lexps = List.map (infer_lexp env) v_lexps in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in + annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ) + | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ) end | LEXP_field (LEXP_aux (LEXP_id v, _), fid) -> (* FIXME: will only work for ASL *) @@ -2868,7 +2867,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in - annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env + annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]) | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp) and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = @@ -2951,7 +2950,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_app (f, xs) -> infer_funapp l env f xs None | E_loop (loop_type, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in - let checked_body = crule check_exp env body unit_typ in + let flows, constrs = infer_flow env checked_cond in + let checked_body = crule check_exp (add_flows true flows env) body unit_typ in annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin @@ -3485,6 +3485,9 @@ and propagate_lexp_effect_aux = function let p_exp2 = propagate_exp_effect exp2 in LEXP_vector_range (p_lexp, p_exp1, p_exp2), union_effects (collect_effects [p_exp1; p_exp2]) (effect_of_lexp p_lexp) + | LEXP_vector_concat lexps -> + let p_lexps = List.map propagate_lexp_effect lexps in + LEXP_vector_concat p_lexps, collect_effects_lexp p_lexps | LEXP_field (lexp, id) -> let p_lexp = propagate_lexp_effect lexp in LEXP_field (p_lexp, id),effect_of_lexp p_lexp diff --git a/src/type_check.mli b/src/type_check.mli index bb52f2aa..ed240839 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -63,6 +63,10 @@ val opt_tc_debug : int ref re-writer passes, so it should only be used for debugging. *) val opt_no_effects : bool ref +(** [opt_no_lexp_bounds_check] turns of the bounds checking in vector + assignments in l-expressions. *) +val opt_no_lexp_bounds_check : bool ref + (** {2 Type errors} *) type type_error = @@ -148,8 +152,9 @@ module Env : sig (** Lookup id searchs for a specified id in the environment, and returns it's type and what kind of identifier it is, using the lvar type. Returns Unbound if the identifier is unbound, and - won't throw any exceptions. *) - val lookup_id : id -> t -> lvar + won't throw any exceptions. If the raw option is true, then look + up the type without any flow typing modifiers. *) + val lookup_id : ?raw:bool -> id -> t -> lvar val is_union_constructor : id -> t -> bool diff --git a/src/value.ml b/src/value.ml index 4b4f0865..e9a98160 100644 --- a/src/value.ml +++ b/src/value.ml @@ -183,6 +183,10 @@ let value_eq_string = function | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) | _ -> failwith "value eq_string" +let value_eq_bit = function + | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2)) + | _ -> failwith "value eq_bit" + let value_length = function | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int) | _ -> failwith "value length" @@ -417,6 +421,7 @@ let primops = ("eq_list", value_eq_list); ("eq_bool", value_eq_bool); ("eq_string", value_eq_string); + ("eq_bit", value_eq_bit); ("eq_anything", value_eq_anything); ("length", value_length); ("subrange", value_subrange); diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh index d4e01079..15a45e7c 100755 --- a/test/arm/run_tests.sh +++ b/test/arm/run_tests.sh @@ -51,7 +51,7 @@ cd $SAILDIR/aarch64 printf "Compiling specification...\n" -if $SAILDIR/sail -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; +if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; then green "compiled no_vector specification" "ok"; mv aarch64_test $DIR/; @@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n" cd $SAILDIR/aarch64 -if $SAILDIR/sail -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; +if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null; then green "loaded no_vector specification" "ok"; diff --git a/test/ocaml/bitfield/bitfield.sail b/test/ocaml/bitfield/bitfield.sail index 2a53ab3c..342b3d08 100644 --- a/test/ocaml/bitfield/bitfield.sail +++ b/test/ocaml/bitfield/bitfield.sail @@ -11,13 +11,6 @@ bitfield cr : bits(8) = { register CR : cr -bitfield dr : vector(4, inc, bit) = { - DR0 : 2 .. 3, - LT : 2 -} - -register DR : dr - val main : unit -> unit effect {rreg, wreg} function main () = { diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail index fab04306..74d2b8e5 100644 --- a/test/ocaml/lsl/lsl.sail +++ b/test/ocaml/lsl/lsl.sail @@ -1,6 +1,3 @@ -val zeros : forall ('n : Int), 'n >= 0. atom('n) -> bits('n) - -function zeros n = replicate_bits(0b0, 'n) val lslc : forall ('n : Int) ('shift : Int), 'n >= 1. (bits('n), atom('shift)) -> (bits('n), bit) effect {escape} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 83178aea..6a8c703f 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -1,18 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) - -infix 4 == - -val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool - -val eq_int = "eq_int" : (int, int) -> bool - -val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool +$include val eq_string = "eq_string" : (string, string) -> bool @@ -25,282 +13,8 @@ val eq_anything = { val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) -overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} - -val vector_subrange_dec = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val vector_subrange_inc = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. - (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) - -/* -val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int). - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) -*/ - -overload vector_subrange = {vector_subrange_dec, vector_subrange_inc} - -val vector_access_dec = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. - (vector('n, dec, 'a), atom('m)) -> 'a - -/* -val vector_access_B = "access" : forall ('n : Int) ('a : Type). - (vector('n, dec, 'a), int) -> 'a -*/ - -overload vector_access = {vector_access_dec} - -val vector_update = "update" : forall 'n ('a : Type). - (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) - -val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) - -val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o. - (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) - -overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} - -val vcons : forall ('n : Int) ('a : Type). - ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) - -val append = "append" : forall ('n : Int) ('m : Int) ('a : Type). - (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) - -val not_bool = "not" : bool -> bool - -val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) +overload operator == = {eq_string, eq_real, eq_anything} overload ~ = {not_bool, not_vec} -val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool - -function neq_atom (x, y) = not_bool(eq_atom(x, y)) - -val neq_int : (int, int) -> bool - -function neq_int (x, y) = not_bool(eq_int(x, y)) - -val neq_vec : forall 'n. (bits('n), bits('n)) -> bool - -function neq_vec (x, y) = not_bool(eq_vec(x, y)) - -val neq_anything : forall ('a : Type). ('a, 'a) -> bool - -function neq_anything (x, y) = not_bool(x == y) - -overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} - -val and_bool = "and_bool" : (bool, bool) -> bool - -val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -function and_vec (xs, ys) = builtin_and_vec(xs, ys) - -overload operator & = {and_bool, and_vec} - -val or_bool = "or_bool" : (bool, bool) -> bool - -val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -function or_vec (xs, ys) = builtin_or_vec(xs, ys) - -overload operator | = {or_bool, or_vec} - -val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) - -val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) - -val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) - -val __SetSlice_bits = "set_slice" : forall 'n 'm. - (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) - -val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) - -val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) - -function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) - -val __raw_SetSlice_bits : forall 'n 'w. - (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) - -val __raw_GetSlice_bits : forall 'n 'w. - (atom('n), atom('w), bits('n), int) -> bits('w) - -val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m) - -val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) - -val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) - -val cast cast_unit_vec : bit -> bits(1) - -function cast_unit_vec bitone = 0b1 -and cast_unit_vec bitzero = 0b0 - val print = "print_endline" : string -> unit - -val putchar = "putchar" : forall ('a : Type). 'a -> unit - -val concat_str = "concat_str" : (string, string) -> string - -val DecStr : int -> string - -val HexStr : int -> string - -val BitStr = "string_of_bits" : forall 'n. bits('n) -> string - -val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val int_power : (int, int) -> int - -val real_power = "real_power" : (real, int) -> real - -overload operator ^ = {xor_vec, int_power, real_power} - -val add_range = "add_int" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val add_int = "add_int" : (int, int) -> int - -val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) - -val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) - -val add_real = "add_real" : (real, real) -> real - -overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} - -val sub_range = "sub_int" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val sub_int = "sub_int" : (int, int) -> int - -val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n) - -val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) - -val sub_real = "sub_real" : (real, real) -> real - -val negate_range = "negate" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) - -val negate_int = "negate" : int -> int - -val negate_real = "negate_real" : real -> real - -overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} - -overload negate = {negate_range, negate_int, negate_real} - -val mult_range = "mult" : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) - -val mult_int = "mult" : (int, int) -> int - -val mult_real = "mult_real" : (real, real) -> real - -overload operator * = {mult_range, mult_int, mult_real} - -val Sqrt = "sqrt_real" : real -> real - -val gteq_int = "gteq" : (int, int) -> bool - -val gteq_real = "gteq_real" : (real, real) -> bool - -overload operator >= = {gteq_atom, gteq_int, gteq_real} - -val lteq_int = "lteq" : (int, int) -> bool - -val lteq_real = "lteq_real" : (real, real) -> bool - -overload operator <= = {lteq_atom, lteq_int, lteq_real} - -val gt_int = "gt" : (int, int) -> bool - -val gt_real = "gt_real" : (real, real) -> bool - -overload operator > = {gt_atom, gt_int, gt_real} - -val lt_int = "lt" : (int, int) -> bool - -val lt_real = "lt_real" : (real, real) -> bool - -overload operator < = {lt_atom, lt_int, lt_real} - -val RoundDown = "round_down" : real -> int - -val RoundUp = "round_up" : real -> int - -val abs = "abs_num" : real -> real - -val quotient_nat = "quotient" : (nat, nat) -> nat - -val quotient_real = "quotient_real" : (real, real) -> real - -val quotient = "quotient" : (int, int) -> int - -infixl 7 / - -overload operator / = {quotient_nat, quotient, quotient_real} - -val modulus = "modulus" : (int, int) -> int - -infixl 7 % - -overload operator % = {modulus} - -val Real = "to_real" : int -> real - -val shl_int = "shl_int" : (int, int) -> int - -val shr_int = "shr_int" : (int, int) -> int - -val min_nat = "min_int" : (nat, nat) -> nat - -val min_int = "min_int" : (int, int) -> int - -val max_nat = "max_int" : (nat, nat) -> nat - -val max_int = "max_int" : (int, int) -> int - -overload min = {min_nat, min_int} - -overload max = {max_nat, max_int} - -val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) - -val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} - -function ex_nat 'n = n - -val cast ex_int : int -> {'n, true. atom('n)} - -function ex_int 'n = n - -val ex_range : forall 'n 'm. - range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)} - -val coerce_int_nat : int -> nat effect {escape} - -function coerce_int_nat 'x = { - assert(constraint('x >= 0)); - x -} - -val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. - (bits('m), int, atom('n)) -> bits('n) - -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) - -val "print_int" : (string, int) -> unit - -val "print_bits" : forall 'n. (string, bits('n)) -> unit \ No newline at end of file diff --git a/test/ocaml/string_of_struct/sos.sail b/test/ocaml/string_of_struct/sos.sail index 69a17e6c..ecef0e36 100644 --- a/test/ocaml/string_of_struct/sos.sail +++ b/test/ocaml/string_of_struct/sos.sail @@ -2,11 +2,6 @@ struct would cause the ocaml backend to generate a bad string_of function for the struct */ -union option ('a : Type) = { - None : unit, - Some : 'a -} - struct test = { test1 : int, test2 : option(int) diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail index d13b527c..6790140e 100644 --- a/test/ocaml/types/types.sail +++ b/test/ocaml/types/types.sail @@ -24,8 +24,6 @@ struct TestStruct = { register SREG : TestStruct -union option ('a : Type) = {None : unit, Some : 'a} - register OREG : option(byte) val main : unit -> unit effect {rreg, wreg} diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail index 5afd421d..ac44d9ae 100644 --- a/test/ocaml/vec_32_64/vec_32_64.sail +++ b/test/ocaml/vec_32_64/vec_32_64.sail @@ -8,11 +8,6 @@ function get_size () = 32 val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit -val zeros : forall 'n. atom('n) -> vector('n, dec, bit) - -function zeros n = - if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1) - val main : unit -> unit function main () = { diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index 6763922a..dc625084 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -10,6 +10,6 @@ function test nzcv = { Z = 0b0; C = 0b0; V = 0b0; - (N, Z, C, V) = nzcv; + (N @ Z @ C @ V) = nzcv; () } diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail index c148e6da..84b4f7b4 100644 --- a/test/typecheck/pass/while_PM.sail +++ b/test/typecheck/pass/while_PM.sail @@ -22,10 +22,12 @@ val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n. register GPR00 : vector(64, dec, bit) +/* FIXME: Currently this doesn't work in lem function test b : bit -> unit = { - i : int = 0; + i : range(0, 64) = 0; while i < 64 do { GPR00[i] = b; - i = i + 1 + i = i + 1; } } +*/ \ No newline at end of file -- cgit v1.2.3