<> <> <> <> <<>> DIRECTORY DragOpsCross, DragOpsCrossUtils, PrincOps; DragOpsCrossHelp: CEDAR PROGRAM IMPORTS DragOpsCrossUtils = BEGIN OPEN DragOpsCross; <<>> <> BytePCToWordAddress: PROC [pc: ByteAddress] RETURNS [addr: Word, index: [0..bytesPerWord)] = { index _ HalfToCard[HalfAnd[LowHalf[pc], CardToHalf[bytesPerWord-1]]]; addr _ HalvesToWord[[ HalfShift[HighHalf[pc], -2], HalfOr[HalfShift[LowHalf[pc], -2], HalfShift[HighHalf[pc], 14]] ]]; }; WordAddressToBytePC: PROC [addr: Word, index: [0..bytesPerWord) _ 0] RETURNS [pc: ByteAddress] = { card: CARD = WordToCard[addr]; RETURN [[CardToWord[card+card+card+card+index]]]; }; FieldDescriptorToCard: PROC [fd: FieldDescriptor] RETURNS [CARDINAL] = TRUSTED { RETURN [LOOPHOLE[fd]]; }; CardToFieldDescriptor: PROC [card: CARDINAL] RETURNS [FieldDescriptor] = TRUSTED { RETURN [LOOPHOLE[card]]; }; StatusToWord: PROC [status: IFUStatusRec] RETURNS [Word] = TRUSTED { RETURN [LOOPHOLE[status]]; }; WordToStatus: PROC [word: Word] RETURNS [IFUStatusRec] = TRUSTED { RETURN [LOOPHOLE[word]]; }; <> BytesToWord: PROC [fb: FourBytes] RETURNS [Word] = TRUSTED { RETURN[LOOPHOLE[fb, Word]]; }; BytesToHalf: PROC [tb: TwoBytes] RETURNS [Half] = TRUSTED { RETURN[LOOPHOLE[tb, Half]]; }; WordToBytes: PROC [w: Word] RETURNS [FourBytes] = TRUSTED { RETURN[LOOPHOLE[w, FourBytes]]; }; HalfToBytes: PROC [h: Half] RETURNS [TwoBytes] = TRUSTED { RETURN[LOOPHOLE[h, TwoBytes]]; }; HalvesToWord: PROC [th: TwoHalves] RETURNS [Word] = TRUSTED { RETURN[LOOPHOLE[th, Word]]; }; WordToHalves: PROC [w: Word] RETURNS [TwoHalves] = TRUSTED { RETURN[LOOPHOLE[w, TwoHalves]]; }; HighHalf: PROC [w: Word] RETURNS [Half] = TRUSTED { RETURN[LOOPHOLE[w, TwoHalves][0]]; }; LowHalf: PROC [w: Word] RETURNS [Half] = TRUSTED { RETURN[LOOPHOLE[w, TwoHalves][1]]; }; LeftHalf: PROC [w: Word] RETURNS [Half] = TRUSTED { RETURN[LOOPHOLE[w, TwoHalves][0]]; }; RightHalf: PROC [w: Word] RETURNS [Half] = TRUSTED { RETURN[LOOPHOLE[w, TwoHalves][1]]; }; SwapHalves: PROC [w: Word] RETURNS [Word] = TRUSTED { RETURN [DragOpsCrossUtils.SwapHalves[w]]; }; <> <> CARD: TYPE = LONG CARDINAL; WordToInt: PROC [w: Word] RETURNS [INT] = TRUSTED { RETURN [DragOpsCrossUtils.WordToInt[w]]; }; IntToWord: PROC [int: INT] RETURNS [Word] = TRUSTED { RETURN [DragOpsCrossUtils.IntToWord[int]]; }; WordToCard: PROC [w: Word] RETURNS [CARD] = TRUSTED { RETURN [DragOpsCrossUtils.WordToCard[w]]; }; HalfToCard: PROC [h: Half] RETURNS [CARDINAL] = TRUSTED { RETURN [LOOPHOLE[h, CARDINAL]]; }; ByteToCard: PROC [b: Byte] RETURNS [[0..255]] = TRUSTED { RETURN [LOOPHOLE[b]]; }; CardToWord: PROC [card: CARD] RETURNS [Word] = TRUSTED { RETURN [DragOpsCrossUtils.CardToWord[card]]; }; CardToHalf: PROC [card: CARDINAL] RETURNS [Half] = TRUSTED { RETURN [LOOPHOLE[card, Half]]; }; CardToByte: PROC [card: [0..255]] RETURNS [Byte] = TRUSTED { RETURN [LOOPHOLE[card, Byte]]; }; <> <<>> DragAnd: PROC [a,b: Word] RETURNS [Word] = { <> RETURN [HalvesToWord[[ HalfAnd[LeftHalf[a], LeftHalf[b]], HalfAnd[RightHalf[a], RightHalf[b]] ]]]; }; DragOr: PROC [a,b: Word] RETURNS [Word] = { <> RETURN [HalvesToWord[[ HalfOr[LeftHalf[a], LeftHalf[b]], HalfOr[RightHalf[a], RightHalf[b]] ]]]; }; DragXor: PROC [a,b: Word] RETURNS [Word] = { <> RETURN [HalvesToWord[[ HalfXor[LeftHalf[a], LeftHalf[b]], HalfXor[RightHalf[a], RightHalf[b]] ]]]; }; DragNot: PROC [w: Word] RETURNS [Word] = { <> RETURN [HalvesToWord[[ HalfNot[LeftHalf[w]], HalfNot[RightHalf[w]] ]]]; }; VanillaAdd: PROC [a,b: Word] RETURNS [Word] = { <> RETURN [IntToWord[WordToInt[a]+WordToInt[b]]]; }; VanillaSub: PROC [a,b: Word] RETURNS [Word] = { <> RETURN [IntToWord[WordToInt[a]-WordToInt[b]]]; }; AddDelta: PROC [w: Word, delta: INT] RETURNS [Word] = { <> RETURN [IntToWord[WordToInt[w]+delta]]; }; <> <<>> HalfNot: PROC [h: Half] RETURNS [nh: Half] = TRUSTED { <> RETURN [DragOpsCrossUtils.HalfNot[h]]; }; HalfAnd: PROC [h0,h1: Half] RETURNS [h: Half] = TRUSTED { <> RETURN [DragOpsCrossUtils.HalfAnd[h0,h1]]; }; HalfOr: PROC [h0,h1: Half] RETURNS [h: Half] = TRUSTED { <> RETURN [DragOpsCrossUtils.HalfOr[h0,h1]]; }; HalfXor: PROC [h0,h1: Half] RETURNS [h: Half] = TRUSTED { <> RETURN [DragOpsCrossUtils.HalfXor[h0,h1]]; }; HalfShift: PROC [h: Half, dist: INTEGER] RETURNS [Half] = TRUSTED { <= 0) or right (if dist <= 0).>> RETURN [DragOpsCrossUtils.HalfShift[h, dist]]; }; <> DoubleWordShiftLeft: PROC [w0,w1: Word, dist: SixBitIndex] RETURNS [Word] = TRUSTED { <> SELECT dist FROM < 16 => RETURN [HalvesToWord[[ HalfOr[HalfShift[LeftHalf[w0], dist], HalfShift[RightHalf[w0], dist-16]], HalfOr[HalfShift[RightHalf[w0], dist], HalfShift[LeftHalf[w1], dist-16]]]]]; ENDCASE => { RETURN [HalvesToWord[[ HalfOr[HalfShift[RightHalf[w0], dist-16], HalfShift[LeftHalf[w1], dist-32]], HalfOr[HalfShift[LeftHalf[w1], dist-16], HalfShift[RightHalf[w1], dist-32]]]]]; }; }; SingleWordShiftLeft: PROC [word: Word, dist: SixBitIndex] RETURNS [Word] = TRUSTED { <> SELECT dist FROM < 16 => RETURN [HalvesToWord[[ HalfOr[HalfShift[LeftHalf[word], dist], HalfShift[RightHalf[word], dist-16]], HalfShift[RightHalf[word], dist]]]]; ENDCASE => { <= 32>> RETURN [HalvesToWord[[HalfShift[RightHalf[word], dist-16], ZerosHalf]]]; }; }; SingleWordShiftRight: PROC [word: Word, dist: SixBitIndex] RETURNS [Word] = TRUSTED { <> SELECT dist FROM < 16 => RETURN [HalvesToWord[[ HalfShift[LeftHalf[word], -dist], HalfOr[HalfShift[LeftHalf[word], 16-dist], HalfShift[RightHalf[word], -dist]] ]]]; ENDCASE => { RETURN [HalvesToWord[[ZerosHalf, HalfShift[LeftHalf[word], 16-dist]]]]; }; }; <> XopToBytePC: PROC [inst: Inst] RETURNS [LONG CARDINAL] = { RETURN [LOOPHOLE[inst, CARDINAL]*TrapWidthBytes+XopBase*bytesPerWord]; }; TrapIndexToBytePC: PROC [tx: TrapIndex] RETURNS [LONG CARDINAL] = { RETURN [LOOPHOLE[tx, CARDINAL]*TrapWidthBytes+TrapBase*bytesPerWord]; }; END.