Large sections of a program may be completely syntactically, obviously equivalent and differences occur in only a couple blocks. A hypothesis is that maybe z3 is getting stuck in the weeds because it can see the details of these blocks, when for comparative purposes they are irrelevant.
In this case, it may be useful to abstract blocks to a set of uninterpreted functions, one for each variable that is written into in the
block. Then the only thing z3 can see about these blocks is that they are the same between comparisons.
It is possible to separate the straight line computation from the control flow jumps that occurs at the end of the block. We'd leave the jumps untouched and only abstract the straight line computation. Z3 and our already existent machinery will then determine if the control flow is equivalent, and in fact that is the only thing it will be checking for abstracted blocks.
They can be seen to be equivalent in the non-control part by a "unification" of their variables (it's a little easier than the usual unification since we can consider their variable sets to be disjoint). Go through the programs line by line maintaining a dictionary of blockA variables to blockB variables. All operations must be equal, every blockA variable when it's the first time you see it, note the corresponding blockB variable in the dict. If blockA key is already in the dict, make sure the blockB value in dict is compatible with what you see at that location in blockB.
The locations in f_1 f_2 where rax and rsp go are determined by the dict from the unification step.
If Z3 returns unsat, great. That is a real unsat. If z3 returns SAT, that may be an erroneous SAT from picking a model of the block functions that isn't right. One can run the input through the program to see if the SAT is actually a countermodel, or equivalently assert the countermodel against the unabstracted wp z3 constraints.
If the SAT model is erroneous, one can then either just try the completely unabstracted version, or trace through the program to find the blocks touched and unabstract one or all of the blocks on that path and try again, iteratively refining the abstraction.
The hypothesis that abstracted blocks are easier on z3 may not be true. In this example, the abstracted version seems more complicated than the original. Maybe it's only worth doing for large blocks? Maybe it doesn't help period. Research.
The simple version above just includes every variable that occurs in the right hand side in the block as an argument to the "block functions", but with a data flow analysis, it could be compressed to
Since we can see that original value of rsp does not affect anything. Not every block function need have the same number of arguments either.
"simultaneous" could be achieved by using temporary variables, or by using Subst of Constr.t, which supports simultaenous substitution
Question: how much of a problem is memory? Memory is written to as a complete overwrite in bap. We would not want to do this in the abstraction, since then the entirety of memory could be scrambled by the block, when surely only a few locations are written to. It seems plausible through some analysis to only use the indexed into memory locations and only write to them though. Looking at bil, writes to memory are almost always in the shape of a simple store from a single location. If such an analysis fails and one knows it failed, one can always revert back to the unabstracted form of that block, and continue on, no harm done.
Another interesting step might be to check for not only syntactic equality, but use z3 to check complete functional equality of the blocks with the variable correspondence asserted as equalities in a comparative precondition. I'm doubtful this would gain much over syntactic equality.
One could also abstract entire equivalent subgraphs of the cfg if they syntactically equivalent and have a single entry and exit edge, in which case they are a kind of "macro block". This is problematic in the sense that if there are loops in this subgraph, control doesn't ever necessarily exit that piece of the cfg, but I'm not sure how good we are on termination anyway.
Large sections of a program may be completely syntactically, obviously equivalent and differences occur in only a couple blocks. A hypothesis is that maybe z3 is getting stuck in the weeds because it can see the details of these blocks, when for comparative purposes they are irrelevant. In this case, it may be useful to abstract blocks to a set of uninterpreted functions, one for each variable that is written into in the block. Then the only thing z3 can see about these blocks is that they are the same between comparisons.
It is possible to separate the straight line computation from the control flow jumps that occurs at the end of the block. We'd leave the jumps untouched and only abstract the straight line computation. Z3 and our already existent machinery will then determine if the control flow is equivalent, and in fact that is the only thing it will be checking for abstracted blocks.
Consider the following two blocks
They can be seen to be equivalent in the non-control part by a "unification" of their variables (it's a little easier than the usual unification since we can consider their variable sets to be disjoint). Go through the programs line by line maintaining a dictionary of blockA variables to blockB variables. All operations must be equal, every blockA variable when it's the first time you see it, note the corresponding blockB variable in the dict. If blockA key is already in the dict, make sure the blockB value in dict is compatible with what you see at that location in blockB.
Here both could be abstracted by
The locations in f_1 f_2 where rax and rsp go are determined by the dict from the unification step.
If Z3 returns unsat, great. That is a real unsat. If z3 returns SAT, that may be an erroneous SAT from picking a model of the block functions that isn't right. One can run the input through the program to see if the SAT is actually a countermodel, or equivalently assert the countermodel against the unabstracted wp z3 constraints. If the SAT model is erroneous, one can then either just try the completely unabstracted version, or trace through the program to find the blocks touched and unabstract one or all of the blocks on that path and try again, iteratively refining the abstraction.
The hypothesis that abstracted blocks are easier on z3 may not be true. In this example, the abstracted version seems more complicated than the original. Maybe it's only worth doing for large blocks? Maybe it doesn't help period. Research.
The simple version above just includes every variable that occurs in the right hand side in the block as an argument to the "block functions", but with a data flow analysis, it could be compressed to
Since we can see that original value of rsp does not affect anything. Not every block function need have the same number of arguments either.
"simultaneous" could be achieved by using temporary variables, or by using Subst of Constr.t, which supports simultaenous substitution
Question: how much of a problem is memory? Memory is written to as a complete overwrite in bap. We would not want to do this in the abstraction, since then the entirety of memory could be scrambled by the block, when surely only a few locations are written to. It seems plausible through some analysis to only use the indexed into memory locations and only write to them though. Looking at bil, writes to memory are almost always in the shape of a simple store from a single location. If such an analysis fails and one knows it failed, one can always revert back to the unabstracted form of that block, and continue on, no harm done.
Another interesting step might be to check for not only syntactic equality, but use z3 to check complete functional equality of the blocks with the variable correspondence asserted as equalities in a comparative precondition. I'm doubtful this would gain much over syntactic equality.
One could also abstract entire equivalent subgraphs of the cfg if they syntactically equivalent and have a single entry and exit edge, in which case they are a kind of "macro block". This is problematic in the sense that if there are loops in this subgraph, control doesn't ever necessarily exit that piece of the cfg, but I'm not sure how good we are on termination anyway.