Daneel: Type inference for Dalvik bytecode
In the last blog post about Daneel I mentioned one particular caveat of Dalvik bytecode, namely the existence of untyped instructions, which has a huge impact on how we transform bytecode. I want to take a similar approach as last time and look at one specific example to illustrate those implications. So let us take a look at the following Java method.
public float untyped(float[] array, boolean flag) { if (flag) { float delta = 0.5f; return array[7] + delta; } else { return 0.2f; } }
The above is a straightforward snippet and most of you probably know how the generated Java bytecode will look like. So let’s jump right to the Dalvik bytecode and discuss that in detail.
UntypedSample.untyped:([FZ)F: [regs=5, ins=3, outs=0] 0000: if-eqz v4, 0009 0002: const/high16 v0, #0x3f000000 0004: const/4 v1, #0x7 0005: aget v1, v3, v1 0007: add-float/2addr v0, v1 0008: return v0 0009: const v0, #0x3e4ccccd 000c: goto 0008
Keep in mind that Daneel doesn’t like to remember things, so he wants to look through the code just once from top to bottom and emit Java bytecode while doing so. He gets really puzzled at certain points in the code.
- Label 2: What is the type of register
v0
? - Label 4: What is the type of register
v1
? - Label 9: Register
v0
again? What’s the type at this point?
You, as a reader, do have the answer because you know and understand the semantic of the underlying Java code, but Daneel doesn’t, so he tries to infer the types. Let’s look through the code in the same way Daneel does.
At method entry he knows about the types of method parameters. Dalvik passes parameters in the last registers (in this case in v3
and v4
). Also we have a register (in this case v2
) holding a this
reference. So we start out with the following register types at method entry.
UntypedSample.untyped:([FZ)F: [regs=5, ins=3, outs=0] uninit uninit object [float bool
The array to the right represents the inferred register types at each point in the instruction stream as determined by the abstract interpreter. Note that we also have to keep track of the dimension count and the element type for array references. Now let’s look at the first block of instructions.
0002: const/high16 v0, #0x3f000000 u32 uninit object [float bool 0004: const/4 v1, #0x7 u32 u32 object [float bool 0005: aget v1, v3, v1 u32 float object [float bool 0007: add-float/2addr v0, v1 float float object [float bool
Each line shows the register type after the instruction has been processed. At each line Daneel learns something new about the register types.
- Label 2: I don’t know the type of
v0
, only that it holds an untyped 32-bit value. - Label 4: Same applies for
v1
here, it’s an untyped 32-bit value as well. - Label 5: Now I know
v1
is used as an array index, it must have been an integer value. Also the array reference in registerv3
is accessed, so I know the result is a float value. The result is stored inv1
, overwriting it’s previous content. - Label 7: Now I know
v0
is used in a floating-point addition, it must have been a float value.
Keep in mind that at each line, Daneel emits appropriate Java bytecode. So whenever he learns the concrete type of a register, he might need to retroactively patch previously emitted instructions, because some of his assumptions about the type were broken.
Finally we look at the second block of instructions reached through the conditional branch as part of the if
-statement.
0009: const v0, #0x3e4ccccd u32 uninit object [float bool 000c: goto 0008 float uninit object [float bool
When reaching this block we basically have the same information as at method entry. Again Daneel learns in the process.
- Label 9: I don’t know the type of
v0
, only that it holds an untyped 32-bit value. - Label 12: Now I know that
v0
has to be a float value because the unconditional branch targets the join-point at label 8. And I already looked at that code and know that we expect a float value in that register at that point.
This illustrates why our abstract interpreter also has to remember and merge register type information at each join-point. It’s important to keep in mind that Daneel follows the instruction stream from top to bottom, as opposed to the control-flow of the code.
Now imagine scrambling up the code so that instruction stream and control-flow are vastly different from each other, together with a few exception handlers and an optimal register re-usage as produced by some SSA representation. That’s where Daneel still keeps choking at the moment. But we can handle most of the code produced by the dx
tool already and will hunt down all those nasty bugs triggered by obfuscated code as well.
Disclaimer: The abstract interpreter and the method rewriter were mostly written by Rémi Forax, with this post I take no credit for it’s implementation whatsoever, I just want to explain how it works.
This is an interesting
This is an interesting article. https://towsontowtruck.com/
I visited a lot of website
I visited a lot of website but I appreciate this one contains something special in it in it Tony Scott Dietrich https://www.tvweek.com/tvbizwire/2019/10/how-to-get-warnermedias-upcomin...
Well written content. Thank
Well written content. Thank you for sharing. https://glenburnietowingservice.com/
The Quality Management
The Quality Management System, also called a QMS, has an array of methods, types, procedures and documents that are recorded. The report scope characterizes the scheme of operational rules that will govern how the company creates and transmits to customers the item and/or administration. The QMS needs to be tailored to your organization’s needs as well as the administration or item you ‘re giving, yet with an ISO 9001 Certification, it provides lots of rules which help make sure you don’t miss significant components where the QMS needs to be effective.
“It’s always good to learn
“It’s always good to learn tips like you share for blog posting. As I just started posting comments for blog and facing problem of lots of rejections. I think your suggestion would be helpful for me. I will let you know if its work for me too.” <a href="https://anthony-scott-dietrich.blogspot.com/">Anthony Scott Dietrich</a>
I was exactly searching for.
I was exactly searching for. Thanks for such a post and please keep it up.
Interesting piece, thanks for
Interesting piece, thanks for sharing! https://rosedaletowtruck.com/
I went through this website
I went through this website and found it very impressive. Keep sharing! https://middlerivertowtruck.com/
Well done on this
Well done on this post https://ellicottcitytowingservice.com/
offers quality plumbing
offers quality plumbing installation and repair services you can trust for your home or business.
Tree services near me are
Tree services near me are going to be able to fulfill all of your needs for tree services and other landscape services, such as weed abatement.
When it comes to fence
When it comes to fence installation, replacement, and repair services, you are going to need to turn to the fencing contractors here at Fencing Services Foster city.
that can provide quality
that can provide quality asphalt paving for any needs that you might have.
wanted to post a brief
wanted to post a brief comment to be able to say thanks to you for some of the amazing tips and hints you are giving here.
We are capable of helping
We are capable of helping with a variety of concrete services, big and small. With our team of experienced Commercial Concrete Portland, no job is beyond our level of expertise.
Concrete Contractor San Mateo
Concrete Contractor San Mateo provides the highest quality services.
Your home is the most
Your home is the most important place for you to feel safe, comfortable, and rejuvenated.
We go above and beyond the
We go above and beyond the regular standards of home renovation contractors, delivering custom design and premium materials.
where you can get top-notch
where you can get top-notch home remodeling services for your home at affordable prices.
Fortunately, you can make
Fortunately, you can make your home your dream living space once again with Home Remodel.
Great content, excellent!
Great content, excellent! https://edgewoodtowtruck.com/
operate throughout Luton
operate throughout Luton Bedfordshire and its surrounding areas, therefore, if you need any inquiry, we are ready to help.
Our carpenters and joiners
Our carpenters and joiners are dedicated to woodworking, loft conversions, framing, bespoke, roofing, and much more.
https://kogler-usa.com/ Well
https://kogler-usa.com/
Well of course you first might want to get acquainted with this new technology in mattresses.
St Albans Electricians Team
St Albans Electricians Team provides professional electrical services.
are professional electricians
are professional electricians and contractors who provide professional electrical services.
The values from the formula
The values from the formula are spot on and tied nicely to the merging of the abstract join points.
Nice approach! Your critical
Nice approach! Your critical thinking is awesome. Keep it up. :)
By decoupling the type
By decoupling the type inference problem from the low level bytecode representation, and abstracting it into a constraint system, we show that there exists verifiable bytecode that cannot be statically typed.
changing the fixtures, the
changing the fixtures, the flooring, and possibly even the design and structure of the walls.
Our concrete contractors work
Our concrete contractors work tirelessly in the Fort Wayne, Indiana area to give our customers the best possible outcome.
the perfect option when it
the perfect option when it refers to all of your remodeling necessities.
always ready to assist,
always ready to assist, whether your kitchen, bathroom, or home needs repair or you just want to modify the look.
renovates homes to meet the
renovates homes to meet the specific needs of each household.
can expertly put to reality
can expertly put to reality your unique preference, taste, and vision.
will provide you with an
will provide you with an instant makeover or a full renovation for your kitchen.
the largest full-service
the largest full-service kitchen remodeling company in California.
is here to help you navigate
is here to help you navigate the renovation phase and see the home remodeling dream through to completion.
services have been a pioneer
services have been a pioneer of home construction and kitchen remodeling contractors for many years.
Your desire is our priority
Your desire is our priority when you choose Home Remodel.
will assist you in remodeling
will assist you in remodeling your home to make it more appropriate for your lifestyle.
You put really very helpful
You put really very helpful information. Keep it up.
even the design and structure
even the design and structure of the walls.
provide quality professional
provide quality professional and affordable tree removal by a fully licenced, insured and experienced team.
provide quality professional
provide quality professional and affordable tree removal.
Our business is based in
Our business is based in Stevenage, Hertfordshire, and serves the town and local area.
I like your site
I like your site https://tysonstowtruck.com/
It's been a long time since
It's been a long time since I've read such a positive story...
Excellent
Excellent posts
https://sterlingtowtruck.com/
Informative, well explained
Informative, well explained https://www.chantillytowtruck.com/