ivg on master
Add PPC frame modi. (compare)
github-actions[bot] on master
github-actions[bot] on v2.6.0-alpha
makes RSP correction for x86 ta… KB-friendly functions in `Bap.S… (compare)
ivg on master
KB-friendly functions in `Bap.S… (compare)
ivg on master
makes RSP correction for x86 ta… (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.
destsproperty 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.collecton the predecessors?