summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/no_vector/spec.sail343
-rw-r--r--aarch64/prelude.sail38
-rw-r--r--editors/sail2-mode.el1
-rw-r--r--language/sail.ott1
-rw-r--r--lib/smt.sail4
-rw-r--r--src/ast_util.ml11
-rw-r--r--src/initial_check.ml60
-rw-r--r--src/interpreter.ml4
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/pretty_print_sail.ml1
-rw-r--r--src/rewriter.ml11
-rw-r--r--src/rewriter.mli3
-rw-r--r--src/rewrites.ml32
-rw-r--r--src/sail.ml3
-rw-r--r--src/type_check.ml267
-rw-r--r--src/type_check.mli9
-rw-r--r--src/value.ml5
-rwxr-xr-xtest/arm/run_tests.sh4
-rw-r--r--test/ocaml/bitfield/bitfield.sail7
-rw-r--r--test/ocaml/lsl/lsl.sail3
-rw-r--r--test/ocaml/prelude.sail290
-rw-r--r--test/ocaml/string_of_struct/sos.sail5
-rw-r--r--test/ocaml/types/types.sail2
-rw-r--r--test/ocaml/vec_32_64/vec_32_64.sail5
-rw-r--r--test/typecheck/pass/nzcv.sail2
-rw-r--r--test/typecheck/pass/while_PM.sail6
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 <smt.sail>
-$include <flow.sail>
+$include <arith.sail>
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.<N,Z,C,V> := 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 <prelude.sail>
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 10:42:13 +0000