On 05.12.2016 17:54, Edward Cree wrote: > On 05/12/16 16:50, Hannes Frederic Sowa wrote: >> On 05.12.2016 17:40, Edward Cree wrote: >>> I may be completely mistaken here, but can't the verifier unroll the loop >>> 'for >>> verification' without it actually being unrolled in the program? >>> I.e., any "proof that the loop terminates" should translate into "rewrite of >>> the directed graph to make it a DAG, possibly duplicating a lot of insns", >>> and >>> you feed the rewritten graph to the verifier, while using the original loopy >>> version as the actual program to store and later execute. >>> Then the verifier happily checks things like array indices being valid, >>> without >>> having to know about the bounded loops. >> That is what is already happening. E.g. __builtin_memset is expanded up >> to 128 rounds (which is a lot) but at some point llvm doesn't do enoug >> unrolling of that. >> >> The BPF target configures that in >> http://llvm.org/docs/doxygen/html/BPFISelLowering_8cpp_source.html on >> line 166-169. > I think you're talking about the _compiler_ unrolling loops before it > submits the program to the kernel. I'm talking about having the _verifier_ > unroll them, so that we can execute the original (non-unrolled) version. > Or am I misunderstanding?
Ah, in the verifier this would be part of flow control analysis what we are talking about in the other part of this thread. Bye, Hannes
