dead code does not propagate through previously live loops?

[vogler]

There's a theoretical issue with our constraints for loops that Helmut mentioned which might be worth thinking about.
The problem is that we just join all incoming edges at the loop head which may be a problem if there is some value > bot from the back-edge from inside the loop and bot from the initial edge.
If a loop is first live, but then after narrowing the initial edge to the nested loop becomes dead, it won't propagate bot, but join it with the back-edge.
The rhs for a loop should be strict for the initial edge a, i.e., if is_bot a then a else join a b where b is the value of the back edge.

The question is whether this can happen at all.
I tried to come up with an example for loops but couldn't find one -- maybe because Base.invariant always limits the values.

If it can occur, the other question is how to improve it.
Constraints.FromSpec().tf_loop would have to consider a loop head with two incoming edges and make the join left-strict.
Problem: currently these generate a constraint for each edge of a node which are only afterwards joined into equations by Generic.SimpleSysConverter.
Also, one would have to think about loops that have jumps into them with goto (I guess you'd have to also identify all incoming edges into the loop body as initial).

[sim642]

Constraints.FromSpec().tf_loop

I think this tf_loop has nothing to do with CIL's Loop, but instead means the interrupt self-loops.

It calls the intrpt (interrupt?) function of a Spec:

analyzer/src/framework/constraints.ml

Lines 599 to 601 in 8a74107

	let tf_loop var edge prev_node getl sidel getg sideg d =
	let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
	common_join ctx (S.intrpt ctx) !r !spawns

It is called for SelfLoop edges:

analyzer/src/framework/constraints.ml

Line 718 in 8a74107

| SelfLoop -> tf_loop var edge prev_node

These should correspond to interrupts:

analyzer/src/framework/myCFG.ml

Lines 39 to 40 in 8a74107

	| SelfLoop
	(** This for interrupt edges.! *)

But this doesn't really matter if this issue cannot actually happen. Although it might still be worth renaming some of those things to make it very clear they're just about interrupts.

[vogler]

Ah, ok, good to know, so it's just tf_test then.

@michael-schwarz and @jerhard came up with an example that fails for solvers that work in phases (for the whole program):

//PARAM: --disable ana.int.def_exc --enable ana.int.interval --sets solver slr3tp

int g = 0;

int main() {
  int x;

  for(x=0; x < 50; x++){
    g = 1;
  }
  // x = [50, 50] after narrow
  if(x>50){ // live after widen, but dead after narrow
    // node after Pos(x>50) is marked dead at the end
    // but the loop is not with x = [51,2147483647]
    for(int i=0; i<=0; i--){
      g = 57;
    }
  }
}

This is not a problem with td3 since it switches to narrowing after the first loop and only then continues with widening for the rest.

[jerhard]

The rhs for a loop should be strict for the initial edge a, i.e., if is_bot a then a else join a b where b is the value of the back edge.

@michael-schwarz and I further discussed this with Helmut. We came up with the potential issue that there might be labels in the loop, and there might be jumps into the loop from outside that could make it live.

One would therefore have to exclude that there are jumps into the loop body from outside code, to do this.

[vogler]

Yes, he mentioned it to me as well.

One would therefore have to exclude that there are jumps into the loop body from outside code, to do this.

What I wrote above should be sufficient and make these cases precise as well, no?

Also, one would have to think about loops that have jumps into them with goto (I guess you'd have to also identify all incoming edges into the loop body as initial).

I.e. every edge going into the loop that does not come from the loop is an initial edge and at the head all of them have to be bot to propagate it.

[jerhard]

I.e. every edge going into the loop that does not come from the loop is an initial edge and at the head all of them have to be bot to propagate it.

I guess that should work, yes.

[sim642]

I.e. every edge going into the loop that does not come from the loop is an initial edge and at the head all of them have to be bot to propagate it.

This sounds like a very non-local property though. I guess at the loop head getl could be used to check that the known alternative entry points to the loop are bot, but it still feels quite dirty.
Although that probably wouldn't even work well since it's checking the bottomness of the nodes, not the entering edges. We don't even have a notion of dead transitions.

Maybe one shouldn't speak of the head of such loop anyway and all target nodes of initial edges should be loop heads in this sense. One could construct loops with just gotos where there's no real head anyway. These initial edges and loop heads should be identifiable by some graph traversal (possibly very similar to the one already there are at the end of CFG construction).
Then the strictness of the initial edge should be again local to that particular node. if all initial edges are dead, then by strictness all heads will be. If some initial edge is live, then it makes the loop (at least partially) live.

[vogler]

Although that probably wouldn't even work well since it's checking the bottomness of the nodes, not the entering edges. We don't even have a notion of dead transitions.

All transitions should be strict, no? So checking if the start node of an edge is bottom should be fine.
(Maybe a candidate to quickcheck (all tf are strict) if it's not too hard.)
Or did you mean that a jump into a loop with a guard might result in bottom? That case would not be precise then, but I guess this would be split into a guard edge before the jump? If not, we'd need to compose tf to check if the transition target is dead.

Maybe one shouldn't speak of the head of such loop anyway and all target nodes of initial edges should be loop heads in this sense. One could construct loops with just gotos where there's no real head anyway.

I thought the loop head is the node which has at least an initial and a back edge incoming. This would also apply to gotos.
If using while/for in C, there should only be one loop head per loop, even if you have a goto into the loop.
(OTOH with gotos you can probably construct cycles in the CFG that can't be linearized to nested C-loops.)
Maybe loop entry is a better name for those target nodes of initial edges.

These initial edges and loop heads should be identifiable by some graph traversal (possibly very similar to the one already there are at the end of CFG construction).
Then the strictness of the initial edge should be again local to that particular node. if all initial edges are dead, then by strictness all heads will be. If some initial edge is live, then it makes the loop (at least partially) live.

Agree, that would be more precise.