CirioTargetsImpl.mesa
Copyright Ó 1991, 1992 by Xerox Corporation. All rights reserved.
Laurie Horton, February 28, 1992 10:16 am PST
Last tweaked by Mike Spreitzer September 19, 1991 9:31 am PDT
Philip James, February 28, 1992 11:20 am PST
Katsuyuki Komatsu December 11, 1992 8:54 pm PST
Jas, January 5, 1993 3:25 pm PST
DIRECTORY
CirioMemory, CirioNubAccess, CirioTargets, CirioTypes, IO, Rope,
LoadStateAccess USING[LoadedModuleInfo],
ObjectFiles USING [Parsed],
ObjectFilesPrivate USING [Module],
SGI USING [FindMatchingProcDescr, WireProcDescriptorBody],
PBasics USING [BITLSHIFT, BITAND];
CirioTargetsImpl: CEDAR PROGRAM
IMPORTS CirioMemory, CirioNubAccess, IO, Rope, PBasics, SGI
EXPORTS CirioTargets =
BEGIN OPEN CirioMemory, CirioTargets;
BitAddr: TYPE ~ CirioTypes.BitAddr;
Mem: TYPE ~ CirioTargets.Mem;
Target: TYPE ~ CirioTargets.Target;
LoadedModuleInfo: TYPE ~ LoadStateAccess.LoadedModuleInfo;
Error: PUBLIC ERROR [msg: ROPE] ~ CODE;
CreateTarget: PUBLIC PROC [h: CirioNubAccess.Handle] RETURNS [Target] ~
{
SPARCTarget: PROC [h: CirioNubAccess.Handle, instrSet, opSys: Rope.ROPE] RETURNS[Target] ~ {
target: Target;
SELECT TRUE FROM
Rope.Equal[opSys, SunOS4] =>
target ← NEW[CirioTargets.TargetRep ← [
nub: h,
bitsPerAu: 8,
bitsPerPtr: 32,
ausPerPtr: 4,
ptrSize: [4, 0],
instrSet: instrSet,
opSys: opSys,
FpFromSp: SPARCSunOS4FpFromSp,
NextSp: SPARCSunOS4NextSp,
ReadPc: SPARCSunOS4ReadPc,
ReadReg: SPARCSunOS4ReadReg,
WriteReg: SPARCSunOS4WriteReg,
RegAddr: SPARCSunOS4RegAddr,
DescriptorFromPC: SPARCSunOS4DescriptorFromPC,
CNameToLoaderName: SPARCSunOS4CNameToLoaderName
]];
Rope.Equal[opSys, SunOS5] =>
target ← NEW[CirioTargets.TargetRep ← [
nub: h,
bitsPerAu: 8,
bitsPerPtr: 32,
ausPerPtr: 4,
ptrSize: [4, 0],
instrSet: instrSet,
opSys: opSys,
FpFromSp: SPARCSunOS4FpFromSp,
NextSp: SPARCSunOS4NextSp,
ReadPc: SPARCSunOS4ReadPc,
ReadReg: SPARCSunOS4ReadReg,
WriteReg: SPARCSunOS4WriteReg,
RegAddr: SPARCSunOS4RegAddr,
DescriptorFromPC: SPARCSunOS4DescriptorFromPC,
CNameToLoaderName: SPARCSunOS5CNameToLoaderName
]];
ENDCASE => Error[Rope.Cat["Unsupported opSys: ", opSys, "\N"]];
RETURN[target];
};
RS6000Target: PROC [h: CirioNubAccess.Handle, instrSet, opSys: Rope.ROPE] RETURNS[Target] ~ {
target: Target;
IF NOT Rope.Equal[opSys, AIX] THEN Error[Rope.Cat["Unsupported opSys: ", opSys, "\N"]];
target ← NEW[CirioTargets.TargetRep ← [
nub: h,
bitsPerAu: 8,
bitsPerPtr: 32,
ausPerPtr: 4,
ptrSize: [4, 0],
instrSet: instrSet,
opSys: opSys,
FpFromSp: RS6000AIXFpFromSp,
NextSp: RS6000AIXNextSp,
ReadPc: RS6000AIXReadPc,
ReadReg: RS6000AIXReadReg,
WriteReg: RS6000AIXWriteReg,
RegAddr: RS6000AIXRegAddr,
DescriptorFromPC: RS6000AIXDescriptorFromPC,
CNameToLoaderName: RS6000AIXCNameToLoaderName
]];
RETURN[target];
};
MIPSTarget: PROC [h: CirioNubAccess.Handle, instrSet, opSys: Rope.ROPE] RETURNS[Target] ~ {
target: Target;
IF NOT (Rope.Equal[opSys, IRIX]) THEN Error[Rope.Cat["Unsupported opSys: ", opSys, "\N"]];
target ← NEW[CirioTargets.TargetRep ← [
nub: h,
bitsPerAu: 8,
bitsPerPtr: 32,
ausPerPtr: 4,
ptrSize: [4, 0],
instrSet: instrSet,
opSys: opSys,
FpFromSp: MIPSFpFromSp,
NextSp: MIPSNextSp,
ReadPc: MIPSReadPc,
ReadReg: MIPSReadReg,
WriteReg: MIPSWriteReg,
RegAddr: MIPSRegAddr,
DescriptorFromPC: MIPSDescriptorFromPC,
CNameToLoaderName: MIPSCNameToLoaderName
]];
RETURN[target];
};
instruction set names
SPARC: Rope.ROPE ← "SPARC";
RS6000: Rope.ROPE ← "RS6000";
MIPSEL: Rope.ROPE ← "MIPSEL"; -- MIPS little endian
MIPSEB: Rope.ROPE ← "MIPSEB"; -- MIPS big endian
operating system names
SunOS4: Rope.ROPE ← "SunOS4";
SunOS5: Rope.ROPE ← "SunOS5";
AIX: Rope.ROPE ← "AIX";
OSF1: Rope.ROPE ← "OSF1";
IRIX: Rope.ROPE ← "IRIX";
instrSet, opSys: Rope.ROPE;
[instrSet, opSys] ← CirioNubAccess.GetInstructionSetAndOperatingSystem[h];
SELECT TRUE FROM
Rope.Equal[instrSet, SPARC] => RETURN[SPARCTarget[h, instrSet, opSys]];
Rope.Equal[instrSet, RS6000] => RETURN[RS6000Target[h, instrSet, opSys]];
Rope.Equal[instrSet, MIPSEL] => RETURN[MIPSTarget[h, instrSet, opSys]];
Rope.Equal[instrSet, MIPSEB] => RETURN[MIPSTarget[h, instrSet, opSys]];
ENDCASE => Error[Rope.Cat["Unsupported instrSet: ", instrSet, "\N"]];
};
SPARC-SunOS4 procs
The parsed and absPC arguments are for the MIPS targets only
SPARCSunOS4FpFromSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
stackOffset: INT ← 14*4;
RETURN[ReadValue[t, sp, stackOffset]];
};
SPARCSunOS4NextSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
RETURN[fp];
};
SPARCSunOS4ReadPc: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
stackOffset: INT ← 15*4;
RETURN[ReadValue[t, sp, stackOffset]];
};
SPARCSunOS4ReadReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD] RETURNS [CARD] ~ {
regMem: Mem;
IF reg < 16 OR reg > 31 THEN Error[IO.PutFR["Can't read register: %g\N", IO.int[reg]]];
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], BaCons[(reg-16)*4, 0], FALSE];
RETURN[regMem.MemRead[32, zeroBA]];
};
SPARCSunOS4WriteReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, val: CARD, absPC: CARD] ~ {
regMem: Mem;
IF reg < 16 OR reg > 31 THEN Error[IO.PutFR["Can't write register: %g\N", IO.int[reg]]];
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], BaCons[(reg-16)*4, 0], FALSE];
regMem.MemWrite[val, 32, zeroBA];
RETURN;
};
SPARCSunOS4RegAddr: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD] RETURNS [BitAddr] ~ {
For SPARCS, the registers are stored on the stack as follows:
globals  r0 - r7 not available on the stack
outputs  r8 - r15 @ fp(callee's)+(reg-8)*4
locals   r16-r23 @ sp+(reg-16)*4
inputs  r24-r29 @ sp+(reg-16)*4
frame pointer (fp)
(caller's sp) r30 @ sp+(reg-16)*4
return address (pc) r31 @ sp+(reg-16)*4
addr: BitAddr;
addrBS: BitStretch;
IF reg < 16 OR reg > 31 THEN Error[IO.PutFR["Can't find address for register: %g\N", IO.int[reg]]];
addrBS ← frame.MemReadPtrReg[sp];
addr ← BaAdd[addrBS.start, AusToBa[(reg-16)*4]];
RETURN[addr];
};
SPARCSunOS4DescriptorFromPC: PROC [t: Target, pc: BitAddr] RETURNS [BitAddr] ~ {
RETURN[pc];
};
SPARCSunOS4CNameToLoaderName: PROC [t: Target, cName: Rope.ROPE] RETURNS [Rope.ROPE] ~ {
IF cName = NIL THEN RETURN [cName];
IF cName.IsEmpty THEN RETURN [cName];
RETURN[Rope.Cat["←", cName]];
};
SPARCSunOS5CNameToLoaderName: PROC [t: Target, cName: Rope.ROPE] RETURNS [Rope.ROPE] ~ {
RETURN [cName];
};
RS6000-AIX procs
The parsed and absPC arguments are for the MIPS targets only
RS6000AIXFpFromSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
RETURN[sp];
};
RS6000AIXNextSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
stackOffset: INT ← 0*4;
RETURN[ReadValue[t, sp, stackOffset]];
};
RS6000AIXReadPc: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ {
stackOffset: INT ← 2*4;
newfp: BitAddr ← ReadValue[t, fp, 0*4];
IF newfp = CirioMemory.zeroBA THEN RETURN[CirioMemory.unspecdBA];
RETURN[ReadValue[t, newfp, stackOffset]];
};
RS6000AIXReadReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD] RETURNS [CARD] ~ {
offset: INT;
regMem: Mem;
IF reg = 0 OR reg > 10 THEN Error[IO.PutFR["Can't read register: %g\N", IO.int[reg]]];
offset ← IF reg = 1 THEN 0*4 ELSE (reg+3)*4;
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], BaCons[offset, 0], FALSE];
RETURN[regMem.MemRead[32, zeroBA]];
};
RS6000AIXWriteReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, val: CARD, absPC: CARD] ~ {
offset: INT;
regMem: Mem;
IF reg = 0 OR reg > 10 THEN Error[IO.PutFR["Can't read register: %g\N", IO.int[reg]]];
offset ← IF reg = 1 THEN 0*4 ELSE (reg+3)*4;
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], BaCons[offset, 0], FALSE];
regMem.MemWrite[val, 32, zeroBA];
RETURN;
};
RS6000AIXRegAddr: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD] RETURNS [BitAddr] ~ {
For RS6000s, the registers are stored on the stack as follows:
back chain  r1 @ sp + 0*4
saved TOC  r2 @ sp + (reg+3)*4
augument list r3 - r10 @ sp + (reg+3)*4
??  r11-r12 ??
gen purpose regs r13-r31 @ sp + ??
addr: BitAddr;
offset: INT;
addrBS: BitStretch;
IF reg = 0 OR reg > 10 THEN Error[IO.PutFR["Can't find address for register: %g\N", IO.int[reg]]];
offset ← IF reg = 1 THEN 0*4 ELSE (reg+3)*4;
addrBS ← frame.MemReadPtrReg[sp];
addr ← BaAdd[addrBS.start, AusToBa[offset]];
RETURN[addr];
};
RS6000AIXDescriptorFromPC: PROC [t: Target, pc: BitAddr] RETURNS [BitAddr] ~ {
symEntry, tocEntry: CirioNubAccess.SymEntry;
tocName: Rope.ROPE;
symEntry ← CirioNubAccess.LookupSymEntryByValue[t.nub, BaToAus[pc], 0];
IF symEntry = NIL THEN RETURN[CirioMemory.unspecdBA];
tocName ← Rope.Substr[symEntry.name, 1, Rope.Length[symEntry.name] - 1];
tocEntry ← CirioNubAccess.LookupSymEntryByName[t.nub, tocName, FALSE, FALSE, 0];
IF tocEntry = NIL THEN RETURN[CirioMemory.unspecdBA];
RETURN[AusToBa[tocEntry.value]];
};
RS6000AIXCNameToLoaderName: PROC [t: Target, cName: Rope.ROPE] RETURNS [Rope.ROPE] ~ {
IF cName = NIL THEN RETURN [cName];
IF cName.IsEmpty THEN RETURN [cName];
RETURN[Rope.Cat[".", cName]];
};
MIPS IRIX target procs
MIPSFpFromSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp: BitAddr, absPC: CARD]
RETURNS [BitAddr] ~ TRUSTED {
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
frameReg: INT32;
frameSize: INT32;
fpAddr : BitAddr;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN [zeroBA];
frameReg ← currentPDR.framereg;
frameSize ← currentPDR.frameoffset;
fpAddr ← BaAdd [sp, BaCons [frameSize, 0]];
RETURN[fpAddr];
};
MIPSNextSp: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD] RETURNS [BitAddr] ~ TRUSTED {
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
fpReg : INT32;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN [zeroBA];
fpReg ← currentPDR.framereg;
IF fpReg = 8 THEN {
Special case, Do the right thing for a crazy XR←Jump6
RETURN[ReadValue[t, BaAdd [sp, BaCons [32, 0]], 0]];
};
the normal case
RETURN[fp];
};
MIPSReadPc: PROC [loadedModule: REF LoadedModuleInfo, t: Target, sp, fp: BitAddr, absPC: CARD]
RETURNS [BitAddr] ~ TRUSTED {
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
fpReg : INT32;
pcReg : INT32;
fpAddr : BitAddr;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN [zeroBA];
fpReg ← currentPDR.framereg;
pcReg ← currentPDR.pcreg;
fpAddr ← MIPSFpFromSp [loadedModule, t, sp, absPC];
IF fpReg = 8 THEN {
Special case, Do the right thing for a crazy XR←Jump6
RETURN[ReadValue[t, BaAdd [sp, BaCons [28, 0]], 0]];
};
-- the normal case, pc stored as $31
IF pcReg = 31 THEN {
frameOffset : INT32 ← currentPDR.regoffset;
frameSize : INT32 ← currentPDR.frameoffset;
offset : BitAddr ← BaCons [(frameSize + frameOffset), 0];
IF frameOffset # 0 THEN
RETURN[ReadValue[t, BaAdd [sp, offset], 0]]
ELSE
{
This is a special case for a leaf proc that was gotten to by a XR←Jump6
RETURN[ReadValue[t, BaSub [sp, BaCons [4, 0]], 0]];
};
} ELSE Error[IO.PutFR["Can't find correct PC reg\N"]];
};
FindPosOfRegOnMipsStack: PROC [reg: INT, procDescrRegmask: INT32]
RETURNS [INT] = {
RegArray: TYPE = ARRAY [1..10] OF INT;
n: INT;
regMask, bitMask: INT32;
savedReg: RegArray ← RegArray[31, 30, 23, 22, 21, 20, 19, 18, 17, 16];
pos: INT ← 1;
Set a local variable to the bit number of the register we are interested in.
regMask ← PBasics.BITLSHIFT[1, reg];
Check and make sure that the register was saved.
IF PBasics.BITAND[regMask, procDescrRegmask] = 1 THEN {
Loop through the registers that could be saved counting the position
of saved registers until the register that we are interested in is found.
FOR n IN [1..10] DO
This is the register we are at.
bitMask ← PBasics.BITLSHIFT[1, savedReg[n]];
Check if the current register was saved.
IF PBasics.BITAND[bitMask, procDescrRegmask] = 1 THEN {
pos ← pos+1;
If we found the register that we are interested in we're done.
IF bitMask = regMask THEN
GO TO stopedAtRegister;
};
ENDLOOP;
EXITS
stopedAtRegister => RETURN [pos];
};
RETURN [-1];
};
MIPSReadReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD]
RETURNS [CARD] ~ TRUSTED {
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
frameOffset : INT32;
frameSize : INT32;
posInStack : INT;
offset : BitAddr;
regMem: Mem;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN [0];
frameOffset ← currentPDR.regoffset;
frameSize ← currentPDR.frameoffset;
posInStack ← FindPosOfRegOnMipsStack [reg, currentPDR.regmask];
IF reg < 16 OR (reg > 23 AND reg # 30) THEN
Error[IO.PutFR["Can't read register: %g\N", IO.int[reg]]];
offset ← BaCons [(frameSize + frameOffset - (posInStack * 4)), 0];
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], offset, FALSE];
RETURN[regMem.MemRead[32, zeroBA]];
};
MIPSWriteReg: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, val: CARD, absPC: CARD] ~ TRUSTED {
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
frameOffset : INT32;
frameSize : INT32;
posInStack : INT;
offset : BitAddr;
regMem: Mem;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN;
frameOffset ← currentPDR.regoffset;
frameSize ← currentPDR.frameoffset;
posInStack ← FindPosOfRegOnMipsStack [reg, currentPDR.regmask];
IF reg < 16 OR (reg > 23 AND reg # 30) THEN
Error[IO.PutFR["Can't write register: %g\N", IO.int[reg]]];
offset ← BaCons [(frameSize + frameOffset - (posInStack * 4)), 0];
regMem ← frame.MemPtrRegIndirect[sp, AusToBa[32], offset, FALSE];
regMem.MemWrite[val, 32, zeroBA];
RETURN;
};
MIPSRegAddr: PROC [loadedModule: REF LoadedModuleInfo, t: Target, frame: Mem, reg: INT, absPC: CARD]
RETURNS [BitAddr] ~ TRUSTED {
For Mips, the registers are stored in the stack on an if used basis and
is described as follows:
return address (pc) r31 registers are in the stack highest register number
saved general registers r30, r23-r16 first and then in decreasing order.
N = 0 being the position of the highest register
on the stack ($31), N = 1 for the next highest
register saved, etc.
@sp+(framesize+frameoffset-(N*4))
module: ObjectFilesPrivate.Module ← LOOPHOLE[loadedModule.module, ObjectFilesPrivate.Module];
parsed: ObjectFiles.Parsed ← LOOPHOLE[module.whole, ObjectFiles.Parsed];
currentPDR: SGI.WireProcDescriptorBody;
found: BOOLEAN;
frameOffset : INT32;
frameSize : INT32;
posInStack : INT;
offset : BitAddr;
addr: BitAddr;
addrBS: BitStretch;
dotORel: CARD;
dotORel ← absPC - loadedModule.lsi[text].base;
[currentPDR, found] ← SGI.FindMatchingProcDescr [dotORel, parsed];
IF found = FALSE THEN RETURN [zeroBA];
frameOffset ← currentPDR.regoffset;
frameSize ← currentPDR.frameoffset;
posInStack ← FindPosOfRegOnMipsStack [reg, currentPDR.regmask];
IF reg < 16 OR (reg > 23 AND reg # 30) THEN
Error[IO.PutFR["Can't find address for register: %g\N", IO.int[reg]]];
addrBS ← frame.MemReadPtrReg[sp];
offset ← BaCons [(frameSize + frameOffset - (posInStack * 4)), 0];
addr ← BaAdd[addrBS.start, offset];
RETURN[addr];
};
MIPSDescriptorFromPC: PROC [t: Target, pc: BitAddr] RETURNS [BitAddr] ~ {
RETURN[pc];
};
MIPSCNameToLoaderName: PROC [t: Target, cName: Rope.ROPE] RETURNS [Rope.ROPE] ~ {
IF cName = NIL THEN RETURN [cName];
IF cName.IsEmpty THEN RETURN [cName];
RETURN[cName];
};
Common procs
ReadValue: PROC[t: Target, base: BitAddr, offset: INT] RETURNS[BitAddr] ~ {
addr: BitAddr ← BaAdd[base, AusToBa[offset]];
value: BitAddr ← PtrToBa[CirioNubAccess.RaFromCi[t.nub, LOOPHOLE[BaToAus[addr]], 0].Read32BitsAsCard];
RETURN[value];
};
WriteValue: PROC[t: Target, base: BitAddr, offset: INT, val: CARD] ~ {
addr: BitAddr ← BaAdd[base, AusToBa[offset]];
CirioNubAccess.RaFromCi[t.nub, LOOPHOLE[BaToAus[addr]], 0].WriteCardAs32Bits[val];
RETURN;
};
END.