291 atomic ip block

pkg/configuration/topology/external_ip.go

@@ -5,20 +5,20 @@ import (
 )
 
 type ExternalIP struct {
-	ipBlock
+	IPBlock
 }
 
 func NewExternalIP(block *netset.IPBlock) *ExternalIP {
-	e := &ExternalIP{ipBlock: ipBlock{Block: block, originalIP: block.String()}}
+	e := &ExternalIP{IPBlock: IPBlock{Block: block, OriginalIP: block.String()}}
 	return e
 }
 
-func (ip *ExternalIP) Name() string   { return ip.originalIP }
-func (ip *ExternalIP) String() string { return ip.originalIP }
+func (ip *ExternalIP) Name() string   { return ip.OriginalIP }
+func (ip *ExternalIP) String() string { return ip.OriginalIP }
 func (ip *ExternalIP) Kind() string   { return "external IP" }
-func (ip *ExternalIP) ID() string     { return ip.originalIP }
+func (ip *ExternalIP) ID() string     { return ip.OriginalIP }
 func (ip *ExternalIP) InfoStr() []string {
 	return []string{ip.Name(), ip.ID(), ip.Name()}
 }
 func (ip *ExternalIP) Tags() []string         { return nil }
-func (ip *ExternalIP) IPAddressesStr() string { return ip.originalIP }
+func (ip *ExternalIP) IPAddressesStr() string { return ip.OriginalIP }

pkg/configuration/topology/ip_blocks.go

@@ -8,26 +8,26 @@ import (
 )
 
 // a base struct to represent external endpoints, segments and rule block
-type ipBlock struct {
+type IPBlock struct {
 	Block      *netset.IPBlock
-	originalIP string
+	OriginalIP string
 }
 type RuleIPBlock struct {
-	ipBlock
+	IPBlock
 	VMs         []Endpoint
 	ExternalIPs []Endpoint
 }
 
 func NewRuleIPBlock(ip string, block *netset.IPBlock) *RuleIPBlock {
-	return &RuleIPBlock{ipBlock: ipBlock{Block: block, originalIP: ip}}
+	return &RuleIPBlock{IPBlock: IPBlock{Block: block, OriginalIP: ip}}
 }
 
 type Segment struct {
-	ipBlock
+	IPBlock
 	name string
 	VMs  []Endpoint
 }
 
 func NewSegment(name string, block *netset.IPBlock, subnetsNetworks []string) *Segment {
-	return &Segment{name: name, ipBlock: ipBlock{Block: block, originalIP: strings.Join(subnetsNetworks, common.CommaSeparator)}}
+	return &Segment{name: name, IPBlock: IPBlock{Block: block, OriginalIP: strings.Join(subnetsNetworks, common.CommaSeparator)}}
 }

pkg/synthesis/symbolicexpr/atomicGeneral.go

@@ -4,46 +4,6 @@ import (
 	"slices"
 )
 
-// tautology implementation
-
-func (tautology) String() string {
-	return "*"
-}
-
-func (tautology) name() string {
-	return ""
-}
-
-func (tautology) negate() atomic {
-	return tautology{}
-}
-
-func (tautology) isNegation() bool {
-	return false
-}
-
-func (tautology) IsTautology() bool {
-	return true
-}
-
-// returns true iff otherAt is negation of
-// once we cache the atomic terms, we can just compare pointers
-func (tautology) isNegateOf(atomic) bool {
-	return false
-}
-func (tautology) AsSelector() (string, bool) {
-	return "", false
-}
-
-// tautology is not disjoint to any atomic term
-func (tautology) disjoint(atomic, *Hints) bool {
-	return false
-}
-
-func (tautology) supersetOf(atom atomic, hints *Hints) bool {
-	return atom.IsTautology()
-}
-
 // general atomic functionality
 
 // are two given by name atomicTerms in disjoint list
@@ -61,11 +21,6 @@ func (hints *Hints) disjoint(name1, name2 string) bool {
 
 // functions of Atomic with identical impl of all implementing structs
 
-// IsTautology an atomicTerm is a non empty cond on a group, a tag etc and is thus not a tautology
-func (atomicTerm) IsTautology() bool {
-	return false
-}
-
 func (atomicTerm atomicTerm) isNegation() bool {
 	return atomicTerm.neg
 }
@@ -82,11 +37,20 @@ func isNegateOf(atom, otherAtom atomic) bool {
 // returns true iff otherAtom is disjoint to atom as given by hints
 // todo: could e.g. groups and tags have the same name????
 func disjoint(atom, otherAtom atomic, hints *Hints) bool {
-	// in hints list of disjoint groups/tags/.. is given. Actual atomicTerms are disjoint only if both not negated
-	if atom.isNegation() || otherAtom.isNegation() {
+	atomBlock := atom.getBlock()
+	otherAtomBlock := otherAtom.getBlock()
+	switch {
+	case atomBlock != nil && otherAtomBlock != nil:
+		return atomBlock.Intersect(otherAtomBlock).IsEmpty()
+	case atomBlock != nil || otherAtomBlock != nil:
 		return false
+	default:
+		// in hints list of disjoint groups/tags/.. is given. Actual atomicTerms are disjoint only if both not negated
+		if atom.isNegation() || otherAtom.isNegation() {
+			return false
+		}
+		return hints.disjoint(atom.name(), otherAtom.name())
 	}
-	return hints.disjoint(atom.name(), otherAtom.name())
 }
 
 // returns true iff atom is supersetOf of otherAtom other as given by hints
@@ -97,3 +61,12 @@ func disjoint(atom, otherAtom atomic, hints *Hints) bool {
 func supersetOf(atom, otherAtom atomic, hints *Hints) bool {
 	return hints.disjoint(atom.name(), otherAtom.name()) && atom.isNegation() && !otherAtom.isNegation()
 }
+
+// return equalSignConst or nonEqualSignConst for atom
+func eqSign(atom atomic) string {
+	equalSign := equalSignConst
+	if atom.isNegation() {
+		equalSign = nonEqualSignConst
+	}
+	return equalSign
+}

pkg/synthesis/symbolicexpr/conjunction.go

@@ -2,6 +2,7 @@ package symbolicexpr
 
 import (
 	"github.com/np-guard/vmware-analyzer/internal/common"
+	"github.com/np-guard/vmware-analyzer/pkg/configuration/topology"
 )
 
 const emptySet = "empty set "
@@ -17,7 +18,33 @@ func (c *Conjunction) add(atom atomic) *Conjunction {
 	if c.contains(atom) {
 		return c
 	}
-	res := append(*c, atom)
+	var ipBlockAddedToExisting bool
+	// if c is an IPBlock, adds it to other IPBlock in the Conjunction, if any. Otherwise, just appends it
+	// in the former case we lose the OriginalIP
+	block := atom.getBlock()
+	var res Conjunction
+	if block != nil { // atom is an IPBlockTerm
+		// looks for an  IPBlock in c
+		for _, itemAtom := range *c {
+			itemBlock := itemAtom.getBlock()
+			if itemBlock == nil { // itemAtom not an IPBlock
+				res = append(res, itemAtom)
+			} else {
+				// note that there could be at most one IPBlock in a conjunction, by design
+				// since the Conjunction's items are added, we should intersect the IPBlocks
+				newIPBlockAtomicTerm := &ipBlockAtomicTerm{atomicTerm: atomicTerm{},
+					IPBlock: &topology.IPBlock{Block: block.Intersect(itemBlock)}}
+				res = append(res, newIPBlockAtomicTerm)
+				ipBlockAddedToExisting = true
+			}
+		}
+	}
+	if ipBlockAddedToExisting {
+		return &res
+	}
+	// atom was not an ipBlockTerm or c did not yet have an ipBlockTerm
+	res = append(*c, atom)
+
 	return &res
 }
 
@@ -27,8 +54,12 @@ func (c *Conjunction) copy() *Conjunction {
 	return &newC
 }
 
+// tautology: ipBlock 0.0.0.0/0 or tautology struct; at most 2 items
 func (c *Conjunction) isTautology() bool {
-	if len(*c) == 1 && (*c)[0].IsTautology() {
+	if len(*c) > 2 || len(*c) == 0 || !(*c)[0].IsTautology() {
+		return false
+	}
+	if len(*c) == 1 || (len(*c) == 2 && (*c)[1].IsTautology()) {
 		return true
 	}
 	return false
@@ -55,7 +86,8 @@ func (c *Conjunction) removeRedundant(hints *Hints) Conjunction {
 	return newC
 }
 
-// atomic atom is a redundant in Conjunction c, if it is a superset of one of c's terms
+// atomic atom is a redundant in Conjunction c, if it is a superset of one of c's terms; this applies to tagTerm and
+// groupTerm; as to ipBlockTerm - there is at most one such term which is not redundant by design
 func atomRedundantInConj(atom atomic, c *Conjunction, hints *Hints) bool {
 	if len(*c) == 0 { // nil Conjunction is equiv to tautology
 		return false
@@ -68,13 +100,21 @@ func atomRedundantInConj(atom atomic, c *Conjunction, hints *Hints) bool {
 	return false
 }
 
-// checks whether the conjunction is empty: either syntactically, or contains an groupAtomicTerm and its negation
+// isEmpty: checks whether the conjunction is false:
+// either contains an empty ipBlockTerm
+// or contains groupAtomicTerm and its negation
 // or contains two atoms that are disjoint to each other by hints
-func (c *Conjunction) isEmptySet(hints *Hints) bool {
+func (c *Conjunction) isEmpty(hints *Hints) bool {
 	if len(*c) == 0 {
-		return true
+		return false
 	}
 	for i, outAtomicTerm := range *c {
+		if outAtomicTerm.IsContradiction() {
+			return true
+		}
+		if outAtomicTerm.getBlock() != nil {
+			continue
+		}
 		reminder := *c
 		reminder = reminder[i+1:]
 		for _, inAtomicTerm := range reminder {
@@ -104,12 +144,26 @@ func (c *Conjunction) disjoint(other *Conjunction, hints *Hints) bool {
 	return false
 }
 
+// a Conjunction c contains an atom atomic if:
+// semantically: the condition in atom is already implied by c
+// syntactically:
+// if atom is a tagTerm or a groupTerm, then if the Conjunction c contains the atom literally
+// if atom is an IPBlock, if there is already an IPBlock in c that atom is a superset of it.
 func (c *Conjunction) contains(atom atomic) bool {
-	for _, atomicTerm := range *c {
-		if atomicTerm.String() == (atom).String() {
+	if atom.IsTautology() {
+		return true
+	}
+	for _, atomicItem := range *c {
+		// the following is relevant only when both atom and atomicItem are ipBlockTerms;
+		// in the other cases supersetOf is based on hints
+		if atom.supersetOf(atomicItem, &Hints{}) {
+			return true
+		}
+		if atomicItem.String() == (atom).String() {
 			return true
 		}
 	}
+
 	return false
 }
 
@@ -143,7 +197,8 @@ func (c *Conjunction) isSuperset(other *Conjunction, hints *Hints) bool {
 
 // Conjunction c is a superset of atomic atom if any resource satisfying atom also satisfies c
 // this is the case if each of c's term is a superset of atom
-// e.g., given that Slytherin and Hufflepuff are disjoint, group != Hufflepuff is a superset of group = Slytherin
+// e.g.,  1.2.1.0/8 is a superset of 1.2.1.0/16;
+// given that Slytherin and Hufflepuff are disjoint, group != Hufflepuff is a superset of group = Slytherin
 func conjSupersetOfAtom(c *Conjunction, atom atomic, hints *Hints) bool {
 	if len(*c) == 0 { // nil Conjunction is equiv to tautology
 		return false

pkg/synthesis/symbolicexpr/contradiction.go

@@ -0,0 +1,51 @@
+package symbolicexpr
+
+import "github.com/np-guard/models/pkg/netset"
+
+// contradiction implementation; contradiction is the negation of tautology
+
+func (contradiction) String() string {
+	return "empty set"
+}
+
+func (contradiction) name() string {
+	return ""
+}
+
+func (contradiction) negate() atomic {
+	return tautology{}
+}
+
+func (contradiction) isNegation() bool {
+	return false
+}
+
+func (contradiction) IsTautology() bool {
+	return false
+}
+
+func (contradiction) IsContradiction() bool {
+	return true
+}
+
+// returns true iff otherAt is negation of
+// once we cache the atomic terms, we can just compare pointers
+func (contradiction) isNegateOf(atom atomic) bool {
+	return atom.IsTautology()
+}
+func (contradiction) AsSelector() (string, bool) {
+	return "", false
+}
+
+// contradiction is disjoint to any atomic term
+func (contradiction) disjoint(atomic, *Hints) bool {
+	return true
+}
+
+func (contradiction) supersetOf(atom atomic, hints *Hints) bool {
+	return false
+}
+
+func (contradiction) getBlock() *netset.IPBlock {
+	return nil
+}

pkg/synthesis/symbolicexpr/groupTerm.go

@@ -3,6 +3,7 @@ package symbolicexpr
 import (
 	"fmt"
 
+	"github.com/np-guard/models/pkg/netset"
 	"github.com/np-guard/vmware-analyzer/pkg/collector"
 	"github.com/np-guard/vmware-analyzer/pkg/logging"
 )
@@ -12,11 +13,17 @@ const equalSignConst = " = "
 const nonEqualSignConst = " != "
 
 func (groupTerm groupAtomicTerm) String() string {
-	equalSign := equalSignConst
-	if groupTerm.neg {
-		equalSign = nonEqualSignConst
-	}
-	return grp + equalSign + groupTerm.name()
+	return grp + eqSign(groupTerm) + groupTerm.name()
+}
+
+// IsTautology false since an groupAtomicTerm is a non-empty cond on a group
+func (groupAtomicTerm) IsTautology() bool {
+	return false
+}
+
+// IsContradiction false since an groupAtomicTerm is a non-empty cond on a group
+func (groupAtomicTerm) IsContradiction() bool {
+	return false
 }
 
 func (groupTerm groupAtomicTerm) AsSelector() (string, bool) {
@@ -82,3 +89,7 @@ func (groupTerm groupAtomicTerm) disjoint(otherAtom atomic, hints *Hints) bool {
 func (groupTerm groupAtomicTerm) supersetOf(otherAtom atomic, hints *Hints) bool {
 	return supersetOf(groupTerm, otherAtom, hints)
 }
+
+func (groupAtomicTerm) getBlock() *netset.IPBlock {
+	return nil
+}