summaryrefslogtreecommitdiff
path: root/aarch64_small
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small')
-rw-r--r--aarch64_small/armV8.h.sail2
-rw-r--r--aarch64_small/armV8.sail182
-rw-r--r--aarch64_small/armV8_A64_lib.sail22
-rw-r--r--aarch64_small/armV8_common_lib.sail38
-rw-r--r--aarch64_small/armV8_lib.h.sail8
-rw-r--r--aarch64_small/prelude.sail18
6 files changed, 135 insertions, 135 deletions
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index ab69f323..d0278d9d 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -218,7 +218,7 @@ let _V : vector(32,dec,(register(bits(128)))) =
/* lsl: used instead of the ARM ARM << over integers */
-val lsl : forall 'm 'n, 'm >= 0 & 'n >= 0. (atom('n), atom('m)) -> atom('n * (2 ^ 'm))
+val lsl : forall 'm 'n, 'm >= 0 & 'n >= 0. (int('n), int('m)) -> int('n * (2 ^ 'm))
function lsl (n, m) = n * (2 ^ m)
/* not_implemented is used to indicate something WE did not implement */
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index b43d9341..8e893e4b 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -67,33 +67,33 @@ union ast = {
BranchRegister : (reg_index,BranchType),
ExceptionReturn : unit, /* TODO: add to .hgen */
DebugRestorePState : unit, /* TODO: add to .hgen */
- LoadLiteral : {'D 'size, RegisterSize('D) & 'size in {1,2,4,8/* ,16 */} & 'size * 8 == 'D. (reg_index,MemOp,boolean,atom('size),bits(64),atom('D))},
- LoadStoreAcqExc : {'D 'R 'elsize, 'D in {8, 16, 32, 64, 128} & RegisterSize('R) & 'elsize <= 'D. (reg_index,reg_index,reg_index,reg_index,AccType,boolean,boolean,MemOp,atom('elsize),atom('R),atom('D))},
- LoadStorePairNonTemp : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,uinteger,atom('D),bits(64))},
- LoadImmediate : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,bits(64),atom('R),atom('D))},
- LoadRegister : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,ExtendType,range(0,3),atom('R),atom('D))},
- LoadStorePair : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,boolean,atom('D),bits(64))},
- AddSubImmediate : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,boolean,bits('R))},
- BitfieldMove : {'R 'r 's, RegisterSize('R) & 0 <= 'r < 'R & 0 <= 's < 'R. (reg_index,reg_index,atom('R),boolean,boolean,atom('r),atom('s),bits('R),bits('R))},
- ExtractRegister : {'R 'lsb, RegisterSize('R) & 0 <= 'lsb <= 'R. (reg_index,reg_index,reg_index,atom('R),atom('lsb))},
- LogicalImmediate : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,LogicalOp,bits('R))},
- MoveWide : {'R 'pos, RegisterSize('R) & 0 <= 'pos < div('R, 2). (reg_index,atom('R),bits(16),atom('pos),MoveWideOp)},
+ LoadLiteral : {'D 'size, RegisterSize('D) & 'size in {1,2,4,8/* ,16 */} & 'size * 8 == 'D. (reg_index,MemOp,boolean,int('size),bits(64),int('D))},
+ LoadStoreAcqExc : {'D 'R 'elsize, 'D in {8, 16, 32, 64, 128} & RegisterSize('R) & 'elsize <= 'D. (reg_index,reg_index,reg_index,reg_index,AccType,boolean,boolean,MemOp,int('elsize),int('R),int('D))},
+ LoadStorePairNonTemp : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,uinteger,int('D),bits(64))},
+ LoadImmediate : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,bits(64),int('R),int('D))},
+ LoadRegister : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,ExtendType,range(0,3),int('R),int('D))},
+ LoadStorePair : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,boolean,int('D),bits(64))},
+ AddSubImmediate : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,boolean,bits('R))},
+ BitfieldMove : {'R 'r 's, RegisterSize('R) & 0 <= 'r < 'R & 0 <= 's < 'R. (reg_index,reg_index,int('R),boolean,boolean,int('r),int('s),bits('R),bits('R))},
+ ExtractRegister : {'R 'lsb, RegisterSize('R) & 0 <= 'lsb <= 'R. (reg_index,reg_index,reg_index,int('R),int('lsb))},
+ LogicalImmediate : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,LogicalOp,bits('R))},
+ MoveWide : {'R 'pos, RegisterSize('R) & 0 <= 'pos < div('R, 2). (reg_index,int('R),bits(16),int('pos),MoveWideOp)},
Address : (reg_index,boolean,bits(64)),
- AddSubExtendRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ExtendType,range(0,7))},
- AddSubShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ShiftType,range(0,63))},
- AddSubCarry : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean)},
- ConditionalCompareImmediate : {'R, RegisterSize('R). (reg_index,atom('R),boolean,bits(4),bits(4),bits('R))},
- ConditionalCompareRegister : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,bits(4),bits(4))},
- ConditionalSelect : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),bits(4),boolean,boolean)},
- Reverse : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),RevOp)},
- CountLeading : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),CountOp)},
- Division : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean)},
- Shift : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),ShiftType)},
- CRC : {'D, DataSize('D). (reg_index,reg_index,reg_index,atom('D),boolean)},
- MultiplyAddSub : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
- MultiplyAddSubLong : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('D),boolean,boolean)},
- MultiplyHigh : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
- LogicalShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
+ AddSubExtendRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean,ExtendType,range(0,7))},
+ AddSubShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean,ShiftType,range(0,63))},
+ AddSubCarry : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean)},
+ ConditionalCompareImmediate : {'R, RegisterSize('R). (reg_index,int('R),boolean,bits(4),bits(4),bits('R))},
+ ConditionalCompareRegister : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,bits(4),bits(4))},
+ ConditionalSelect : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),bits(4),boolean,boolean)},
+ Reverse : {'R, RegisterSize('R). (reg_index,reg_index,int('R),RevOp)},
+ CountLeading : {'R, RegisterSize('R). (reg_index,reg_index,int('R),CountOp)},
+ Division : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean)},
+ Shift : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),ShiftType)},
+ CRC : {'D, DataSize('D). (reg_index,reg_index,reg_index,int('D),boolean)},
+ MultiplyAddSub : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('R),boolean)},
+ MultiplyAddSubLong : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('D),boolean,boolean)},
+ MultiplyHigh : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('R),boolean)},
+ LogicalShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
}
val execute : ast -> unit effect {rreg,wreg,rmem,barr,eamem,wmv,exmem,escape}
@@ -186,7 +186,7 @@ function decodeCompareBranchImmediate ([sf]@0b011010@[op]@(imm19:bits(19))@(Rt:b
Some(CompareAndBranch(t,datasize,iszero,offset));
}
-function clause execute (CompareAndBranch((t,(datasize as atom('R)),iszero,offset))) = {
+function clause execute (CompareAndBranch((t,(datasize as int('R)),iszero,offset))) = {
operand1 : bits('R) = rX(datasize,t);
if IsZero(operand1) == iszero then
BranchTo(rPC() + offset, BranchType_JMP);
@@ -554,7 +554,7 @@ val decodeTestBranchImmediate : bits(32) -> option(ast) effect {escape}
function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 : bits(14))@(Rt:bits(5))) = {
t : reg_index = UInt_reg(Rt);
- let datasize : {| 32, 64 |} /* as atom('R) */ = if b5 == b1 then 64 else 32;
+ let datasize : {| 32, 64 |} /* as int('R) */ = if b5 == b1 then 64 else 32;
let bit_pos : uinteger = UInt([b5]@b40);
bit_val : bit = op;
offset : bits(64) = SignExtend(imm14@0b00);
@@ -696,12 +696,12 @@ function decodeLoadRegisterLiteral ((opc : bits(2))@0b011@0b0@0b00@(imm19 : bits
/* CP: adding let bindings so typechecker has more information */
let size = size;
- let datasize /* as atom('D) */ = size*8; /* not in ARM ARM */
+ let datasize /* as int('D) */ = size*8; /* not in ARM ARM */
Some(LoadLiteral(t,memop,_signed,size,offset,datasize));
}
-function clause execute ( LoadLiteral((t,memop,_signed,size,offset,(datasize as atom('D)) )) ) = {
+function clause execute ( LoadLiteral((t,memop,_signed,size,offset,(datasize as int('D)) )) ) = {
address : bits(64) = rPC() + offset;
let data = Zeros(datasize); /* ARM: uninitialized */
match memop {
@@ -759,13 +759,13 @@ function decodeLoadStoreExclusive ((size : bits(2))@0b001000@[o2]@[L]@[o1]@(Rs:b
let excl : boolean = (o2 == b0);
let pair : boolean = (o1 == b1);
let memop : MemOp = if L == b1 then MemOp_LOAD else MemOp_STORE;
- let size_uint as atom('size) = UInt(size);
- let elsize : atom(8 * (2 ^ 'size)) = lsl(8, size_uint);
- let elsize as atom('elsize) = elsize;
+ let size_uint as int('size) = UInt(size);
+ let elsize : int(8 * (2 ^ 'size)) = lsl(8, size_uint);
+ let elsize as int('elsize) = elsize;
assert(elsize == 8 | elsize == 16 | elsize == 32 | elsize == 64); /*FIXME: CP: adding assertion to make typecheck*/
- let regsize as atom('R) = if elsize == 64 then 64 else 32;
- let datasize : {'n, 'n in {8,16,32,64,128} & 'elsize <= 'n. atom('n)} = if pair then elsize * 2 else elsize;
+ let regsize as int('R) = if elsize == 64 then 64 else 32;
+ let datasize : {'n, 'n in {8,16,32,64,128} & 'elsize <= 'n. int('n)} = if pair then elsize * 2 else elsize;
/* lemma: pair --> datasize = 2*regsize */
/* follows from "if o1 == 1 & size[1] == 0 then UnallocatedEncoding();" */
@@ -773,10 +773,10 @@ function decodeLoadStoreExclusive ((size : bits(2))@0b001000@[o2]@[L]@[o1]@(Rs:b
Some(LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize)));
}
-function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,(regsize as atom('R)),(datasize as atom('D)) ))) = {
+function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,(regsize as int('R)),(datasize as int('D)) ))) = {
address : bits(64) = Zeros(); /* ARM: uninitialized */
data : bits('D) = Zeros(datasize); /* ARM: uninitialized */
- /*constant*/ dbytes : atom(div('D,8)) = quot (datasize,8);
+ /*constant*/ dbytes : int(div('D,8)) = quot (datasize,8);
rt_unknown : boolean = false;
rn_unknown : boolean = false;
@@ -847,7 +847,7 @@ function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsi
data = UNKNOWN_BITS(datasize) /* : bits('D) */
}
else if pair then {
- let halfsize : atom(div('D,2)) = quot(datasize,2);
+ let halfsize : int(div('D,2)) = quot(datasize,2);
assert( excl ); /* FIXME: CP adding assertion: in the 'pair' case datasize > 8 */
assert(datasize > 8);
el1 /* : bits('R) */ = rX(halfsize/* regsize */,t); /* ARM: bits(datasize / 2) see lemma in the decoding */
@@ -960,18 +960,18 @@ function decodeLoadStoreNoAllocatePairOffset ((opc : bits(2))@0b101@0b0@0b000@[L
memop : MemOp = if L == b1 then MemOp_LOAD else MemOp_STORE;
if opc[0] == b1 then UnallocatedEncoding();
let scale : {| 2, 3 |} = 2 + UInt([opc[1]]);
- let datasize /* : {| 32,64 |} */ /* as atom('D) */ = lsl(8, scale);
+ let datasize /* : {| 32,64 |} */ /* as int('D) */ = lsl(8, scale);
assert(datasize == 32 | datasize == 64); /*FIXME: CP adding assertion to make typecheck*/
offset : bits(64) = LSL(SignExtend(imm7), scale);
Some(LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset));
}
-function clause execute ( LoadStorePairNonTemp((wback,postindex,n,t,t2,acctype,memop,scale,(datasize as atom('D)),offset)) ) = {
+function clause execute ( LoadStorePairNonTemp((wback,postindex,n,t,t2,acctype,memop,scale,(datasize as int('D)),offset)) ) = {
address : bits(64) = Zeros(); /* ARM: uninitialized */
data1 : bits('D) = Zeros(); /* ARM: uninitialized */
data2 : bits('D) = Zeros(); /* ARM: uninitialized */
- /*constant*/ dbytes : atom(div('D,8)) = quot(datasize,8);
+ /*constant*/ dbytes : int(div('D,8)) = quot(datasize,8);
rt_unknown : boolean = false;
if memop == MemOp_LOAD & t == t2 then {
@@ -1064,7 +1064,7 @@ function sharedDecodeLoadImmediate (opc : bits(2),size : bits(2), Rn : bits(5),
acctype : AccType = AccType_NORMAL/AccType_UNPRIV; */
memop : MemOp = MemOp_LOAD; /* ARM: uninitialized */
_signed : boolean = false; /* ARM: uninitialized */
- regsize : { 'R, RegisterSize('R). atom('R) } = 64; /* ARM: uninitialized */
+ regsize : { 'R, RegisterSize('R). int('R) } = 64; /* ARM: uninitialized */
if opc[1] == b0 then {
/* store or zero-extending load */
@@ -1090,7 +1090,7 @@ function sharedDecodeLoadImmediate (opc : bits(2),size : bits(2), Rn : bits(5),
};
};
- let datasize /* : { 'D, DataSize('D). atom('D) } */ = lsl(8, scale);
+ let datasize /* : { 'D, DataSize('D). int('D) } */ = lsl(8, scale);
assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
Some(LoadImmediate(n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize));
@@ -1112,7 +1112,7 @@ function decodeLoadStoreRegisterImmediatePostIndexed ((size:bits(2))@0b111@0b0@0
(opc,size,Rn,Rt,wback,postindex,scale,offset,AccType_NORMAL,false);
}
-function clause execute ( LoadImmediate ((n,t,acctype,memop,_signed,wback,postindex,offset,regsize as atom('R),datasize as atom('D))) ) = {
+function clause execute ( LoadImmediate ((n,t,acctype,memop,_signed,wback,postindex,offset,regsize as int('R),datasize as int('D))) ) = {
address : bits(64) = Zeros(); /* ARM: uninitialized */
data : bits('D) = Zeros(); /* ARM: uninitialized */
wb_unknown : boolean = false;
@@ -1233,7 +1233,7 @@ function sharedDecodeLoadRegister(Rn:bits(5), Rt:bits(5), Rm:bits(5), opc : bits
acctype : AccType = AccType_NORMAL;
memop : MemOp = MemOp_LOAD; /* ARM: uninitialized */
_signed : boolean = b0; /* ARM: uninitialized */
- regsize : { 'R, RegisterSize('R). atom('R) }/* atom('R) */ = 64; /* ARM: uninitialized */
+ regsize : { 'R, RegisterSize('R). int('R) }/* int('R) */ = 64; /* ARM: uninitialized */
if opc[1] == b0 then {
/* store or zero-extending load */
@@ -1253,7 +1253,7 @@ function sharedDecodeLoadRegister(Rn:bits(5), Rt:bits(5), Rm:bits(5), opc : bits
};
};
- let datasize /* : {'D, DataSize('D). atom('D)} */ /* : atom('D) */ = lsl(8, scale);
+ let datasize /* : {'D, DataSize('D). int('D)} */ /* : int('D) */ = lsl(8, scale);
assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
Some (LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize));
}
@@ -1278,7 +1278,7 @@ function decodeLoadStoreRegisterRegisterOffset ((size:bits(2))@0b111@0b0@0b00@(o
sharedDecodeLoadRegister(Rn,Rt,Rm,opc,size,wback,postindex,scale,extend_type,shift);
}
-function clause execute ( LoadRegister((n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize as atom('R),datasize as atom('D))) ) = {
+function clause execute ( LoadRegister((n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize as int('R),datasize as int('D))) ) = {
offset : bits(64) = ExtendReg(m, extend_type, shift);
address : bits(64) = Zeros(); /* ARM: uninitialized */
data : bits('D) = Zeros(); /* ARM: uninitialized */
@@ -1437,7 +1437,7 @@ function sharedDecodeLoadStorePair (L:boolean,opc : bits(2),imm7:bits(7),Rn:bits
if [L,opc[0]] == 0b01 | opc == 0b11 then UnallocatedEncoding();
_signed : (boolean) = (opc[0] != b0);
scale : range(2,3) = 2 + UInt([opc[1]]);
- let datasize /* : { 'D, DataSize('D). atom('D) } */ = lsl(8, scale);
+ let datasize /* : { 'D, DataSize('D). int('D) } */ = lsl(8, scale);
assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
offset : (bits(64)) = LSL(SignExtend(imm7), scale);
@@ -1455,11 +1455,11 @@ function decodeLoadStoreRegisterPairOffset (opc:bits(2)@0b101@0b0@0b010@[L]@(imm
sharedDecodeLoadStorePair(L,opc,imm7,Rn,Rt,Rt2,wback,postindex);
}
-function clause execute ( LoadStorePair((wback,postindex,n,t,t2,acctype,memop,_signed,datasize as atom('D),offset)) ) = {
+function clause execute ( LoadStorePair((wback,postindex,n,t,t2,acctype,memop,_signed,datasize as int('D),offset)) ) = {
address : bits(64) = Zeros(); /* ARM: uninitialized */
data1 : (bits('D)) = Zeros(); /* ARM: uninitialized */
data2 : (bits('D)) = Zeros(); /* ARM: uninitialized */
- /*constant*/ let dbytes : {'db, 'db == div('D,8) & 'db in {1,2,4,8}. atom('db) } = quot (datasize,8);
+ /*constant*/ let dbytes : {'db, 'db == div('D,8) & 'db in {1,2,4,8}. int('db) } = quot (datasize,8);
rt_unknown : (boolean) = false;
wb_unknown : (boolean) = false;
@@ -1615,7 +1615,7 @@ function decodeAddSubtractImmediate ([sf]@[op]@[S]@0b10001@(shift:bits(2))@(imm1
Some(AddSubImmediate((d,n,datasize,sub_op,setflags,imm)));
}
-function clause execute (AddSubImmediate((d,n,datasize as atom('R),sub_op,setflags,imm))) = {
+function clause execute (AddSubImmediate((d,n,datasize as int('R),sub_op,setflags,imm))) = {
operand1 : (bits('R)) = if n == 31 then rSP() else rX(n);
operand2 : (bits('R)) = imm;
carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1647,7 +1647,7 @@ function decodeBitfield ([sf]@(opc:bits(2))@0b100110@[N]@(immr : bits(6))@(imms
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
let datasize : {|32,64|} = if sf == b1 then 64 else 32;
- /* let datasize as atom('R) = datasize; */
+ /* let datasize as int('R) = datasize; */
inzero : (boolean) = false; /* ARM: uninitialized */
extend : (boolean) = false; /* ARM: uninitialized */
@@ -1675,7 +1675,7 @@ function decodeBitfield ([sf]@(opc:bits(2))@0b100110@[N]@(immr : bits(6))@(imms
}}
-function clause execute (BitfieldMove((d,n,(datasize as atom('R)),inzero,extend,R,S,wmask,tmask))) = {
+function clause execute (BitfieldMove((d,n,(datasize as int('R)),inzero,extend,R,S,wmask,tmask))) = {
dst : bits('R) = if inzero then Zeros() else rX(d);
src : bits('R) = rX(n);
@@ -1707,7 +1707,7 @@ function decodeExtract ([sf]@0b00@0b100111@[N]@0b0@(Rm:bits(5))@(imms : bits(6))
Some(ExtractRegister((d,n,m,datasize,lsb)));
}
-function clause execute ( ExtractRegister((d,n,m,datasize as atom('R),lsb)) ) = {
+function clause execute ( ExtractRegister((d,n,m,datasize as int('R),lsb)) ) = {
result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
@@ -1724,7 +1724,7 @@ val decodeLogicalImmediate : bits(32) -> option(ast) effect {escape}
function decodeLogicalImmediate ([sf]@(opc:bits(2))@0b100100@[N]@(immr : bits(6))@(imms : bits(6))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
- let datasize : {|32,64|} /* atom('R) */ = if sf == b1 then 64 else 32;
+ let datasize : {|32,64|} /* int('R) */ = if sf == b1 then 64 else 32;
setflags : (boolean) = false; /* ARM: uninitialized */
op : (LogicalOp) = LogicalOp_AND; /* ARM: uninitialized */
match opc {
@@ -1740,7 +1740,7 @@ function decodeLogicalImmediate ([sf]@(opc:bits(2))@0b100100@[N]@(immr : bits(6)
Some(LogicalImmediate((d,n,datasize,setflags,op,imm)));
}}
-function clause execute (LogicalImmediate((d,n,datasize as atom('R),setflags,op,imm))) = {
+function clause execute (LogicalImmediate((d,n,datasize as int('R),setflags,op,imm))) = {
result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = imm;
@@ -1766,7 +1766,7 @@ function clause execute (LogicalImmediate((d,n,datasize as atom('R),setflags,op,
val decodeMoveWideImmediate : bits(32) -> option(ast) effect {escape}
function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(imm16 : bits(16))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
- let datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ let datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
imm : (bits(16)) = imm16;
pos : (uinteger) = 0; /* ARM: uninitialized */
opcode : (MoveWideOp) = MoveWideOp_N; /* ARM: uninitialized */
@@ -1785,7 +1785,7 @@ function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(im
Some(MoveWide(d,datasize,imm,pos,opcode));
}
-function clause execute ( MoveWide((d,datasize as atom('R),imm,pos,opcode)) ) = {
+function clause execute ( MoveWide((d,datasize as int('R),imm,pos,opcode)) ) = {
result : (bits('R)) = Zeros(); /* ARM: uninitialized */
if opcode == MoveWideOp_K then
@@ -1831,7 +1831,7 @@ function decodeAddSubtractExtendedRegister ([sf]@[op]@[S]@0b01011@0b00@0b1@(Rm:b
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
sub_op : (boolean) = (op == b1);
setflags : (boolean) = (S == b1);
extend_type : (ExtendType) = DecodeRegExtend(option_v);
@@ -1841,7 +1841,7 @@ function decodeAddSubtractExtendedRegister ([sf]@[op]@[S]@0b01011@0b00@0b1@(Rm:b
Some(AddSubExtendRegister(d,n,m,datasize,sub_op,setflags,extend_type,shift));
}
-function clause execute (AddSubExtendRegister((d,n,m,datasize as atom('R),sub_op,setflags,extend_type,shift))) = {
+function clause execute (AddSubExtendRegister((d,n,m,datasize as int('R),sub_op,setflags,extend_type,shift))) = {
operand1 : (bits('R)) = if n == 31 then rSP() else rX(n);
operand2 : (bits('R)) = ExtendReg(m, extend_type, shift);
carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1871,7 +1871,7 @@ function decodeAddSubtractShiftedRegister ([sf]@[op]@[S]@0b01011@(shift:bits(2))
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {| 32,64 |} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32,64 |} /* : int('R) */ = if sf == b1 then 64 else 32;
sub_op : (boolean) = (op == b1);
setflags : (boolean) = (S == b1);
@@ -1884,7 +1884,7 @@ function decodeAddSubtractShiftedRegister ([sf]@[op]@[S]@0b01011@(shift:bits(2))
Some(AddSubShiftedRegister(d,n,m,datasize,sub_op,setflags,shift_type,shift_amount));
}
-function clause execute (AddSubShiftedRegister((d,n,m,(datasize as atom('R)),sub_op,setflags,shift_type,shift_amount))) = {
+function clause execute (AddSubShiftedRegister((d,n,m,(datasize as int('R)),sub_op,setflags,shift_type,shift_amount))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = ShiftReg(m, shift_type, shift_amount);
carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1914,14 +1914,14 @@ function decodeAddSubtractWithCarry ([sf]@[op]@[S]@0b11010000@(Rm:bits(5))@0b000
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
sub_op : (boolean) = (op == b1);
setflags : (boolean) = (S == b1);
Some(AddSubCarry(d,n,m,datasize,sub_op,setflags));
}
-function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setflags))) = {
+function clause execute( AddSubCarry((d,n,m,(datasize as int('R)),sub_op,setflags))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
@@ -1941,7 +1941,7 @@ function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setfla
val decodeConditionalCompareImmediate : bits(32) -> option(ast) effect pure
function decodeConditionalCompareImmediate ([sf]@[op]@[b1]@0b11010010@(imm5 : bits(5))@(_cond:bits(4))@[b1]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
n : (reg_index) = UInt_reg(Rn);
- let datasize : {| 32, 64 |} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ let datasize : {| 32, 64 |} /* : int('R) */ = if sf == b1 then 64 else 32;
sub_op : boolean = (op == b1);
condition : bits(4) = _cond;
flags : bits(4) = nzcv;
@@ -1950,7 +1950,7 @@ function decodeConditionalCompareImmediate ([sf]@[op]@[b1]@0b11010010@(imm5 : bi
Some(ConditionalCompareImmediate((n,datasize,sub_op,condition,flags,imm)));
}
-function clause execute(ConditionalCompareImmediate((n,datasize as atom('R),sub_op,condition,flags,imm))) = {
+function clause execute(ConditionalCompareImmediate((n,datasize as int('R),sub_op,condition,flags,imm))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = imm;
carry_in : (bit) = b0;
@@ -1972,7 +1972,7 @@ val decodeConditionalCompareRegister : bits(32) -> option(ast) effect pure
function decodeConditionalCompareRegister ([sf]@[op]@[b1]@0b11010010@(Rm:bits(5))@ (_cond:bits(4))@[b0]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
n : reg_index = UInt_reg(Rn);
m : reg_index = UInt_reg(Rm);
- datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
sub_op : boolean = (op == b1);
condition : bits(4) = _cond;
flags : bits(4) = nzcv;
@@ -1980,7 +1980,7 @@ function decodeConditionalCompareRegister ([sf]@[op]@[b1]@0b11010010@(Rm:bits(5)
Some(ConditionalCompareRegister(n,m,datasize,sub_op,condition,flags));
}
-function clause execute (ConditionalCompareRegister((n,m,datasize as atom('R),sub_op,condition,flags))) = {
+function clause execute (ConditionalCompareRegister((n,m,datasize as int('R),sub_op,condition,flags))) = {
operand1 : bits('R) = rX(n);
operand2 : bits('R) = rX(m);
carry_in : bit = b0;
@@ -2005,7 +2005,7 @@ function decodeConditionalSelect ([sf]@[op]@[b0]@0b11010100@(Rm:bits(5))@(_cond:
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {|32,64|}/* (int('R)) */ = if sf == b1 then 64 else 32;
condition : (bits(4)) = _cond;
else_inv : (boolean) = (op == b1);
else_inc : (boolean) = (o2 == b1);
@@ -2013,7 +2013,7 @@ function decodeConditionalSelect ([sf]@[op]@[b0]@0b11010100@(Rm:bits(5))@(_cond:
Some(ConditionalSelect(d,n,m,datasize,condition,else_inv,else_inc));
}
-function clause execute ( ConditionalSelect((d,n,m,datasize as atom('R),condition,else_inv,else_inc)) ) = {
+function clause execute ( ConditionalSelect((d,n,m,datasize as int('R),condition,else_inv,else_inc)) ) = {
result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
@@ -2040,7 +2040,7 @@ function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b0000@(opc
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
- datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {|32,64|}/* (int('R)) */ = if sf == b1 then 64 else 32;
op : (RevOp) = RevOp_RBIT; /* ARM: uninitialized */
match opc {
@@ -2059,7 +2059,7 @@ function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b0000@(opc
Some(Reverse(d,n,datasize,op));
}
-function clause execute ( Reverse((d,n,datasize as atom('R),op)) ) = {
+function clause execute ( Reverse((d,n,datasize as int('R),op)) ) = {
result : (bits('R)) = Zeros(); /* ARM uninitialized */
/* let V : (bits(6)) = Zeros(); /\* ARM uninitialized *\/ */
@@ -2096,13 +2096,13 @@ function clause execute ( Reverse((d,n,datasize as atom('R),op)) ) = {
function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b00010@[op]@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
- datasize : {| 32,64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32,64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
opcode : (CountOp) = if op == b0 then CountOp_CLZ else CountOp_CLS;
Some(CountLeading(d,n,datasize,opcode));
}
-function clause execute (CountLeading((d,n,datasize as atom('R),opcode))) = {
+function clause execute (CountLeading((d,n,datasize as int('R),opcode))) = {
result : integer = 0; /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
@@ -2125,13 +2125,13 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b0000
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
_unsigned : (boolean) = (o1 == b0);
Some(Division(d,n,m,datasize,_unsigned));
}
-function clause execute ( Division((d,n,m,datasize as atom('R),_unsigned)) ) = {
+function clause execute ( Division((d,n,m,datasize as int('R),_unsigned)) ) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
result : (integer) = 0; /* ARM: uninitialized */
@@ -2152,13 +2152,13 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b0010
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
shift_type : (ShiftType) = DecodeShift(op2);
Some(Shift(d,n,m,datasize,shift_type));
}
-function clause execute (Shift((d,n,m,datasize as atom('R),shift_type))) = {
+function clause execute (Shift((d,n,m,datasize as int('R),shift_type))) = {
result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand2 : (bits('R)) = rX(m);
@@ -2174,14 +2174,14 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b010@
m : (reg_index) = UInt_reg(Rm);
if sf == b1 & sz != 0b11 then UnallocatedEncoding();
if sf == b0 & sz == 0b11 then UnallocatedEncoding();
- let size /* : {| 8,16,32,64 |} */ /* (atom('D)) */ = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
+ let size /* : {| 8,16,32,64 |} */ /* (int('D)) */ = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
assert (size == 8 | size == 16 | size == 32 | size == 64); /*FIXME: CP adding assertion to make typecheck*/
crc32c : (boolean) = (C == b1);
Some(CRC(d,n,m,size,crc32c));
}
-function clause execute ( CRC((d,n,m,(size as atom('D)),crc32c)) ) = {
+function clause execute ( CRC((d,n,m,(size as int('D)),crc32c)) ) = {
if ~(HaveCRCExt()) then
UnallocatedEncoding();
@@ -2208,14 +2208,14 @@ function clause decodeData3Source ([sf]@0b00@0b11011@0b000@(Rm:bits(5))@[o0]@(Ra
let n : (reg_index) = UInt_reg(Rn);
let m : (reg_index) = UInt_reg(Rm);
let a : (reg_index) = UInt_reg(Ra);
- let destsize /* (atom('R)) */ = if sf == b1 then 64 else 32;
- let datasize /* (atom('D)) */ = destsize;
+ let destsize /* (int('R)) */ = if sf == b1 then 64 else 32;
+ let datasize /* (int('D)) */ = destsize;
let sub_op : (boolean) = (o0 == b1);
Some(MultiplyAddSub((d,n,m,a,destsize,datasize,sub_op)));
}
-function clause execute ( MultiplyAddSub((d,n,m,a,destsize as atom('D),datasize as atom('R),sub_op)) ) = {
+function clause execute ( MultiplyAddSub((d,n,m,a,destsize as int('D),datasize as int('R),sub_op)) ) = {
operand1 : (bits('D)) = rX(n);
operand2 : (bits('D)) = rX(m);
operand3 : (bits('R)) = rX(a);
@@ -2239,15 +2239,15 @@ function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b01@(Rm:bits(5))@[o0]@
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
a : (reg_index) = UInt_reg(Ra);
- destsize /* : (atom('R)) */ = 64;
- datasize /* : (atom('D)) */ = 32;
+ destsize /* : (int('R)) */ = 64;
+ datasize /* : (int('D)) */ = 32;
sub_op : (boolean) = (o0 == b1);
_unsigned : (boolean) = (U == b1);
Some(MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_unsigned));
}
-function clause execute ( MultiplyAddSubLong((d,n,m,a,destsize as atom('R),datasize as atom('D),sub_op,_unsigned)) ) = {
+function clause execute ( MultiplyAddSubLong((d,n,m,a,destsize as int('R),datasize as int('D),sub_op,_unsigned)) ) = {
operand1 : (bits('D)) = rX(n);
operand2 : (bits('D)) = rX(m);
operand3 : (bits('R)) = rX(a);
@@ -2269,14 +2269,14 @@ function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b10@(Rm:bits(5))@[b0]@
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
a : (reg_index) = UInt_reg(Ra); /* ignored by UMULH/SMULH */
- destsize /* : (atom('R)) */ = 64;
- datasize /* : (atom('D)) */ = destsize;
+ destsize /* : (int('R)) */ = 64;
+ datasize /* : (int('D)) */ = destsize;
_unsigned : (boolean) = (U == b1);
Some(MultiplyHigh(d,n,m,a,destsize,datasize,_unsigned));
}
-function clause execute ( MultiplyHigh((d,n,m,a,destsize as atom('R),datasize,_unsigned)) ) = {
+function clause execute ( MultiplyHigh((d,n,m,a,destsize as int('R),datasize,_unsigned)) ) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
@@ -2300,7 +2300,7 @@ function decodeLogicalShiftedRegister ([sf]@(opc:bits(2))@0b01010@(shift:bits(2)
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : {| 32,64 |} /* : (atom('R)) */ = if sf == b1 then 64 else 32;
+ datasize : {| 32,64 |} /* : (int('R)) */ = if sf == b1 then 64 else 32;
setflags : (boolean) = false; /* ARM: uninitialized */
op : (LogicalOp) = LogicalOp_AND; /* ARM: uninitialized */
match opc {
@@ -2319,7 +2319,7 @@ function decodeLogicalShiftedRegister ([sf]@(opc:bits(2))@0b01010@(shift:bits(2)
Some(LogicalShiftedRegister((d,n,m,datasize,setflags,op,shift_type,shift_amount,invert)))
}
-function clause execute (LogicalShiftedRegister((d,n,m,datasize as atom('R),setflags,op,shift_type,shift_amount,invert))) = {
+function clause execute (LogicalShiftedRegister((d,n,m,datasize as int('R),setflags,op,shift_type,shift_amount,invert))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = ShiftReg(m, shift_type, shift_amount);
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index 35961c02..ee9eabc9 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -288,7 +288,7 @@ function AArch64_CheckAlignment(address : bits(64), size : uinteger,
/** FUNCTION:// AArch64.MemSingle[] - non-assignment (read) form */
-val AArch64_rMemSingle : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType, boolean, bool) -> read_buffer_type effect {escape}
+val AArch64_rMemSingle : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType, boolean, bool) -> read_buffer_type effect {escape}
function AArch64_rMemSingle (read_buffer, address, size, acctype, wasaligned, exclusive) = {
/*assert size IN {1, 2, 4, 8, 16};*/
assert(address == Align(address, size));
@@ -310,7 +310,7 @@ function AArch64_rMemSingle (read_buffer, address, size, acctype, wasaligned, ex
/** FUNCTION:// AArch64.MemSingle[] - assignment (write) form */
-val AArch64_wMemSingle : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, boolean, bool, bits('N*8)) -> write_buffer_type effect {escape}
+val AArch64_wMemSingle : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, boolean, bool, bits('N*8)) -> write_buffer_type effect {escape}
function AArch64_wMemSingle (write_buffer, address, size, acctype, wasaligned, exclusive, value) = {
/*assert size IN {1, 2, 4, 8, 16};*/
assert(address == Align(address, size));
@@ -351,7 +351,7 @@ function CheckSPAlignment() = {
/** FUNCTION:// Mem[] - non-assignment (read) form */
-val rMem' : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64),atom('N), AccType, bool) -> read_buffer_type effect {escape,rreg}
+val rMem' : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64),int('N), AccType, bool) -> read_buffer_type effect {escape,rreg}
function rMem'(read_buffer, address, size, acctype, exclusive) =
{
/* ARM: assert size IN {1, 2, 4, 8, 16}; */
@@ -391,11 +391,11 @@ function rMem'(read_buffer, address, size, acctype, exclusive) =
read_buffer'
}
-val rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType) -> read_buffer_type effect {escape,rreg}
+val rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType) -> read_buffer_type effect {escape,rreg}
function rMem (read_buffer, address, size, acctype) =
rMem'(read_buffer, address, size, acctype, false)
-val rMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType) -> read_buffer_type effect {escape,rreg}
+val rMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType) -> read_buffer_type effect {escape,rreg}
function rMem_exclusive(read_buffer, address, size, acctype) =
rMem'(read_buffer, address, size, acctype, true)
@@ -405,7 +405,7 @@ function rMem_exclusive(read_buffer, address, size, acctype) =
store-exclusive, this function should only be called indirectly by one
of the functions that follow it.
returns true if the store-exclusive was successful. */
-val wMem' : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8), bool) -> write_buffer_type effect {escape,rreg}
+val wMem' : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8), bool) -> write_buffer_type effect {escape,rreg}
function wMem' (write_buffer, address, size, acctype, value, exclusive) = {
write_buffer' : write_buffer_type = write_buffer;
@@ -445,11 +445,11 @@ function wMem' (write_buffer, address, size, acctype, value, exclusive) = {
write_buffer'
}
-val wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
+val wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
function wMem (write_buffer, address, size, acctype, value) =
wMem'(write_buffer, address, size, acctype, value, false)
-val wMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
+val wMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
function wMem_exclusive(write_buffer, address, size, acctype, value) =
wMem'(write_buffer, address, size, acctype, value, true)
@@ -780,7 +780,7 @@ function DecodeRegExtend (op : bits(3)) -> ExtendType = {
/** FUNCTION:aarch64/instrs/extendreg/ExtendReg */
val ExtendReg : forall 'N 'S, 'N in {8,16,32,64} & 'S >= 0 & 'S <= /* 4 */ 7.
- (implicit('N), reg_index, ExtendType, atom('S)) -> bits('N) effect {rreg,escape}
+ (implicit('N), reg_index, ExtendType, int('S)) -> bits('N) effect {rreg,escape}
function ExtendReg (N, _reg, etype, shift) = {
/*assert( shift >= 0 & shift <= 4 );*/
_val : bits('N) = rX(_reg);
@@ -810,7 +810,7 @@ function ExtendReg (N, _reg, etype, shift) = {
/** FUNCTION:(bits(M), bits(M)) DecodeBitMasks (bit immN, bits(6) imms, bits(6) immr, boolean immediate) */
val DecodeBitMasks : forall 'M, 'M >= 0 /* & 'E in {2,4,8,16,32,64} */. (implicit('M), bit, bits(6), bits(6), boolean) -> (bits('M), bits('M)) effect {escape}
-function DecodeBitMasks(M : atom('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+function DecodeBitMasks(M : int('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
/* let M = (length((bit['M]) 0)) in { */
/* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
/* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
@@ -837,7 +837,7 @@ function DecodeBitMasks(M : atom('M), immN : bit, imms : bits(6), immr : bits(6)
let R = UInt (immr & levels);
let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
- let esize as atom('E) = lsl(1, len);
+ let esize as int('E) = lsl(1, len);
let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
welem : bits('E) = ZeroExtend(Ones(S + 1));
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index 5b6cd52e..c2ed72ee 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -186,7 +186,7 @@ function ASR_C (x, shift) = {
/* SignExtend : */
-/* 'S+'N > 'N & 'N >= 1. (atom('S+'N),bits('N)) -> bits('S+'N) */
+/* 'S+'N > 'N & 'N >= 1. (int('S+'N),bits('N)) -> bits('S+'N) */
/** FUNCTION:integer Align(integer x, integer y) */
@@ -314,11 +314,11 @@ function LSR_C(x, shift) = {
/** FUNCTION:integer Min(integer a, integer b) */
-val Min : forall 'M 'N.(atom('M), atom('N)) -> min('M,'N)
+val Min : forall 'M 'N.(int('M), int('N)) -> min('M,'N)
function Min (a,b) =
if a <= b then a else b
-val uMin : forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> min('M,'N)
+val uMin : forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> min('M,'N)
function uMin (a,b) =
if a <= b then a else b
@@ -537,7 +537,7 @@ function BigEndian() = {
val BigEndianReverse : forall 'W, 'W in {8,16,32,64,128}. bits('W) -> bits('W) effect pure
function BigEndianReverse (value) = {
let 'half = 'W / 2;
- width : atom('W) = length(value);
+ width : int('W) = length(value);
/* half : uinteger = width / 2; */
if width == 8 then value
else {
@@ -601,15 +601,15 @@ function Hint_Prefetch(addr,hint,target,stream) = ()
/** FUNCTION:shared/functions/memory/_Mem */
/* regular load */
-/* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
/* non-temporal load (LDNP), see ARM ARM for special exception to normal memory ordering rules */
-/* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
/* load-acquire */
-/* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
/* load-exclusive */
-/* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
/* load-exclusive+acquire */
-/* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
struct read_buffer_type = {
acctype : AccType,
@@ -627,7 +627,7 @@ let empty_read_buffer : read_buffer_type =
address = Zeros()
}
-val _rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, AddressDescriptor, atom('N), AccType, bool) -> read_buffer_type effect {escape}
+val _rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, AddressDescriptor, int('N), AccType, bool) -> read_buffer_type effect {escape}
function _rMem(read_buffer, desc, size, acctype, exclusive) = {
if read_buffer.size == 0 then
struct { acctype = acctype,
@@ -644,7 +644,7 @@ function _rMem(read_buffer, desc, size, acctype, exclusive) = {
}
}
-val flush_read_buffer : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, atom('N)) -> bits('N*8) effect {rmem, rreg, escape}
+val flush_read_buffer : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, int('N)) -> bits('N*8) effect {rmem, rreg, escape}
function flush_read_buffer(read_buffer, size) =
{
assert(read_buffer.size == size);
@@ -677,15 +677,15 @@ function flush_read_buffer(read_buffer, size) =
/** FUNCTION:_Mem[AddressDescriptor desc, integer size, AccType acctype] = bits(8*size) value; */
/* regular store */
-/* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
/* store-release */
-/* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
/* store-exclusive */
-/* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
/* store-exclusive+release */
-/* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
-val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), atom('N), AccType, boolean) -> unit effect {eamem, escape}
+val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), int('N), AccType, boolean) -> unit effect {eamem, escape}
function wMem_Addr(address, size, acctype, excl) =
{
match (excl, acctype) {
@@ -701,9 +701,9 @@ function wMem_Addr(address, size, acctype, excl) =
/* regular store */
-/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (atom('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
/* store-exclusive */
-/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (atom('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
struct write_buffer_type = {
@@ -724,7 +724,7 @@ let empty_write_buffer : write_buffer_type = struct {
value = Zeros()
}
-val _wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, AddressDescriptor, atom('N), AccType, bool, bits('N*8)) -> write_buffer_type effect {escape}
+val _wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, AddressDescriptor, int('N), AccType, bool, bits('N*8)) -> write_buffer_type effect {escape}
function _wMem(write_buffer, desc, size, acctype, exclusive, value) = {
let s = write_buffer.size;
if s == 0 then {
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 28be493c..66071b3a 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -153,10 +153,10 @@ struct AddressDescriptor = {
enum PrefetchHint = {Prefetch_READ, Prefetch_WRITE, Prefetch_EXEC}
-val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect {escape}
-val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
-val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
-val ROR_C : forall 'N 'S, 'N >= 1 & 'S != 0. (bits('N),atom('S)) -> (bits('N), bit) effect pure
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect {escape}
+val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect pure
+val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect pure
+val ROR_C : forall 'N 'S, 'N >= 1 & 'S != 0. (bits('N),int('S)) -> (bits('N), bit) effect pure
val IsZero : forall 'N, 'N >=0. bits('N) -> boolean effect pure
val Replicate : forall 'N 'M, 'N >='M & 'M >=0. (implicit('N),bits('M)) -> bits('N) effect {escape}
val SignExtend : forall 'N 'M, 'N > 'M & 'M >= 1. (implicit('N),bits('M)) -> bits('N) effect {escape}
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index ffb91630..2dbd2bf4 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -35,8 +35,8 @@ overload operator << = {shift_bits_left, shift_left}
overload operator >> = {shift_bits_right, shift_right}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
+val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
@@ -58,7 +58,7 @@ function operator <_u (x, y) = unsigned(x) < unsigned(y)
function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
-val pow2_atom = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+val pow2_atom = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
val pow2_int = "pow2" : int -> int
overload pow2 = {pow2_atom, pow2_int}
@@ -125,15 +125,15 @@ overload operator - = {sub_int, sub_vec, sub_vec_int}
val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} :
- forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> atom(div('M,'N))
+ forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> int(div('M,'N))
val quotient = {ocaml: "quotient", lem: "integerDiv"} :
- forall 'M 'N. (atom('M), atom('N)) -> atom(div('M,'N))
+ forall 'M 'N. (int('M), int('N)) -> int(div('M,'N))
overload quot = {quotient_nat, quotient}
-val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
+val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (int('w), int, int) -> bits('w)
-val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
+val __GetSlice_int : forall 'n, 'n >= 0. (int('n), int, int) -> bits('n)
function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
val to_bits : forall 'l, 'l >= 0.(implicit('l), int) -> bits('l)
@@ -158,7 +158,7 @@ val mod = {
lem: "integerMod",
c: "tmod_int",
coq: "Z.rem"
-} : forall 'M 'N. (atom('M), atom('N)) -> {'O, 0 <= 'O & 'O < N . atom('O)}
+} : forall 'M 'N. (int('M), int('N)) -> {'O, 0 <= 'O & 'O < N . int('O)}
/* overload operator % = {mod_int} */
@@ -170,7 +170,7 @@ function error(message) = {
exit()
}
-type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. atom('O)}
+type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. int('O)}
val appendL : forall ('a:Type). (list('a),list('a)) -> list('a)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:49 +0000