github-actions[bot] on v2.3.0-alpha
introduces the BIL code slot an… (compare)
ivg on master
introduces the BIL code slot an… (compare)
github-actions[bot] on v2.3.0-alpha
ivg on master
introduces BIL special encoding… (compare)
ivg on master
fixes PE/COFF sections (#1263) … (compare)
ivg on master
starts 2.3.0 release cycle (#12… (compare)
Using this option:
--bil-enable-intrinsics=VAL
Translate the specified instructions into calls to intrinsic
functions. The option accepts a list of instruction specifications
and can be specified multiple times. Each element of the list is
either a keyword or a parametrized predicate. If an instruction
matches any of the specifications than it will be translated into a
call to an intrinsic function. The following keywords are
recognized, :any - matches with any instruction, :unknown - matches
with instructions that have unknown (to our lifters) semantics,
:special - matches with instructions that have special semantics
(expressed with the special statement by our lifters). The
following predicates are recognized, asm:<str> matches with
instructions which assembly strings start with <str>, tag:<str> -
matches with instructions that have a tag (kind) that starts with
<str>, <s1>:<s2> - matches with instructions that have opcodes
starting with <s2> in the encoding that starts with <s1>. For
predicates, all string comparisons are made case-insensitive.
Example, :unknown,:special,asm:addsd,llvm:trap.
It is quite cumbersome, so maybe we should disable SSE by default (and use intrinsics for them) and add an oposite option that will enable them. Basically, it is very easy to kill BAP with SSE instructions and heavy inlining.
If I include threads and not lwt.unix, it fails on an undefined unix_exit symbol from lwt.unix, so I don't think it is an exclusively thread related problem.
@philzook58, don't think that I've forgotten about you :) So, I looked at the problem and it looks like that the problem is in the compiler, i.e., in the unix.cmxs
file that it generates. It is indeed missing the unix_exit
symbol, which is never referenced in their code and therefore is not included. I've sent ocaml/ocaml#9906 to the upstream but even if it will be merged it will hit bap no earlier than in a couple of years, which is not an option for us.
Another two solutions is to ask lwt to remove the reference to unix_exit
(or to add their own stub). There is also a workaround, we can just add external unix_exit : int -> 'a = "unix_exit"
to the bap_frontend.ml
and thus force the linker to link it in, and then we can easily link lwt programs into bap.
Going back to @philzook58 question, if we would like to compute the liveness analysis without having a CFG, we can employ the KB for that. E.g.,
let () = KB.promise liveness @@ fun label ->
KB.collect Theory.Program.Semantics.slot label >>= fun insn ->
let sol = liveness_from_insn insn in
let dests = KB.Value.get Insn.Slot.dests insn in
fallthrough label >>= fun fall ->
let dests = Set.add dests fall in
Set.to_sequence dests |>
KB.Seq.fold ~init:sol ~f:(fun sol dest ->
KB.collect liveness dest >>| merge sol)
This will compute the fixed point solution, without actually building the graph. So that asking for the liveness at the given address will trigger some number of instruction (that belong to the same execution path, potentially all instruction, potentiall the current instruction itself) and iterate until the fixed point is reached. Of course, since we don't have the graph we can iterate in the desired order so we have to rely on the stochastic fixed point.
dests
property computation there could be the VSA computation, that itself may access the liveness information, and it will be included in the fixed point also.
KB.collect
on the predecessors?