You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Context: I am currently creating a lifter plugin for aarch64. We use BAP to disassemble and obtain the opcodes for a program, which are then passed into the ASL-interpreter, which obtains an OCaml representation of the semantics of the instructions, which are then passed back to the plugin to be translated and added to the knowledge base.
At this stage, the lifter is able to successfully lift many different instructions, and doesn't throw any errors when lifting a binary file. However, when we give it a binary file, gotos are inserted between each instruction in the BIR output, causing the output to be quite a bit more complicated than it needs to be.
0003ad3b:
0003ad45: goto %0003ad41
0003ad41:
0003ad4b: goto %0003ad47
0003ad47:
0003ad52: goto %0003ad4e
0003ad4e:
0003ad57: Exp21__5 := SP\.read13__5
0003ad5b: Exp23__5 := R29
0003ad5f: Exp25__5 := R30
0003ad65: mem := mem with [Exp21__5 - 0x20, be]:u64 <- Exp23__5
0003ad6b: mem := mem with [Exp21__5 - 0x18, be]:u64 <- Exp25__5
0003ad6f: Exp28__5 := SPF
0003adab: goto %0003ada5
0003ada5:
0003ada7: when ~Exp28__5 goto %0003ad73
0003ada8: goto %0003ad77
I would like these instructions to just be outputted sequentially, with no gotos in between them. I believe that the issue isn't in the translating itself, as these gotos are even generated for empty operations, where we don't translate any ASL (Arm Specification Language) statements.
One thing that may be causing this could be incorrect use of the ctrl parameter to CT.blk. We may not be constructing the control flow graph correctly. However, I'm not sure what to do differently, as when the error occurs for empty operations, ctrl is initialised as CT.perform Theory.Effect.Sort.bot (which I've seen in numerous other plugins), and is not mutated at all.
Using CT.blk could be wrong as well, as I don't necessarily want each operation to be its own 'block', but I'm not sure how else to wrap the data and ctrl to add it to the knowledge base.
Throughout the translation process, we have a state:
type comp_state = {
vars: unit Theory.Var.t Variables.t;
data: Theory.data Theory.effect KB.t;
ctrl: Theory.ctrl Theory.effect KB.t;
throwErrors: bool;
}
This state originally starts as empty for data and ctrl, but data knowledge is added through Theory.Core operations, and ctrl is modified if we encounter branching.
The lifter function returns
Another idea I had is that we are currently not specifying a domain or KB.Class.property, which contains some methods to specify like join. I haven't had any success so far with these having any affect on the BIR output.
let domain = KB.Domain.flat "a64-program" ~empty:(KB.return (Theory.Effect.empty Theory.Effect.Sort.bot)) ~equal:(fun _ _ -> true) in
let property = KB.Class.property Theory.Semantics.cls "a64-lifter" domain ~public:true in
...
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
Context: I am currently creating a lifter plugin for aarch64. We use BAP to disassemble and obtain the opcodes for a program, which are then passed into the ASL-interpreter, which obtains an OCaml representation of the semantics of the instructions, which are then passed back to the plugin to be translated and added to the knowledge base.
At this stage, the lifter is able to successfully lift many different instructions, and doesn't throw any errors when lifting a binary file. However, when we give it a binary file,
goto
s are inserted between each instruction in the BIR output, causing the output to be quite a bit more complicated than it needs to be.I would like these instructions to just be outputted sequentially, with no
goto
s in between them. I believe that the issue isn't in the translating itself, as thesegoto
s are even generated for empty operations, where we don't translate any ASL (Arm Specification Language) statements.One thing that may be causing this could be incorrect use of the
ctrl
parameter toCT.blk
. We may not be constructing the control flow graph correctly. However, I'm not sure what to do differently, as when the error occurs for empty operations,ctrl
is initialised asCT.perform Theory.Effect.Sort.bot
(which I've seen in numerous other plugins), and is not mutated at all.Using
CT.blk
could be wrong as well, as I don't necessarily want each operation to be its own 'block', but I'm not sure how else to wrap thedata
andctrl
to add it to the knowledge base.Throughout the translation process, we have a state:
This state originally starts as empty for
data
andctrl
, but data knowledge is added through Theory.Core operations, andctrl
is modified if we encounter branching.The
lifter
function returnswhich is called by a
load
function, which returnsAnother idea I had is that we are currently not specifying a domain or
KB.Class.property
, which contains some methods to specify likejoin
. I haven't had any success so far with these having any affect on the BIR output.Thanks!
Beta Was this translation helpful? Give feedback.
All reactions