Liveness states equal hint rfc #8333
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Allow reading object file list from file. E.g. the following command: ./veristat @list.txt Is equivalent to the following invocation: ./veristat line-1 line-2 ... line-N Where line-i corresponds to lines from list.txt. Lines starting with '#' are ignored. Signed-off-by: Eduard Zingerman <[email protected]>
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
3 times, most recently
from
9632415 to
21a4297
Compare
eddyz87
force-pushed
the
liveness-states-equal-hint-rfc
branch
2 times, most recently
from
763d6bd to
712bff5
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
21a4297 to
36a754d
Compare
Compute may-live registers after each instruction in the program.
The register is live after the instruction I if it is read by some
instruction S following I during program execution and is not
overwritten between I and S.
This information would be used in the follow-up patches to insert
registers r0-r5 spills and fills for helper calls following
no_caller_saved_registers convention.
Use a simple algorithm described in [1] to compute this information:
- define the following:
- I.use : a set of all registers read by instruction I;
- I.def : a set of all registers written by instruction I;
- I.in : a set of all registers that may be alive before I execution;
- I.out : a set of all registers that may be alive after I execution;
- I.successors : a set of instructions S that might immediately
follow I for some program execution;
- associate separate empty sets 'I.in' and 'I.out' with each instruction;
- visit each instruction in a postorder and update corresponding
'I.in' and 'I.out' sets as follows:
I.out = U [S.in for S in I.successors]
I.in = (I.out / I.def) U I.use
(where U stands for set union, / stands for set difference)
- repeat the computation while I.{in,out} changes for any instruction.
On implementation side keep things as simple, as possible:
- check_cfg() already marks instructions EXPLORED in post-order,
modify it to save the index of each EXPLORED instruction in a vector;
- represent I.{in,out,use,def} as bitmasks;
- don't split the program into basic blocks and don't maintain the
work queue, instead:
- do fixed-point computation by visiting each instruction;
- maintain a simple 'changed' flag if I.{in,out} for any instruction
change;
Measurements show that even such simplistic implementation does not
add measurable verification time overhead (for selftests, at-least).
Note on check_cfg() ex_insn_beg/ex_done change:
To avoid out of bounds access to env->cfg.insn_postorder array,
it should be guaranteed that instruction transitions to EXPLORED state
only once. Previously this was not the fact for incorrect programs
with direct calls to exception callbacks.
The 'align' selftest needs adjustment to skip computed insn/live
registers printout. Otherwise it matches lines from the live registers
printout.
[1] https://en.wikipedia.org/wiki/Live-variable_analysis
Signed-off-by: Eduard Zingerman <[email protected]>
Liveness analysis DFA computes a conservative set of registers live before each instruction. Leverage this information to skip comparison of dead registers in func_states_equal(). This helps with convergance of iterator processing loops, as bpf_reg_state->live marks can't be used when loops are processed. This has certain performance impact for selftests, here is a veristat listing for bigger ones: File Program Insns (DIFF) States (DIFF) ---------------------------------- ----------------------------------- ---------------- -------------- iters.bpf.o checkpoint_states_deletion -16636 (-91.81%) -745 (-91.19%) iters.bpf.o iter_nested_deeply_iters -267 (-47.09%) -26 (-41.27%) iters.bpf.o iter_nested_iters -181 (-22.26%) -17 (-21.52%) iters.bpf.o iter_subprog_iters -339 (-33.80%) -24 (-28.92%) iters.bpf.o loop_state_deps2 -349 (-48.14%) -27 (-42.86%) pyperf600_iter.bpf.o on_event -795 (-6.59%) +239 (+65.30%) The pyperf600_iter is curious, as it shows an increase in number of processed states. The reason for this is: <TBD> Signed-off-by: Eduard Zingerman <[email protected]>
Cover instructions from each kind: - assignment - arithmetic - store/load - endian conversion - atomics - branches, conditional branches, may_goto, calls - LD_ABS/LD_IND - address_space_cast Signed-off-by: Eduard Zingerman <[email protected]>
eddyz87
force-pushed
the
liveness-states-equal-hint-rfc
branch
from
712bff5 to
8e31ba2
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
5 times, most recently
from
483693f to
d01d9d5
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.