<> <> <> <<>> <> <<>> DIRECTORY Basics USING [BITAND, BITOR, Card16FromH, FWORD, HFromCard16, HWORD], CommBuffer USING [Overhead], Arpa USING [Address]; ArpaBuf: CEDAR DEFINITIONS IMPORTS Basics ~ { HWORD: TYPE ~ Basics.HWORD; FWORD: TYPE ~ Basics.FWORD; <> maxBytes: CARDINAL ~ 1500; <> <

> Version: TYPE ~ CARDINAL [0..0FH]; thisVersion: Version ~ 4; IHL: TYPE ~ CARDINAL [0..0FH]; minIHL: IHL ~ 5; IHLBytes: PROC [b: Buffer] RETURNS [CARD16] ~ INLINE { <> RETURN[b.hdr1.ihl * 4] }; maxOptionsBytes: CARDINAL = 4 * (IHL.LAST - minIHL); OptionsBytes: PROC [b: Buffer] RETURNS [CARD16] ~ INLINE { <> RETURN[(b.hdr1.ihl * 4) - hdrBytes] }; DataBytes: PROC [b: Buffer] RETURNS [CARD16] ~ INLINE { <> RETURN[Basics.Card16FromH[b.hdr1.length] - (b.hdr1.ihl * 4)] }; FragmentCtl: TYPE ~ HWORD; defaultFragmentCtl: FragmentCtl ~ [0, 0]; defaultFragmentCtlDontFragment: FragmentCtl ~ [40H, 0]; <> 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 { <> RETURN[Basics.Card16FromH[LOOPHOLE[Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[fragmentOffsetMask]]]]]; }; FragmentOffsetBytes: PROC [b: Buffer] RETURNS [CARD16] ~ INLINE { <> RETURN[8*Basics.Card16FromH[LOOPHOLE[Basics.BITAND[LOOPHOLE[b.hdr1.fragmentCtl], LOOPHOLE[fragmentOffsetMask]]]]]; }; InteriorFragmentCtl: PROC [byteOffset: CARD16] RETURNS [HWORD] ~ INLINE { <> RETURN [LOOPHOLE[Basics.BITOR[LOOPHOLE[moreFragmentsMask], LOOPHOLE[Basics.HFromCard16[byteOffset/8]]]] ] }; FinalFragmentCtl: PROC [byteOffset: CARD16] RETURNS [HWORD] ~ INLINE { <> 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]; <> Body: TYPE ~ MACHINE DEPENDENT RECORD [ SELECT OVERLAID * FROM bytes => [bytes: PACKED ARRAY [0..maxBodyBytes) OF BYTE], chars => [chars: PACKED ARRAY [0..maxBodyChars) OF CHAR], hWords => [hWords: PACKED ARRAY [0..maxBodyHWords) OF HWORD], fWords => [fWords: PACKED ARRAY [0..maxBodyFWords) OF FWORD] ENDCASE ]; maxBodyBytes: CARDINAL ~ maxBytes - hdrBytes; maxBodyChars: CARDINAL ~ maxBodyBytes; maxBodyHWords: CARDINAL ~ maxBodyBytes/BYTES[HWORD]; maxBodyFWords: CARDINAL ~ maxBodyBytes/BYTES[FWORD]; <> Packet: TYPE ~ REF PacketObject; PacketObject: TYPE ~ MACHINE DEPENDENT RECORD [ hdr: Hdr, body: Body]; <> <> <<>> Buffer: TYPE ~ REF BufferObject; BufferObject: TYPE ~ MACHINE DEPENDENT RECORD [ ovh: CommBuffer.Overhead, hdr1: Hdr, body: Body]; <<>> <> <> <<>> 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]; }.