procedure summaries crash

[utting]

Procedure summary generation crashes on the hlist_mod function of cntlm_noduk.

This happens in the main branch and also in branch wpdual-fix

The error (using wpdual-fix branch) is:

% ./mill run -i ../cntlm/cntlm_noduk.gtirb --lifter --summarise-procedures -o ../cntlm/basil_procsummary_wpdual-fix.bpl     
[279/279] run
[279] [INFO]   Basil
[279]          Version: 0.1.2-alpha-1105-gaf237ff53
[279]          Commit:  af237ff537c1a8b395f46777214965d2b88e8a42
[279] [INFO]   [!] Loading Program
[279] [INFO]   [!] Using ELF data from GTIRB: ../cntlm/cntlm_noduk.gtirb
[279] [INFO]   [!] Removed all PC-related statements
[279] [INFO]   [!] Typecheck Passed
[279] [INFO]   [!] Removing external function calls
[279] [INFO]   [!] Removed unreachable blocks
[279] [INFO]   [!] Typecheck Passed
[279] [INFO]   [!] Generating Procedure Summaries
[279] Exception in thread "main" java.lang.Exception: Expected to be able to construct predicate for: boolnot(var1_4238980_bool:bool)
[279] 	at analysis.GammaDomains$package$.expectPredicate(GammaDomains.scala:199)
[279] 	at analysis.WpDualDomain.transfer(GammaDomains.scala:246)
[279] 	at analysis.WpDualDomain.transfer(GammaDomains.scala:220)
[279] 	at ir.transforms.worklistSolver.$anonfun$7$$anonfun$1(AbsInt.scala:222)
[279] 	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
[279] 	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
[279] 	at scala.collection.immutable.List.foldLeft(List.scala:79)
[279] 	at ir.transforms.worklistSolver.$anonfun$7(AbsInt.scala:222)
[279] 	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
[279] 	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
[279] 	at scala.collection.immutable.List.foldLeft(List.scala:79)
[279] 	at ir.transforms.worklistSolver.solve(AbsInt.scala:218)
[279] 	at ir.transforms.worklistSolver.solveProc(AbsInt.scala:149)
[279] 	at analysis.InterprocSummaryGenerator.transfer(SummaryGenerator.scala:95)
[279] 	at analysis.SummaryGenerator.$init$$$anonfun$3(SummaryGenerator.scala:180)
[279] 	at ir.transforms.SCCCallgraphWorklistSolver.solve$$anonfun$7(AbsInt.scala:367)
[279] 	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
[279] 	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
[279] 	at scala.collection.immutable.List.foreach(List.scala:334)
[279] 	at ir.transforms.SCCCallgraphWorklistSolver.solve(AbsInt.scala:355)
[279] 	at analysis.SummaryGenerator.<init>(SummaryGenerator.scala:180)
[279] 	at analysis.SummaryGenerator$package$.getGenerateProcedureSummariesTransform$$anonfun$1(SummaryGenerator.scala:222)
[279] 	at ir.transforms.Transform.apply(Transform.scala:99)
[279] 	at util.RunUtils$.loadAndTranslate(RunUtils.scala:152)
[279] 	at util.RunUtils$.run(RunUtils.scala:37)
[279] 	at Main$.$anonfun$15(Main.scala:481)
[279] 	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
[279] 	at gtirb.GTIRBReadELF$.withWarnings(GTIRBReadELF.scala:246)
[279] 	at Main$.main(Main.scala:482)
[279] 	at Main.main(Main.scala)

A previous run (using main branch) with logging enabled shows:
...
[279] [DEBUG] Generating gamma with reachability preconditions for @hlist_mod_4214384 [transfer@SummaryGenerator.scala:46]
[279] [DEBUG] Generating mini wp preconditions for @hlist_mod_4214384 [transfer@SummaryGenerator.scala:93]
[279] Exception in thread "main" java.lang.Exception: Expected to be able to construct predicate for: boolnot(var1_4214540_bool:bool)
[279] at analysis.GammaDomains$package$.expectPredicate(GammaDomains.scala:199)
[279] at analysis.WpDualDomain.transfer(GammaDomains.scala:246)
[279] at analysis.WpDualDomain.transfer(GammaDomains.scala:220)
...

The code for hlist_mod is:

/*
 * Change the value of a key. If add is true, we store it in the
 * list if the key is not found. Unlike hlist_add, which offers
 * pointer storage or memory duplication for both the key and the
 * value separately, hlist_mod always duplicates.
 *
 * Used to add a header, which might already be present.
 */
hlist_t hlist_mod(hlist_t list, char *key, char *value, int add) {
	hlist_t t = list;

	while (t) {
		if (!strcasecmp(t->key, key))
			break;
		t = t->next;
	}

	if (t) {
		free(t->value);
		t->value = strdup(value);
	} else if (add) {
		list = hlist_add(list, key, value, HLIST_ALLOC, HLIST_ALLOC);
	}

	return list;
}

This code was compiled with aarch64-linux-gnu-gcc -O3

[b-paul]

I'm not able to easily replicate this issue on my machine but from the error indicates that there was a form of expression in an assume that isn't handled. I've pushed a change where predicates that can't be read just go to top, but it seems in my testing that there's another issue running cntlm without --simplify where a domain doesn't terminate (it does terminate with --simplify at least on the example in ./examples/cnltm-noduk). I think the issue comes from an incorrect widening on the bounded disjunctive completion domain.

Would you be able to run this example on the latest commit of wpdual-fix?

[utting]

Yes, with that latest commit it goes into a loop for 1/2 an hour or more printing these lines repeatedly:
./mill run -i ../cntlm/cntlm_noduk.gtirb --lifter --summarise-procedures -o ../cntlm/basil_procsummary_wpdual-fix2.bpl
[279] [WARN] Large join count on block memxor_85, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_83, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_81, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_79, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_77, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_75, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_73, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_71, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_69, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_85, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_83, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_81, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_79, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_77, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_75, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_73, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_71, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_69, no fix point? (-v for more info) [solve@AbsInt.scala:233]
[279] [WARN] Large join count on block memxor_85, no fix point? (-v for more info) [solve@AbsInt.scala:233]

I killed it after 1/2 an hour.

[b-paul]

I think this is happening because reducibleloops isn't being run and so loop headers aren't being annotated (hence no widening points). Perhaps procedure summaries should depend on reducible loops too...

[utting]

I've tried it again (in the main branch, after your merge of "Wpdual fix (#593)").
I ran it with the --transform-irreducible-loops flag added.
And also with both --dsa= and --transform-irreducible-loops flags.
E.g. ./mill run -i ../cntlm/cntlm_noduk_191.gtirb --dsa= --generate-procedure-summaries

But I get the same infinite looping printing behaviour in both cases.
("Large join count on block phi_27, no fix point?" and similar messages)

[b-paul]

This should be resolved in #597