- class Logic m p where
- (|-) :: Logic m p => m -> p -> Bool
- data PacketPredicate
- = AndPP PacketPredicate PacketPredicate
- | OrPP PacketPredicate PacketPredicate
- | TruePP
- | FalsePP
- | InPortIs PortID
- | MacSourceIs EthernetAddress
- | MacDestIs EthernetAddress
- | VLANIDIs VLANID
- | VLANPriority VLANPriority
- | MacFrameTypeIs EthernetTypeCode
- | IPTypeOfService IPTypeOfService
- | IPProtocolIs IPProtocol
- | IPSourceIn IPAddressPrefix
- | IPDestIn IPAddressPrefix
- | SenderTransportPortIs Word16
- | ReceiverTransportPortIs Word16
- type Clause = [Literal]
- type Literal = PacketPredicate
- (<&>) :: PacketPredicate -> PacketPredicate -> PacketPredicate
- (<|>) :: PacketPredicate -> PacketPredicate -> PacketPredicate
- anyPacket :: PacketPredicate
- inPortIs :: PortID -> PacketPredicate
- ethSourceIs :: EthernetAddress -> PacketPredicate
- ethDestIs :: EthernetAddress -> PacketPredicate
- vLANIDIs :: VLANID -> PacketPredicate
- vlanPriority :: VLANPriority -> PacketPredicate
- ethFrameTypeIs :: EthernetTypeCode -> PacketPredicate
- ipTypeOfService :: IPTypeOfService -> PacketPredicate
- transportProtocolIs :: IPProtocol -> PacketPredicate
- ipSourceIn :: IPAddressPrefix -> PacketPredicate
- ipDestIn :: IPAddressPrefix -> PacketPredicate
- senderTransportIs :: Word16 -> PacketPredicate
- receiverTransportIs :: Word16 -> PacketPredicate
- receiverTransportIn :: [Word16] -> PacketPredicate
- ands :: [PacketPredicate] -> PacketPredicate
- ors :: [PacketPredicate] -> PacketPredicate
- satisfies :: (PortID, EthernetFrame) -> PacketPredicate -> Bool
- clauses :: PacketPredicate -> [Clause]
- literals :: PacketPredicate -> [Literal]
- overlaps :: PacketPredicate -> PacketPredicate -> Bool
- dhcp :: PacketPredicate
- dns :: PacketPredicate
- arp :: PacketPredicate
- lldp :: PacketPredicate
- ip :: PacketPredicate
- udp :: PacketPredicate
- ethSourceDestAre :: EthernetAddress -> EthernetAddress -> PacketPredicate
- fromMatch :: Match -> PacketPredicate
- toMatches :: PacketPredicate -> Maybe [Match]
- realizable :: PacketPredicate -> Bool
- packetInFrame :: PacketInfo -> Either ErrorMessage EthernetFrame
- exactPredicate :: PacketInfo -> Either ErrorMessage PacketPredicate
- packetInMatches :: PacketInfo -> PacketPredicate -> Either ErrorMessage Bool
Packet predicates and match semantics
Type class for pairs of types where one type is a set of structures, and the other is a set of predicates over these structures, and for which there exists a relations of satisfaction.
Packet Predicates Note that values of this data type should NOT be constructed using the constructors of this data type, but rather through the functions defined below. The functions below maintain this data type's invariants, whereas these constructors do not.
A clause is a list of literals. A packet satisfies a clause if it satisfies all the literals in the clause. From this, it follows that any packet satisfies an empty clause; i.e. the empty clause is equivalent to True.
A literal is any packet predicate except those formed using conjunction or disjunction. The type synonym does not enforce this constraint - we just use it as a reminder of the intent.
This function defines when an incoming packet (as received by a switch) satisfies a given packet predicate.
Computes the clauses for a packet predicate; assumes the data type invariants hold. A packet satisfies a list of clauses if it satisfies some clause in the list. From this it follows that no packet satisfies the empty list of clauses. I.e. the empty list of clauses is equivalent to False.
With the above, we can now calculate whether two packet predicates overlap, that is, when their intersection is non-empty.
Commonly occurring packet predicates.
Packet predicates and matches for this version
Calculates a packet predicate that matches the same in-packets as the given match.
The disjunction of (toMatches pred) matches the same set of packets as the packet predicate pred does.