Add essential missing sanity check on primitive inputs

cmd/vplogic/attackerstate.go

@@ -65,7 +65,7 @@ func attackerStateAbsorbPhaseValues(valPrincipalState *PrincipalState) error {
 				attackerStateShared.PrincipalState, valPrincipalStateClone,
 			)
 		}
-		aa, _, err := valueResolveValueInternalValuesFromPrincipalState(
+		aa, err := valueResolveValueInternalValuesFromPrincipalState(
 			a, a, i, valPrincipalState, attackerStateShared, true,
 		)
 		if err != nil {

cmd/vplogic/mutationmap.go

@@ -19,6 +19,7 @@ func mutationMapInit(
 		Mutations:      [][]*Value{},
 		Combination:    []*Value{},
 		DepthIndex:     []int{},
+		Worthwhile:     false,
 		OutOfMutations: false,
 	}
 	InfoMessage(fmt.Sprintf(
@@ -147,7 +148,7 @@ func mutationMapReplacePrimitive(
 				}
 			}
 		case typesEnumPrimitive:
-			a, _, err = valueResolveValueInternalValuesFromPrincipalState(
+			a, err = valueResolveValueInternalValuesFromPrincipalState(
 				a, a, rootIndex, valPrincipalState, valAttackerState, false,
 			)
 			if err != nil {
@@ -205,11 +206,15 @@ func mutationMapReplaceEquation(
 }
 
 func mutationMapNext(valMutationMap MutationMap) MutationMap {
+	valMutationMap.Worthwhile = false
 	if len(valMutationMap.Combination) == 0 {
 		valMutationMap.OutOfMutations = true
 		return valMutationMap
 	}
 	for i := 0; i < len(valMutationMap.Combination); i++ {
+		if i >= valMutationMap.LastIncrement {
+			valMutationMap.Worthwhile = true
+		}
 		valMutationMap.Combination[i] = valMutationMap.Mutations[i][valMutationMap.DepthIndex[i]]
 		if i != len(valMutationMap.Combination)-1 {
 			continue

cmd/vplogic/sanity.go

@@ -170,7 +170,7 @@ func sanityPrimitive(p *Primitive, outputs []*Constant) error {
 	if p.Check && !check {
 		return fmt.Errorf("primitive is checked but does not support checking")
 	}
-	return nil
+	return sanityCheckPrimitiveArgumentOutputs(p)
 }
 
 func sanityQueries(m Model, valKnowledgeMap *KnowledgeMap) error {
@@ -381,6 +381,37 @@ func sanityFailOnFailedCheckedPrimitiveRewrite(failedRewrites []*Primitive) erro
 	return nil
 }
 
+func sanityCheckPrimitiveArgumentOutputs(p *Primitive) error {
+	for i := 0; i < len(p.Arguments); i++ {
+		switch p.Arguments[i].Kind {
+		case typesEnumPrimitive:
+			var output []int
+			if primitiveIsCorePrim(p.Arguments[i].Data.(*Primitive).ID) {
+				prim, err := primitiveCoreGet(p.Arguments[i].Data.(*Primitive).ID)
+				if err != nil {
+					return err
+				}
+				output = prim.Output
+			} else {
+				prim, err := primitiveGet(p.Arguments[i].Data.(*Primitive).ID)
+				if err != nil {
+					return err
+				}
+				output = prim.Output
+			}
+			if !intInSlice(1, output) {
+				return fmt.Errorf(
+					"primitive %s cannot have %s as an argument, since %s necessarily produces more than one output",
+					prettyPrimitive(p),
+					prettyPrimitive(p.Arguments[i].Data.(*Primitive)),
+					prettyPrimitive(p.Arguments[i].Data.(*Primitive)),
+				)
+			}
+		}
+	}
+	return nil
+}
+
 func sanityCheckEquationRootGenerator(e *Equation) error {
 	if len(e.Values) > 3 {
 		return fmt.Errorf(

cmd/vplogic/types.go

@@ -325,6 +325,7 @@ type MutationMap struct {
 	Constants      []*Constant
 	Mutations      [][]*Value
 	Combination    []*Value
+	Worthwhile     bool
 	DepthIndex     []int
 }
 

cmd/vplogic/value.go

@@ -550,16 +550,12 @@ func valueResolveEquationInternalValuesFromKnowledgeMap(
 func valueResolveValueInternalValuesFromPrincipalState(
 	a *Value, rootValue *Value, rootIndex int, valPrincipalState *PrincipalState,
 	valAttackerState AttackerState, forceBeforeMutate bool,
-) (*Value, []*Value, error) {
-	var v []*Value
+) (*Value, error) {
 	switch a.Kind {
 	case typesEnumConstant:
-		if valueEquivalentValueInValues(a, v) < 0 {
-			v = append(v, a)
-		}
 		nextRootIndex := valueGetPrincipalStateIndexFromConstant(valPrincipalState, a.Data.(*Constant))
 		if nextRootIndex < 0 {
-			return &Value{}, []*Value{}, errors.New("invalid index")
+			return &Value{}, errors.New("invalid index")
 		}
 		switch nextRootIndex {
 		case rootIndex:
@@ -597,23 +593,23 @@ func valueResolveValueInternalValuesFromPrincipalState(
 	}
 	switch a.Kind {
 	case typesEnumConstant:
-		return a, v, nil
+		return a, nil
 	case typesEnumPrimitive:
 		return valueResolvePrimitiveInternalValuesFromPrincipalState(
-			a, v, rootValue, rootIndex, valPrincipalState, valAttackerState, forceBeforeMutate,
+			a, rootValue, rootIndex, valPrincipalState, valAttackerState, forceBeforeMutate,
 		)
 	case typesEnumEquation:
 		return valueResolveEquationInternalValuesFromPrincipalState(
-			a, v, rootValue, rootIndex, valPrincipalState, valAttackerState, forceBeforeMutate,
+			a, rootValue, rootIndex, valPrincipalState, valAttackerState, forceBeforeMutate,
 		)
 	}
-	return a, v, nil
+	return a, nil
 }
 
 func valueResolvePrimitiveInternalValuesFromPrincipalState(
-	a *Value, v []*Value, rootValue *Value, rootIndex int, valPrincipalState *PrincipalState,
+	a *Value, rootValue *Value, rootIndex int, valPrincipalState *PrincipalState,
 	valAttackerState AttackerState, forceBeforeMutate bool,
-) (*Value, []*Value, error) {
+) (*Value, error) {
 	if valPrincipalState.Creator[rootIndex] == valPrincipalState.ID {
 		forceBeforeMutate = false
 	}
@@ -627,27 +623,22 @@ func valueResolvePrimitiveInternalValuesFromPrincipalState(
 		},
 	}
 	for i := 0; i < len(a.Data.(*Primitive).Arguments); i++ {
-		s, vv, err := valueResolveValueInternalValuesFromPrincipalState(
+		s, err := valueResolveValueInternalValuesFromPrincipalState(
 			a.Data.(*Primitive).Arguments[i], rootValue, rootIndex, valPrincipalState,
 			valAttackerState, forceBeforeMutate,
 		)
 		if err != nil {
-			return &Value{}, []*Value{}, err
+			return &Value{}, err
 		}
 		r.Data.(*Primitive).Arguments = append(r.Data.(*Primitive).Arguments, s)
-		for _, vvv := range vv {
-			if valueEquivalentValueInValues(vvv, v) < 0 {
-				v = append(v, vvv)
-			}
-		}
 	}
-	return r, v, nil
+	return r, nil
 }
 
 func valueResolveEquationInternalValuesFromPrincipalState(
-	a *Value, v []*Value, rootValue *Value, rootIndex int, valPrincipalState *PrincipalState,
+	a *Value, rootValue *Value, rootIndex int, valPrincipalState *PrincipalState,
 	valAttackerState AttackerState, forceBeforeMutate bool,
-) (*Value, []*Value, error) {
+) (*Value, error) {
 	r := &Value{
 		Kind: typesEnumEquation,
 		Data: &Equation{
@@ -667,53 +658,37 @@ func valueResolveEquationInternalValuesFromPrincipalState(
 			if forceBeforeMutate {
 				aa[aai] = valPrincipalState.BeforeMutate[i]
 			}
-			if valueEquivalentValueInValues(aa[aai], v) < 0 {
-				v = append(v, aa[aai])
-			}
 		}
 	}
 	for aai := range aa {
 		switch aa[aai].Kind {
 		case typesEnumConstant:
 			r.Data.(*Equation).Values = append(r.Data.(*Equation).Values, aa[aai])
-			if valueEquivalentValueInValues(aa[aai], v) < 0 {
-				v = append(v, aa[aai])
-			}
 		case typesEnumPrimitive:
-			aaa, vv, err := valueResolvePrimitiveInternalValuesFromPrincipalState(
-				aa[aai], v, rootValue, rootIndex,
+			aaa, err := valueResolvePrimitiveInternalValuesFromPrincipalState(
+				aa[aai], rootValue, rootIndex,
 				valPrincipalState, valAttackerState, forceBeforeMutate,
 			)
 			if err != nil {
-				return &Value{}, []*Value{}, err
+				return &Value{}, err
 			}
 			r.Data.(*Equation).Values = append(r.Data.(*Equation).Values, aaa)
-			for _, vvv := range vv {
-				if valueEquivalentValueInValues(vvv, v) < 0 {
-					v = append(v, vvv)
-				}
-			}
 		case typesEnumEquation:
-			aaa, vv, err := valueResolveEquationInternalValuesFromPrincipalState(
-				aa[aai], v, rootValue, rootIndex,
+			aaa, err := valueResolveEquationInternalValuesFromPrincipalState(
+				aa[aai], rootValue, rootIndex,
 				valPrincipalState, valAttackerState, forceBeforeMutate,
 			)
 			if err != nil {
-				return &Value{}, []*Value{}, err
+				return &Value{}, err
 			}
 			if aai == 0 {
 				r.Data.(*Equation).Values = aaa.Data.(*Equation).Values
 			} else {
 				r.Data.(*Equation).Values = append(r.Data.(*Equation).Values, aaa.Data.(*Equation).Values[1:]...)
 			}
-			for _, vvv := range vv {
-				if valueEquivalentValueInValues(vvv, v) < 0 {
-					v = append(v, vvv)
-				}
-			}
 		}
 	}
-	return r, v, nil
+	return r, nil
 }
 
 func valueConstantIsUsedByPrincipalInKnowledgeMap(
@@ -744,14 +719,14 @@ func valueResolveAllPrincipalStateValues(
 	var err error
 	valPrincipalStateClone := constructPrincipalStateClone(valPrincipalState, false)
 	for i := range valPrincipalState.Assigned {
-		valPrincipalStateClone.Assigned[i], _, err = valueResolveValueInternalValuesFromPrincipalState(
+		valPrincipalStateClone.Assigned[i], err = valueResolveValueInternalValuesFromPrincipalState(
 			valPrincipalState.Assigned[i], valPrincipalState.Assigned[i], i, valPrincipalState,
 			valAttackerState, valueShouldResolveToBeforeMutate(i, valPrincipalState),
 		)
 		if err != nil {
 			return &PrincipalState{}, err
 		}
-		valPrincipalStateClone.BeforeRewrite[i], _, err = valueResolveValueInternalValuesFromPrincipalState(
+		valPrincipalStateClone.BeforeRewrite[i], err = valueResolveValueInternalValuesFromPrincipalState(
 			valPrincipalState.BeforeRewrite[i], valPrincipalState.BeforeRewrite[i], i, valPrincipalState,
 			valAttackerState, valueShouldResolveToBeforeMutate(i, valPrincipalState),
 		)
@@ -767,7 +742,7 @@ func valueContainsFreshValues(
 	valPrincipalState *PrincipalState, valAttackerState AttackerState,
 ) (bool, error) {
 	i := valueGetPrincipalStateIndexFromConstant(valPrincipalState, c)
-	v, _, err := valueResolveValueInternalValuesFromPrincipalState(
+	v, err := valueResolveValueInternalValuesFromPrincipalState(
 		v, v, i, valPrincipalState, valAttackerState, false,
 	)
 	if err != nil {
@@ -822,17 +797,3 @@ func valueDeepCopy(v *Value) Value {
 	}
 	return d
 }
-
-func valueNestedConstantInResolvedValue(
-	c *Constant, a *Value,
-	valPrincipalState *PrincipalState, valAttackerState AttackerState,
-) bool {
-	i := valueGetPrincipalStateIndexFromConstant(valPrincipalState, c)
-	_, v, _ := valueResolveValueInternalValuesFromPrincipalState(
-		a, a, i, valPrincipalState, valAttackerState, true,
-	)
-	return valueEquivalentValueInValues(&Value{
-		Kind: typesEnumConstant,
-		Data: c,
-	}, v) >= 0
-}

cmd/vplogic/verify.go

@@ -14,9 +14,11 @@ import (
 // Verify runs the main verification engine for Verifpal on a model loaded from a file.
 // It returns a slice of verifyResults and a "results code".
 func Verify(filePath string) ([]VerifyResult, string, error) {
-	// f, _ := os.Create("cpu.pprof")
-	// pprof.StartCPUProfile(f)
-	// defer pprof.StopCPUProfile()
+	/*
+		f, _ := os.Create("cpu.pprof")
+		pprof.StartCPUProfile(f)
+		defer pprof.StopCPUProfile()
+	*/
 	m, err := libpegParseModel(filePath, true)
 	if err != nil {
 		return []VerifyResult{}, "", err

cmd/vplogic/verifyactive.go

@@ -90,11 +90,10 @@ func verifyActiveScan(
 		scanGroup.Done()
 		return err
 	}
-	valPrincipalStateClone := constructPrincipalStateClone(valPrincipalState, true)
-	valPrincipalStateMutated, isWorthwhileMutation := verifyActiveMutatePrincipalState(
-		valPrincipalStateClone, valAttackerState, valMutationMap,
-	)
-	if isWorthwhileMutation {
+	if valMutationMap.Worthwhile {
+		valPrincipalStateMutated := verifyActiveMutatePrincipalState(
+			constructPrincipalStateClone(valPrincipalState, true), valAttackerState, valMutationMap,
+		)
 		scanGroup.Add(1)
 		go func() {
 			err = verifyAnalysis(
@@ -124,12 +123,12 @@ func verifyActiveScan(
 
 func verifyActiveMutatePrincipalState(
 	valPrincipalState *PrincipalState, valAttackerState AttackerState, valMutationMap MutationMap,
-) (*PrincipalState, bool) {
-	isWorthwhileMutation := false
+) *PrincipalState {
+MutationLoop:
 	for i := 0; i < len(valMutationMap.Constants); i++ {
 		ai, ii := valueResolveConstant(valMutationMap.Constants[i], valPrincipalState)
 		ac := valMutationMap.Combination[i]
-		ar, _, _ := valueResolveValueInternalValuesFromPrincipalState(
+		ar, _ := valueResolveValueInternalValuesFromPrincipalState(
 			ai, ai, ii, valPrincipalState, valAttackerState, true,
 		)
 		switch ar.Kind {
@@ -152,24 +151,22 @@ func verifyActiveMutatePrincipalState(
 				ac.Data.(*Primitive).Output = ar.Data.(*Primitive).Output
 				ac.Data.(*Primitive).Check = ar.Data.(*Primitive).Check
 			}
+			acc := valueGetConstantsFromValue(ac)
+			for acci := 0; acci < len(acc); acci++ {
+				if acc[acci].ID == valMutationMap.Constants[i].ID {
+					continue MutationLoop
+				}
+			}
 		}
 		switch {
 		case valueEquivalentValues(ac, ar, true):
 			continue
-		case valueNestedConstantInResolvedValue(valMutationMap.Constants[i], ac, valPrincipalState, valAttackerState):
-			continue
 		}
 		valPrincipalState.Creator[ii] = principalNamesMap["Attacker"]
 		valPrincipalState.Sender[ii] = principalNamesMap["Attacker"]
 		valPrincipalState.Mutated[ii] = true
 		valPrincipalState.Assigned[ii] = ac
 		valPrincipalState.BeforeRewrite[ii] = ac
-		if i >= valMutationMap.LastIncrement {
-			isWorthwhileMutation = true
-		}
-	}
-	if !isWorthwhileMutation {
-		return valPrincipalState, isWorthwhileMutation
 	}
 	valPrincipalState, _ = valueResolveAllPrincipalStateValues(valPrincipalState, valAttackerState)
 	failedRewrites, failedRewriteIndices, valPrincipalState := valuePerformAllRewrites(valPrincipalState)
@@ -197,7 +194,7 @@ FailedRewritesLoop:
 			}
 		}
 	}
-	return valPrincipalState, isWorthwhileMutation
+	return valPrincipalState
 }
 
 func verifyActiveDropPrincipalStateAfterIndex(valPrincipalState *PrincipalState, f int) *PrincipalState {