Fix check on negated alternatives

[marvinvo]

How does the check work?

CrySL required preds will be stored as CrySLConstraints. The ConstraintSolvers will convert required CrySLConstraints to AlternativeReqPredicates, see here

CryptoAnalysis/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java

Line 111 in 35d0916

requiredPredicates.add(collectAlternativePredicates((CrySLConstraint) cons, null));

All required preds, also the AlternativeReqPredicates, will be used to check wether a AnalysisSeedWithSpecification satisfies its required predicates or not in the checkPredicates() method.

CryptoAnalysis/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java

Line 377 in 35d0916

for (ISLConstraint con : constraintSolver.getRequiredPredicates()) {

What is the issue?

Checking on an AlternativeReqPredicate with all alternative predicates negated - keep in mind that they are connected with a logical or - is done by returning false (false = predicates does not satisfy constraints) if only one negated alternative predicate is ensured by the seed.
That is wrong, because it should actually satisfy its constraints, if at least one negated alternative predicate is not ensured, since they are connected with a logical or.

This needs to be testet first

Current tests does not cover this code, so someone should write tests before merging.

[marvinvo]

It's a wrong fix I did there, should be more like:

if (negatives.size() == alternatives.size()) {
	if (alternatives.parallelStream().allMatch(e -> e is in list of ensured predicates) {
	    return false;			
	}
}

[AnakinRaW]

@marvinvo
Could you please write some tests?
Negative and positive tests please!

Also, could you please look into #265 and it's liked issue. It this a duplicate?

[marvinvo]

Here a little update:
I created a rule as follows:

SPEC java.security.SecureRandom

OBJECTS 
	byte[] seed;
	byte[] next;
	
EVENTS
	c1: SecureRandom();
	Cons := c1;

	nB: nextBytes(next);
	Ends := nB;

ORDER
	Cons, Ends*
 	
REQUIRES	
	!test[next] || !test2[next];
	
ENSURES
	test[next] after Ends;

The assertion code

SecureRandom sr = new SecureRandom();
byte[] genSeed = new byte[32];
sr.nextBytes(genSeed); // this ensured genSeed as test
Assertions.hasEnsuredPredicate(genSeed);
SecureRandom sr2 = new SecureRandom();
sr2.nextBytes(genSeed); 
// genSeed should be either !test or !test2
// since test2 was nowhere ensured, the result should throw no errors
Assertions.errorCount(0);

does not throw any errors, which is weird in my eyes. So I started debugging and it turns out, that the error is catched by an if statement at this line:

CryptoAnalysis/CryptoAnalysis/src/main/java/crypto/predicates/PredicateHandler.java

Line 233 in 35d0916

if (!rule.getPredicates().parallelStream().anyMatch(e -> missingPred.getPred().getPredName().equals(e.getPredName()) && missingPred.getPred().getParameters().get(0).equals(e.getParameters().get(0)))) {

Is there a reason why it should throw now errors if a predicate is missed but could be ensured by the rule?

I'm still convinced that this is an issue, but it may need a larger test with at least two rules to get over this if statement..

[AnakinRaW]

scheduled for 2.8

[smeyer198]

A fix and tests have been added in #376. Therefore, this PR is not required anymore