Header
Version: TYPE ~ CARDINAL [0..0FH];
thisVersion: Version ~ 4;
IHL: TYPE ~ CARDINAL [0..0FH];
minIHL: IHL ~ 5;
IHLBytes:
PROC [b: Buffer]
RETURNS [
CARD16] ~
INLINE {
Return number of bytes in internet header, counting options.
RETURN[b.hdr1.ihl * 4] };
maxOptionsBytes: CARDINAL = 4 * (IHL.LAST - minIHL);
OptionsBytes:
PROC [b: Buffer]
RETURNS [
CARD16] ~
INLINE {
Return number of bytes of options in IP Hdr.
RETURN[(b.hdr1.ihl * 4) - hdrBytes] };
DataBytes:
PROC [b: Buffer]
RETURNS [
CARD16] ~
INLINE {
Return number of bytes of data in IP Body.
RETURN[Basics.Card16FromH[b.hdr1.length] - (b.hdr1.ihl * 4)] };
FragmentCtl: TYPE ~ HWORD;
defaultFragmentCtl: FragmentCtl ~ [0, 0];
defaultFragmentCtlDontFragment: FragmentCtl ~ [40H, 0];
Masks for use against FragmentCtl
dontFragmentMask: FragmentCtl ~ [40H, 0];
moreFragmentsMask: FragmentCtl ~ [20H, 0];
fragmentOffsetMask: FragmentCtl ~ [1FH, 0FFH];
DontFragment:
PROC [b: Buffer]
RETURNS [
BOOL] ~
INLINE {
RETURN [
Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[dontFragmentMask]] # 0];
};
MoreFragments:
PROC [b: Buffer]
RETURNS [
BOOL] ~
INLINE {
RETURN [
Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[moreFragmentsMask]] # 0];
};
FragmentOffset:
PROC [b: Buffer]
RETURNS [
CARD16] ~
INLINE {
Result is the offset in 8-byte chunks from the beginning of the datagram, not counting the header.
RETURN[Basics.Card16FromH[LOOPHOLE[Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[fragmentOffsetMask]]]]];
};
FragmentOffsetBytes:
PROC [b: Buffer]
RETURNS [
CARD16] ~
INLINE {
Result is the offset in bytes from the beginning of the datagram, not counting the header.
RETURN[8*Basics.Card16FromH[LOOPHOLE[Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[fragmentOffsetMask]]]]];
};
InteriorFragmentCtl:
PROC [byteOffset:
CARD16]
RETURNS [
HWORD] ~
INLINE {
The offset is in bytes from the beginning of the datagram, not counting the header.
RETURN [LOOPHOLE[Basics.BITOR[LOOPHOLE[moreFragmentsMask], LOOPHOLE[Basics.HFromCard16[byteOffset/8]]]] ] };
FinalFragmentCtl:
PROC [byteOffset:
CARD16]
RETURNS [
HWORD] ~
INLINE {
The offset is in bytes from the beginning of the datagram, not counting the header.
RETURN [Basics.HFromCard16[byteOffset/8]] };
TypeOfService:
TYPE ~
MACHINE
DEPENDENT
RECORD [
precedence: Precedence,
lowDelay: BOOL,
highThroughput: BOOL,
highReliability: BOOL,
filler0: BOOL,
filler1: BOOL
];
defaultTypeOfService: TypeOfService ~
[routine, FALSE, FALSE, FALSE, FALSE, FALSE];
Precedence:
TYPE ~
MACHINE
DEPENDENT {
routine(0),
priority(1),
immediate(2),
flash(3),
flashOverride(4),
critECP(5),
inetCtl(6),
netCtl(7)
};
maxTimeToLive: BYTE ~ 60;
Protocol:
TYPE ~
MACHINE
DEPENDENT {
icmp(1), -- Internet Control Message Protocol
igmp(2), -- Internet Group Management Protocol
tcp(6), -- Transmission Control Protocol
egp(8), -- Exterior Gateway Protocol
igp(9), -- Interior Gateway
pup(12), -- PUP
udp(17), -- User Datagram Protocol
xnsidp(22), -- XNS Internet Datagram Packet
isotp4(29), -- ISO Transport Protocol Class 4
netblt(30), -- Bulk Data Transfer Protocol
last(0FFH)
};
Hdr:
TYPE ~
MACHINE
DEPENDENT
RECORD [
version: Version ← thisVersion,
ihl: IHL ← minIHL,
typeOfService: TypeOfService ← defaultTypeOfService,
length: HWORD,
fragmentId: HWORD ← [0, 0],
fragmentCtl: FragmentCtl ← defaultFragmentCtl,
timeToLive: BYTE,
protocol: Protocol,
checksum: HWORD ← [0, 0],
source: Arpa.Address,
dest: Arpa.Address];
hdrBytes: CARDINAL ~ BYTES[Hdr];
Options
These appear in CommBuffer.BufferObject.spaceForOptions.
OptionType:
TYPE ~
MACHINE
DEPENDENT
RECORD [
mustBeCopied: BOOL,
class: [0..3B],
number: OptionNumber
];
OptionNumber:
TYPE ~
MACHINE
DEPENDENT {
endOfList(0),
noOp(1),
security(2),
looseSourceRouting(3),
timestamp(4),
recordRoute(7),
streamID(8),
strictSourceRouting(9),
last(37B)
};
Option:
TYPE ~
MACHINE
DEPENDENT
RECORD [
type: OptionType,
length: BYTE
];
variableLength: BYTE ~ 0;
endOfListOption: Option ~ [[FALSE, 0, endOfList], 1]; -- no length field!
noOpOption: Option ~ [[FALSE, 0, noOp], 1]; -- no length field!
securityOption: Option ~ [[TRUE, 0, security], 11];
looseSourceRoutingOption: Option ~ [[TRUE, 0, looseSourceRouting], variableLength];
timestampOption: Option ~ [[FALSE, 2, timestamp], variableLength];
recordRouteOption: Option ~ [[FALSE, 0, recordRoute], variableLength];
streamIDOption: Option ~ [[FALSE, 0, streamID], 4];
strictSourceRoutingOption: Option ~ [[TRUE, 0, strictSourceRouting], variableLength];
}.