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 register v3 is accessed, so I know the result is a float value. The result is stored in v1, 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.

I like how it is

I like how it is explained
https://leesburgtowtruck.com/

Great blog! Hoping to see

Great blog! Hoping to see more of these posts in the future!

I want to learn more of this

I want to learn more of this https://viennatowtruck.com/

I think this shoul'd feet to

I think this shoul'd feet to our service: ac company in pittsburgh

It was very useful to me.

It was very useful to me. Thank you so much as you have been willing to share information with us. We will forever admire all you have done here

Thank you for sharing this

Thank you for sharing this https://mcleantowtruck.com/

Interesting, so nice

Interesting, so nice https://centrevilletowtruck.com/

Nice work

So great

https://willdylan.tv

https://victoriasbestflooring

https://www.theconductorbarbe

https://paccapital.com.au

Amazing piece! I'll bookmark

Amazing piece! I'll bookmark this and will share it to a friend.

https://nlsinspections.com

https://www.jmw.com/

I really loved reading your

I really loved reading your blog. It was very well authored and easy to understand.

https://getfreighted.com.au/

https://www.getfreightedcella

https://car2cash.com.au

https://authenticbotulinum.co

This is interesting

This is interesting https://burketowtruck.com/

Impressive https://annandalet

That is really good |

That is really good | https://towtruckarlingtonva.com/

Nice one!

great job on that

great job on that https://towtruckfairfax.com/

This site is really nice

This site is really nice https://woodbridgetowtruck.com/

Nice post

That was a nice post |

That was a nice post | https://manassastowtruck.com/

If you are on the hunt for a

If you are on the hunt for a company that not only cares for its clients but also the city in which it operates, then you should call NYC Demolition Contractor Co today!

Which converts Java bytecode

Which converts Java bytecode to Dalvik bytecode?

I think everything published

I think everything published was very reasonable.
But, what about this? what if you wrote a catchier title?

I am not saying your information is not solid, however what
if you added something that makes people desire
more? I mean Reply to comment | antforge.org is a little plain. You should peek at Yahoo's home page and note how they write article
titles to get viewers interested. You might add a related
video or a related pic or two to get readers excited about
everything've got to say. In my opinion, it would make your website a little bit more
interesting. https://8tracks.com/jgbsor43

We work in a very competitive

We work in a very competitive industry. Over the years, the number of concrete companies in Indiana has grown in numbers.

This is what I need, the Java

This is what I need, the Java method. Been trying to figure it out on my own but I can't. I think I need a mentor for this.

I've been practising this

I've been practising this since last year but it's too hard to analyze each code. You are great!

As a leading concrete

As a leading concrete contractor in the region, we conduct our business with the highest level of honesty and transparency.

What's up friends, its

What's up friends, its enormous paragraph about educationand entirely
explained, keep it up all the time. http://forum.geonames.org/gforum/user/profile/569859.page

This is what I want to learn,

This is what I want to learn, making a bytecode. Thank you for sharing this Java method.

Our name is Bloomington

Our name is Bloomington Concrete Contractors Co, the city of Bloomington’s favorite concrete provider. When you need first-class solutions in concrete installations and repairs, you can always count on us.

This is something we can rely

This is something we can rely on, isn't it?

This is exactly what I'm

This is exactly what I'm looking for! Thanks for sharing!

We will wait for the next

We will wait for the next update for this particular topic!

Yes, we will also wait for

Yes, we will also wait for more updates ! thank you

This is what the people

This is what the people online need, quality content like this

Welcome to the number one

Welcome to the number one source of epoxy solutions in the city of Port St Lucie, Florida, Port St Lucie Epoxy Garage Floor Pros.

Please give us more updates,

Please give us more updates, really love the details, you see.

Are there any updates

Are there any updates regarding this topic? https://www.mycardetailchicago.com/

Thus not only can one gain

Thus not only can one gain excitement out of this sport but also money. Online games can be played any where so long as one can access the internet and subscribe for them. However some may not be easy to down load if they require a certain amount of money to be paid or fee before gaining access to them.

This is exactly what I'm

This is exactly what I'm looking for, Thanks for the valuable ideas!

The lines were very well

The lines were very well explained and the sequencing is indeed perfect as it is.