Ite predication #9
Conversation
|
Could you please remove the badc474 commit from this branch as it is already in the master branch? |
There was a problem hiding this comment.
We're using the if <cond> then <exp1> else <exp2> syntax that vocalizes that this is a control-flow expression and brings all the common intuition that the evaluation of the branches shall not be strict.
So in order not to bring the wrath of angriness upon us, I'm suggesting changing the concrete syntax as well :)
I've reviewed different languages and systems, to understand which syntax will bring the right intuition.
-
c ? x : yis used by Verilog to define multiplexers, but it is also defined C and most people will think in terms of C, rather than Verilog. -
x when c else yis used in VHDL for the same purpose, but it resembles a lot Pythonishx if c else y, so it bears the same wrong intuition. Also, it is verbose. -
mux c x yis used by Hardcaml, however, it sounds to low-level (despite the fact, that reflects the exact semantics) -
ite c x y is used by SMT-LIB where it is defined as a function in the Core logic.
While mux looks like the right solution, I personally don't like its low-levelness. I believe that majority of BAP users reason more in terms of SMT-LIB and mathematical logic, rather than combinatorial logic.
So, if nobody have any objections, could you please change it to ite c x y syntax.
This reverts commit 978af49.
DIJamner
force-pushed
the
ite_predication
branch
from
1a93aab to
dffddbc
Compare
|
The |
|
thanks! |
|
Looks like a very reasonable PR 👍 |
The semantics of ite evaluation in Primus follow the latest updates in the BIL specification: BinaryAnalysisPlatform/bil#9 The extra option in the BIL normalization function enables the user to preserve ite if that is desirable.
The semantics of ite evaluation in Primus follow the latest updates in the BIL specification: BinaryAnalysisPlatform/bil#9 The extra option in the BIL normalization function enables the user to preserve ite if that is desirable.
…#850) The semantics of ite evaluation in Primus follow the latest updates in the BIL specification: BinaryAnalysisPlatform/bil#9 The extra option in the BIL normalization function enables the user to preserve ite if that is desirable.
Changes the semantics of ite expressions to evaluate their branches before reducing the condition. Also adds last rule necessary to prove progress and preservation for expression evaluation. Note that this pull request is on top of pull request #8. This pull request should only be merged if it is determined that this behavior for ite is desirable.