1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
val DecodeBitMasks2 : forall 'M 'S 'd, 'M >= 'd + 1 & 'S >= 0 & 'd >= 0. (int, int('S), nat, int('d), int('M)) -> (bits('M), bits('M)) effect {escape}
function DecodeBitMasks2(esize as 'E, S, R, d, M) = {
assert(constraint('E in {2,4,8,16,32,64} & 'M >= 'E & 'E >= 'd + 1));
assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
welem : bits('E) = ZeroExtend(Ones(S + 1));
telem : bits('E) = ZeroExtend(Ones(d + 1));
wmask = Replicate(M,ROR(welem, R));
tmask = Replicate(M,telem);
(wmask, tmask);
}
function DecodeBitMasks(M : int('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
/* let M = (length((bit['M]) 0)) in { */
/* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
/* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
levels : bits(6) = Zeros(); /* ARM: uninitialized */
/* Compute log2 of element size */
/* 2^len must be in range [2, 'M] */
let len : range(0,6) = match HighestSetBit([immN]@(~(imms))) {
None() => { assert (false, "DecodeBitMasks: HighestSetBit returned None"); 0; },
Some(c) => c
};
if len < 1 then {ReservedValue(); exit()} else {
assert(M >= lsl(1, len));
/* Determine S, R and S - R parameters */
levels = ZeroExtend(Ones(len));
/* For logical immediates an all-ones value of S is reserved */
/* since it would generate a useless all-ones result (many times) */
if immediate & ((imms & levels) == levels) then
ReservedValue();
let S = UInt (imms & levels);
let R = UInt (immr & levels);
let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
let esize as int('E) = lsl(1, len);
let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
DecodeBitMasks2(esize, S, R, d, M);
}}
|
