Loop Unrolling for the first exp.unrolling-factor Iterations

[mikcp]

Implementation of the loop unrolling functionality.

• exp.unrolling-factor is 0 by default, case in which the unrolling does not take place.
• if exp.unrolling-factor>0, all loops will be unrolled factor times.

This is the first part of a precision optimization. Unrolling the loop's body k times outside the loop, will allow us to see those k iterations more precisely.

[michael-schwarz]

Could you maybe also add tests for this feature?

One should be able to observe a precision increase for some programs even without the modified array domain.
E.g. programs where Goblint is newly able to show precise asserts about a variable that is modified in the loop other than the ones used in the loop head, provided the loop goes through less iterations than exp.unrolling-factor?

[michael-schwarz]

I just started another sv-comp run with an unrolling of 5. If there are no abnormalities there, I think we can merge this.

[sim642]

If there are no abnormalities there, I think we can merge this.

I would still be hesitant about that, regarding the unresolved points above. Not handling gotos like copyFunctionVisitor in unrolled loops could be very problematic, it might not just show as unsoundness on sv-benchmarks.
Also duplicating the functionality of prepareCFG and this not working right when relying on prepareCFG instead is again quite suspicious. It could also be related to the gotos that prepareCFG introduces.

[sim642]

I just started another sv-comp run with an unrolling of 5.

Also, this is a bit laughable considering Frama-C-SV used loop unrolling of 1024 according to their tool paper.

[michael-schwarz]

A run with an unrolling of 5 reveals ~48 cases where Goblint now succeeds (including these product-lines/elevator_spec13_product23.cil.yml like tasks), and ~33 cases where we newly fail.

An interesting class of programs for which we newly fail contain loops of the flavor:

int main()
{
	int current_execution_context;
	unsigned short random;

	do
	{
		random = __VERIFIER_nondet_ushort();

		switch (random)
		{
		case 1:
			current_execution_context = 1;

			break;

		default:
			break;
		}
	} while (random);
}

Without unrolling, everything works. With it Goblint fails with:

Fatal error: exception Failure("MyCFG.createCFG.find_real_stmt: >1 succ")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from CfgTools.createCFG.find_real_stmt in file "src/framework/cfgTools.ml", line 230, characters 14-44
Called from Stdlib__list.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39
Called from CfgTools.createCFG.(fun).handle in file "src/framework/cfgTools.ml", line 309, characters 48-61
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from CfgTools.createCFG.(fun) in file "src/framework/cfgTools.ml", line 383, characters 8-37
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from Cil.iterGlobals in file "src/cil.ml", line 5635, characters 2-29
Called from CfgTools.createCFG in file "src/framework/cfgTools.ml", line 239, characters 2-1023
Called from CfgTools.getCFG in file "src/framework/cfgTools.ml", line 593, characters 19-33
Called from Control.compute_cfg in file "src/framework/control.ml", line 671, characters 19-39
Called from Control.analyze in file "src/framework/control.ml", line 682, characters 21-37
Called from Maingoblint.do_analyze.do_all_phases.do_one_phase in file "src/maingoblint.ml", line 357, characters 12-48
Re-raised at Maingoblint.do_analyze.do_all_phases.do_one_phase in file "src/maingoblint.ml", line 366, characters 10-51
Called from BatEnum.iter.loop in file "src/batEnum.ml", line 315, characters 4-16
Called from BatEnum.iter in file "src/batEnum.ml", line 319, characters 4-10
Called from Maingoblint.do_analyze.do_all_phases in file "src/maingoblint.ml", line 378, characters 16-68
Called from Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 106, characters 10-15
Re-raised at Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 110, characters 1-8
Called from Maingoblint.main in file "src/maingoblint.ml", line 510, characters 6-34
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 554, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 560, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20

Any idea what's happening there @mikcp?

[michael-schwarz]

The corresponding tables if anyone is interested:
default-vs-unroll5-2min-all.zip

[michael-schwarz]

More natural example of the same issue

int main(void) {
	for (int i = 0; i < 2; ++i) {
		switch (i) {
		case 0:
			break;
		case 1:
		}
	}

	return 0;
}

[sim642]

I wouldn't be the least surprised if the crash was due to the lacking goto handling, because the invariants here come from CIL itself:

analyzer/src/framework/cfgTools.ml

Lines 195 to 209 in a0bb640

	| Goto _ (* 1 succ *)
	| Instr [] (* CIL inserts like unlabelled goto, 0-1 succs *)
	| Block _ (* just container for stmts, 0-1 succs *)
	| Loop _ -> (* just container for (prepared) body, 1 succ *)
	begin match stmt.succs with
	| [] ->
	if not_found then
	raise Not_found
	else
	stmt
	| [next] ->
	find (stmt.sid :: visited_sids) next
	| _ -> (* >1 succ *)
	failwith "MyCFG.createCFG.find_real_stmt: >1 succ"
	end

If the AST is additionally screwed with without maintaining those, things are bound to be wrong.

[michael-schwarz]

I have now re-implemented it. They key idea now is: We still do the transformation before prepareCfg to avoid complicated reasoning about which gotos were originally gotos and which gotos correspond to loop control structures and hence need to be modified in some way and maintaining preds and succs correctly.

This comes at the price of putting each replicated body into a fake while(1) loop, inserting an appropriate break at the end of the replicated bodies and patching all top-level continues to be breaks. Apart from that we remove all labels from the unrolled loop, getting rid of issues with duplicate labels and trivially ensuring correctness of jumps by always jumping into the non-unrolled part.

The resulting C code after the transformation is a bit ugly, but the unnecessary loops will hopefully not lead to widening as there is no back edge, and the OCaml code is cleaner than the approach originally taken for the thesis.

[michael-schwarz]

Ok, I made one (hopefully last) rewrite. Now, it no longer inserts pointless loops but instead simply replaces top-level break and continue with appropriate gotos for the unrolled iterations.

Also, I discovered that in order to benefit from switches in unrolled loops, one needs to do more with labels. We now replace all labels with fresh labels, remembering the old and the new statement. Then, once we are done copying and renaming labels, we path all gotos that are internal to the unrolling under consideration to refer to the new copy of the label.

That way, all external gotos still go into the non-unrolled code, but gotos that are within one iteration of the loop stay so.