Add sources.

.gitignore

@@ -17,3 +17,5 @@ project/plugins/project/
 .scala_dependencies
 .worksheet
 
+# IntelliJ IDEA
+.idea/

README.md

@@ -1,3 +1,12 @@
-# DalvikBytecodeAnalysis
+# Dalvik bytecode analysis
+
+## Installation
+
+[SBT](https://www.scala-sbt.org/)
+
+## System requirements
+
+[Apktool](https://ibotpeaches.github.io/Apktool/) in the path.
+
+[Z3](https://github.com/Z3Prover/z3) version >= 4.6.1
 
-Master's thesis project.

build.sbt

@@ -0,0 +1,14 @@
+name := "MasterThesisProject"
+
+version := "0.1"
+
+scalaVersion := "2.12.6"
+
+// https://mvnrepository.com/artifact/org.smali/baksmali
+libraryDependencies += "org.smali" % "baksmali" % "2.2.3"
+
+// https://mvnrepository.com/artifact/com.typesafe.scala-logging/scala-logging
+libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.0"
+
+// https://mvnrepository.com/artifact/ch.qos.logback/logback-classic
+libraryDependencies += "ch.qos.logback" % "logback-classic" % "1.2.3"

project/build.properties

@@ -0,0 +1 @@
+sbt.version = 1.1.1

src/main/resources/android/Callbacks.txt

@@ -0,0 +1,182 @@
+android.accounts.OnAccountsUpdateListener
+android.animation.Animator$AnimatorListener
+android.animation.LayoutTransition$TransitionListener
+android.animation.TimeAnimator$TimeListener
+android.animation.ValueAnimator$AnimatorUpdateListener
+android.app.ActionBar$OnMenuVisibilityListener
+android.app.ActionBar$OnNavigationListener
+android.app.ActionBar$TabListener
+android.app.Application$ActivityLifecycleCallbacks
+android.app.DatePickerDialog$OnDateSetListener
+android.app.FragmentBreadCrumbs$OnBreadCrumbClickListener
+android.app.FragmentManager$OnBackStackChangedListener
+android.app.KeyguardManager$OnKeyguardExitResult
+android.app.LoaderManager$LoaderCallbacks
+android.app.PendingIntent$OnFinished
+android.app.SearchManager$OnCancelListener
+android.app.SearchManager$OnDismissListener
+android.app.TimePickerDialog$OnTimeSetListener
+android.bluetooth.BluetoothProfile$ServiceListener
+android.content.ServiceConnection
+android.content.ClipboardManager$OnPrimaryClipChangedListener
+android.content.ComponentCallbacks
+android.content.ComponentCallbacks2
+android.content.DialogInterface$OnCancelListener
+android.content.DialogInterface$OnClickListener
+android.content.DialogInterface$OnDismissListener
+android.content.DialogInterface$OnKeyListener
+android.content.DialogInterface$OnMultiChoiceClickListener
+android.content.DialogInterface$OnShowListener
+android.content.IntentSender$OnFinished
+android.content.Loader$OnLoadCanceledListener
+android.content.Loader$OnLoadCompleteListener
+android.content.SharedPreferences$OnSharedPreferenceChangeListener
+android.content.SyncStatusObserver
+android.database.sqlite.SQLiteTransactionListener
+android.drm.DrmManagerClient$OnErrorListener
+android.drm.DrmManagerClient$OnEventListener
+android.drm.DrmManagerClient$OnInfoListener
+android.gesture.GestureOverlayView$OnGestureListener
+android.gesture.GestureOverlayView$OnGesturePerformedListener
+android.gesture.GestureOverlayView$OnGesturingListener
+android.graphics.SurfaceTexture$OnFrameAvailableListener
+android.hardware.Camera$AutoFocusCallback
+android.hardware.Camera$AutoFocusMoveCallback
+android.hardware.Camera$ErrorCallback
+android.hardware.Camera$FaceDetectionListener
+android.hardware.Camera$OnZoomChangeListener
+android.hardware.Camera$PictureCallback
+android.hardware.Camera$PreviewCallback
+android.hardware.Camera$ShutterCallback
+android.hardware.SensorEventListener
+android.hardware.display.DisplayManager$DisplayListener
+android.hardware.input.InputManager$InputDeviceListener
+android.inputmethodservice.KeyboardView$OnKeyboardActionListener
+android.location.GpsStatus$Listener
+android.location.GpsStatus$NmeaListener
+android.location.LocationListener
+android.media.AudioManager$OnAudioFocusChangeListener
+android.media.AudioRecord$OnRecordPositionUpdateListener
+android.media.JetPlayer$OnJetEventListener
+android.media.MediaPlayer$OnBufferingUpdateListener
+android.media.MediaPlayer$OnCompletionListener
+android.media.MediaPlayer$OnErrorListener
+android.media.MediaPlayer$OnInfoListener
+android.media.MediaPlayer$OnPreparedListener
+android.media.MediaPlayer$OnSeekCompleteListener
+android.media.MediaPlayer$OnTimedTextListener
+android.media.MediaPlayer$OnVideoSizeChangedListener
+android.media.MediaRecorder$OnErrorListener
+android.media.MediaRecorder$OnInfoListener
+android.media.MediaScannerConnection$MediaScannerConnectionClient
+android.media.MediaScannerConnection$OnScanCompletedListener
+android.media.SoundPool$OnLoadCompleteListener
+android.media.audiofx.AudioEffect$OnControlStatusChangeListener
+android.media.audiofx.AudioEffect$OnEnableStatusChangeListener
+android.media.audiofx.BassBoost$OnParameterChangeListener
+android.media.audiofx.EnvironmentalReverb$OnParameterChangeListener
+android.media.audiofx.Equalizer$OnParameterChangeListener
+android.media.audiofx.PresetReverb$OnParameterChangeListener
+android.media.audiofx.Virtualizer$OnParameterChangeListener
+android.media.audiofx.Visualizer$OnDataCaptureListener
+android.media.effect$EffectUpdateListener
+android.net.nsd.NsdManager$DiscoveryListener
+android.net.nsd.NsdManager$RegistrationListener
+android.net.nsd.NsdManager$ResolveListener
+android.net.sip.SipRegistrationListener
+android.net.wifi.p2p.WifiP2pManager$ActionListener
+android.net.wifi.p2p.WifiP2pManager$ChannelListener
+android.net.wifi.p2p.WifiP2pManager$ConnectionInfoListener
+android.net.wifi.p2p.WifiP2pManager$DnsSdServiceResponseListener
+android.net.wifi.p2p.WifiP2pManager$DnsSdTxtRecordListener
+android.net.wifi.p2p.WifiP2pManager$GroupInfoListener
+android.net.wifi.p2p.WifiP2pManager$PeerListListener
+android.net.wifi.p2p.WifiP2pManager$ServiceResponseListener
+android.net.wifi.p2p.WifiP2pManager$UpnpServiceResponseListener
+android.os.CancellationSignal$OnCancelListener
+android.os.IBinder$DeathRecipient
+android.os.MessageQueue$IdleHandler
+android.os.RecoverySystem$ProgressListener
+android.preference.Preference$OnPreferenceChangeListener
+android.preference.Preference$OnPreferenceClickListener
+android.preference.PreferenceFragment$OnPreferenceStartFragmentCallback
+android.preference.PreferenceManager$OnActivityDestroyListener
+android.preference.PreferenceManager$OnActivityResultListener
+android.preference.PreferenceManager$OnActivityStopListener
+android.security.KeyChainAliasCallback
+android.speech.RecognitionListener
+android.speech.tts.TextToSpeech$OnInitListener
+android.speech.tts.TextToSpeech$OnUtteranceCompletedListener
+android.view.ActionMode$Callback
+android.view.ActionProvider$VisibilityListener
+android.view.GestureDetector$OnDoubleTapListener
+android.view.GestureDetector$OnGestureListener
+android.view.InputQueue$Callback
+android.view.KeyEvent$Callback
+android.view.MenuItem$OnActionExpandListener
+android.view.MenuItem$OnMenuItemClickListener
+android.view.ScaleGestureDetector$OnScaleGestureListener
+android.view.SurfaceHolder$Callback
+android.view.SurfaceHolder$Callback2
+android.view.TextureView$SurfaceTextureListener
+android.view.View$OnAttachStateChangeListener
+android.view.View$OnClickListener
+android.view.View$OnCreateContextMenuListener
+android.view.View$OnDragListener
+android.view.View$OnFocusChangeListener
+android.view.View$OnGenericMotionListener
+android.view.View$OnHoverListener
+android.view.View$OnKeyListener
+android.view.View$OnLayoutChangeListener
+android.view.View$OnLongClickListener
+android.view.View$OnSystemUiVisibilityChangeListener
+android.view.View$OnTouchListener
+android.view.ViewGroup$OnHierarchyChangeListener
+android.view.ViewStub$OnInflateListener
+android.view.ViewTreeObserver$OnDrawListener
+android.view.ViewTreeObserver$OnGlobalFocusChangeListener
+android.view.ViewTreeObserver$OnGlobalLayoutListener
+android.view.ViewTreeObserver$OnPreDrawListener
+android.view.ViewTreeObserver$OnScrollChangedListener
+android.view.ViewTreeObserver$OnTouchModeChangeListener
+android.view.accessibility.AccessibilityManager$AccessibilityStateChangeListener
+android.view.animation.Animation$AnimationListener
+android.view.inputmethod.InputMethod$SessionCallback
+android.view.inputmethod.InputMethodSession$EventCallback
+android.view.textservice.SpellCheckerSession$SpellCheckerSessionListener
+android.webkit.DownloadListener
+android.widget.AbsListView$MultiChoiceModeListener
+android.widget.AbsListView$OnScrollListener
+android.widget.AbsListView$RecyclerListener
+android.widget.AdapterView$OnItemClickListener
+android.widget.AdapterView$OnItemLongClickListener
+android.widget.AdapterView.OnItemSelectedListener
+android.widget.AutoCompleteTextView$OnDismissListener
+android.widget.CalendarView$OnDateChangeListener
+android.widget.Chronometer$OnChronometerTickListener
+android.widget.CompoundButton$OnCheckedChangeListener
+android.widget.DatePicker$OnDateChangedListener
+android.widget.ExpandableListView$OnChildClickListener
+android.widget.ExpandableListView$OnGroupClickListener
+android.widget.ExpandableListView$OnGroupCollapseListener
+android.widget.ExpandableListView$OnGroupExpandListener
+android.widget.Filter$FilterListener
+android.widget.NumberPicker$OnScrollListener
+android.widget.NumberPicker$OnValueChangeListener
+android.widget.NumberPicker$OnDismissListener
+android.widget.PopupMenu$OnMenuItemClickListenermk
+android.widget.PopupWindow$OnDismissListener
+android.widget.RadioGroup$OnCheckedChangeListener
+android.widget.RatingBar$OnRatingBarChangeListener
+android.widget.SearchView$OnCloseListener
+android.widget.SearchView$OnQueryTextListener
+android.widget.SearchView$OnSuggestionListener
+android.widget.SeekBar$OnSeekBarChangeListener
+android.widget.ShareActionProvider$OnShareTargetSelectedListener
+android.widget.SlidingDrawer$OnDrawerCloseListener
+android.widget.SlidingDrawer$OnDrawerOpenListener
+android.widget.SlidingDrawer$OnDrawerScrollListener
+android.widget.TabHost$OnTabChangeListener
+android.widget.TextView$OnEditorActionListener
+android.widget.TimePicker$OnTimeChangedListener
+android.widget.ZoomButtonsController$OnZoomListener 

src/main/resources/android/EntryPoints.txt

@@ -0,0 +1,155 @@
+%handler
+Landroid/os/Handler; handleMessage(Landroid/os/Message;)V
+%content provider
+Landroid/content/ContentProvider; <init>()V
+Landroid/content/ContentProvider; onCreate()Z
+Landroid/content/ContentProvider; onLowMemory()V
+Landroid/content/ContentProvider; onTrimMemory(I)V
+%application
+Landroid/app/Application; <init>()V
+Landroid/app/Application; onCreate()V
+Landroid/app/Application; onLowMemory()V
+Landroid/app/Application; onTerminate()V
+Landroid/app/Application; onTrimMemory(I)V
+%activity
+Landroid/app/Activity; onCreate(Landroid/os/Bundle;)V
+Landroid/app/Activity; onDestroy()V
+Landroid/app/Activity; <init>()V
+Landroid/app/Activity; <clinit>()V
+Landroid/app/Activity; onResume()V
+Landroid/app/Activity; onStart()V
+Landroid/app/Activity; onStop()V
+Landroid/app/Activity; onPause()V
+Landroid/app/Activity; onRestart()V
+Landroid/app/Activity; onUserLeaveHint()V
+Landroid/app/Activity; onPostResume()V
+Landroid/app/Activity; onNewIntent(Landroid/content/Intent;)V
+Landroid/app/Activity; onPostCreate(Landroid/os/Bundle;)V
+Landroid/app/Activity; onSaveInstanceState(Landroid/os/Bundle;)V
+Landroid/app/Activity; onRestoreInstanceState(Landroid/os/Bundle;)V
+Landroid/app/Activity; onLowMemory()V
+Landroid/app/Activity; onBackPressed()V
+Landroid/app/Activity; onContentChanged()V
+Landroid/app/Activity; onDetachedFromWindow()V
+Landroid/app/Activity; onEnterAnimationComplete()V
+Landroid/app/Activity; onNavigateUp()V
+Landroid/app/Activity; onSearchRequested()V
+Landroid/app/Activity; attachBaseContext(Landroid/content/Context;)V
+Landroid/app/Activity; onActivityResult(IILandroid/content/Intent;)V
+Landroid/support/v7/app/ActionBarActivity; onCreate(Landroid/os/Bundle;)V
+Landroid/support/v7/app/ActionBarActivity; onDestroy()V
+Landroid/support/v7/app/ActionBarActivity; <init>()V
+Landroid/support/v7/app/ActionBarActivity; <clinit>()V
+Landroid/support/v7/app/ActionBarActivity; onResume()V
+Landroid/support/v7/app/ActionBarActivity; onStart()V
+Landroid/support/v7/app/ActionBarActivity; onStop()V
+Landroid/support/v7/app/ActionBarActivity; onPause()V
+Landroid/support/v7/app/ActionBarActivity; onRestart()V
+Landroid/support/v7/app/ActionBarActivity; onUserLeaveHint()V
+Landroid/support/v7/app/ActionBarActivity; onPostResume()V
+Landroid/support/v7/app/ActionBarActivity; onNewIntent(Landroid/content/Intent;)V
+Landroid/support/v7/app/ActionBarActivity; onPostCreate(Landroid/os/Bundle;)V
+Landroid/support/v7/app/ActionBarActivity; onSaveInstanceState(Landroid/os/Bundle;)V
+Landroid/support/v7/app/ActionBarActivity; onRestoreInstanceState(Landroid/os/Bundle;)V
+Landroid/support/v7/app/ActionBarActivity; onLowMemory()V
+Landroid/support/v7/app/ActionBarActivity; onBackPressed()V
+Landroid/support/v7/app/ActionBarActivity; onContentChanged()V
+Landroid/support/v7/app/ActionBarActivity; onDetachedFromWindow()V
+Landroid/support/v7/app/ActionBarActivity; onEnterAnimationComplete()V
+Landroid/support/v7/app/ActionBarActivity; onNavigateUp()V
+Landroid/support/v7/app/ActionBarActivity; onSearchRequested()V
+Landroid/support/v7/app/ActionBarActivity; attachBaseContext(Landroid/content/Context;)V
+Landroid/support/v7/app/ActionBarActivity; onActivityResult(IILandroid/content/Intent;)V
+%service
+Landroid/app/Service; onBind(Landroid/content/Intent;)Landroid/os/IBinder;
+Landroid/app/Service; onConfigurationChanged(Landroid/content/res/Configuration;)V
+Landroid/app/Service; onCreate()V
+Landroid/app/Service; onDestroy()V
+Landroid/app/Service; onLowMemory()V
+Landroid/app/Service; onDestroy()V
+Landroid/app/Service; onRebind(Landroid/content/Intent;)V
+Landroid/app/Service; onStart(Landroid/content/Intent;I)V
+Landroid/app/Service; onStartCommand(Landroid/content/Intent;II)I
+Landroid/app/Service; onTaskRemoved(Landroid/content/Intent;)V
+Landroid/app/Service; onTrimMemory(I)V
+Landroid/app/Service; onUnbind(Landroid/content/Intent;)Z
+Landroid/app/Service; <init>()V
+Landroid/app/Service; <clinit>()V
+%broadcast receiver
+Landroid/content/BroadcastReceiver; onReceive(Landroid/content/Context;Landroid/content/Intent;)V
+Landroid/content/BroadcastReceiver; <init>()V
+Landroid/content/BroadcastReceiver; <clinit>()V
+%fragment
+Landroid/app/Fragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/app/Fragment; onCreate(Landroid/os/Bundle;)V
+Landroid/app/Fragment; onDestroy()V
+Landroid/app/Fragment; onDestroyOptionsMenu()V
+Landroid/app/Fragment; onDetach()V
+Landroid/app/Fragment; onLowMemory()V
+Landroid/app/Fragment; onPause()V
+Landroid/app/Fragment; onResume()V
+Landroid/app/Fragment; onStart()V
+Landroid/app/Fragment; onStop()V
+Landroid/app/Fragment; onTrimMemory(I)V
+Landroid/app/Fragment; <init>()V
+Landroid/app/Fragment; <clinit>()V
+Landroid/app/Fragment; onAttach(Landroid/app/Activity;)V
+Landroid/support/v4/app/FragmentActivity; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/support/v4/app/FragmentActivity; onCreate(Landroid/os/Bundle;)V
+Landroid/support/v4/app/FragmentActivity; onDestroy()V
+Landroid/support/v4/app/FragmentActivity; onDestroyOptionsMenu()V
+Landroid/support/v4/app/FragmentActivity; onDetach()V
+Landroid/support/v4/app/FragmentActivity; onLowMemory()V
+Landroid/support/v4/app/FragmentActivity; onPause()V
+Landroid/support/v4/app/FragmentActivity; onResume()V
+Landroid/support/v4/app/FragmentActivity; onStart()V
+Landroid/support/v4/app/FragmentActivity; onStop()V
+Landroid/support/v4/app/FragmentActivity; onTrimMemory(I)V
+Landroid/support/v4/app/FragmentActivity; <init>()V
+Landroid/support/v4/app/FragmentActivity; <clinit>()V
+Landroid/support/v4/app/FragmentActivity; onAttach(Landroid/app/Activity;)V
+Landroid/support/v4/app/Fragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/support/v4/app/Fragment; onCreate(Landroid/os/Bundle;)V
+Landroid/support/v4/app/Fragment; onDestroy()V
+Landroid/support/v4/app/Fragment; onDestroyOptionsMenu()V
+Landroid/support/v4/app/Fragment; onDetach()V
+Landroid/support/v4/app/Fragment; onLowMemory()V
+Landroid/support/v4/app/Fragment; onPause()V
+Landroid/support/v4/app/Fragment; onResume()V
+Landroid/support/v4/app/Fragment; onStart()V
+Landroid/support/v4/app/Fragment; onStop()V
+Landroid/support/v4/app/Fragment; onTrimMemory(I)V
+Landroid/support/v4/app/Fragment; <init>()V
+Landroid/support/v4/app/Fragment; <clinit>()V
+Landroid/support/v4/app/Fragment; onAttach(Landroid/app/Activity;)V
+%list fragment
+Landroid/app/ListFragment; <init>()V
+Landroid/app/ListFragment; <clinit>()V
+Landroid/app/ListFragment; onAttach(Landroid/app/Activity;)V
+Landroid/app/ListFragment; onCreate(Landroid/os/Bundle;)V
+Landroid/app/ListFragment; onListItemClick(Landroid/widget/ListView;Landroid/view/View;IJ)V
+Landroid/app/ListFragment; onStart()V
+Landroid/app/ListFragment; onStop()V
+Landroid/app/ListFragment; onDetach()V
+Landroid/app/ListFragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/app/ListFragment; onTrimMemory(I)V
+Landroid/app/ListFragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/app/ListFragment; onDestroy()V
+Landroid/app/ListFragment; onDestroyOptionsMenu()V
+Landroid/app/ListFragment; onPause()V
+Landroid/app/ListFragment; onResume()V
+Landroid/support/v4/app/ListFragment; <init>()V
+Landroid/support/v4/app/ListFragment; <clinit>()V
+Landroid/support/v4/app/ListFragment; onAttach(Landroid/app/Activity;)V
+Landroid/support/v4/app/ListFragment; onCreate(Landroid/os/Bundle;)V
+Landroid/support/v4/app/ListFragment; onListItemClick(Landroid/widget/ListView;Landroid/view/View;IJ)V
+Landroid/support/v4/app/ListFragment; onStart()V
+Landroid/support/v4/app/ListFragment; onStop()V
+Landroid/support/v4/app/ListFragment; onDetach()V
+Landroid/support/v4/app/ListFragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/support/v4/app/ListFragment; onTrimMemory(I)V
+Landroid/support/v4/app/ListFragment; onActivityCreated(Landroid/os/Bundle;)V
+Landroid/support/v4/app/ListFragment; onDestroy()V
+Landroid/support/v4/app/ListFragment; onDestroyOptionsMenu()V
+Landroid/support/v4/app/ListFragment; onPause()V
+Landroid/support/v4/app/ListFragment; onResume()V

src/main/scala/Main.scala

@@ -0,0 +1,91 @@
+import java.io.{File, PrintWriter}
+import java.time.{Duration, Instant, LocalTime}
+import java.util
+
+import analysis.{Analyzer, PreAnalyzer}
+import ch.qos.logback.classic.{Level, Logger}
+import com.microsoft.z3._
+import com.typesafe.scalalogging.StrictLogging
+import constraints.Z3Constraint
+import domain._
+import org.slf4j.LoggerFactory
+import parser.Parser
+
+object Main extends App with StrictLogging {
+
+  val help = """Usage:
+    -apk=FILE     Apk file to analyze
+    -print-rules  Print the textual description of the constraints
+    -print-goal   Print the Z3 goal
+    """
+
+  // Check parameters
+  if (args.length == 0) {
+    println(help)
+    System.exit(1)
+  }
+  val apkArg = args.find(a => a.startsWith("-apk"))
+  if (apkArg.isEmpty) {
+    println("No apk given")
+    System.exit(1)
+  }
+  val apkLocation: String = apkArg.get.split("=")(1)
+  val printRules: Boolean = args.exists(a => a.startsWith("-print-rules"))
+  val printGoal: Boolean = args.exists(a => a.startsWith("-print-goal"))
+
+  val parser = new Parser(apkLocation)
+  var start = Instant.now()
+  logger.info(s"Start: ${LocalTime.now()}")
+
+  // Context
+  val cfg = new util.HashMap[String, String]
+  cfg.put("model", "true")
+  val ctx = new Context(cfg)
+  // Goal
+  val g = ctx.mkGoal(true, false, false)
+
+  val domainsCollection =
+    AbstractDomainsCollection(
+      new TopDomain(ctx),
+      new ReferenceDomain(ctx),
+      new TaintDomain(ctx)
+    )
+  val app = parser.dexApp
+  val preAnalysisResult = new PreAnalyzer(app.classes).analyze
+  val analyzer =
+    new Analyzer(ctx, domainsCollection, app, preAnalysisResult)
+  val constraints: Seq[Z3Constraint] = analyzer.analyze
+  g.add(
+    ctx.mkAnd(
+      constraints.map(c => c.boolExpr): _*
+    )
+  )
+  if (printRules) {
+    println("Rules:")
+    println(
+      constraints
+        .map(c => s"${c.pp.m.shortName}-${c.pp.pc} ${c.description}")
+        .mkString("\n")
+    )
+  }
+  if (printGoal) {
+    println("Goal:")
+    println(g)
+  }
+  var end = Instant.now()
+  logger.info(
+    s"Time to generate goal: ${Duration.between(start, end).getSeconds} seconds")
+  start = Instant.now()
+  val solver = ctx.mkSolver
+  g.getFormulas.foreach(solver.add(_))
+  val status = solver.check()
+  end = Instant.now()
+  logger.info(
+    s"Time to check goal: ${Duration.between(start, end).getSeconds} seconds")
+  status match {
+    case Status.SATISFIABLE   => println("OK")
+    case Status.UNSATISFIABLE => println("LEAK")
+    case Status.UNKNOWN       => println(s"UNKNOWN: ${solver.getReasonUnknown}")
+  }
+
+}

src/main/scala/analysis/Analyzer.scala

@@ -0,0 +1,158 @@
+package analysis
+
+import com.microsoft.z3._
+import com.typesafe.scalalogging.StrictLogging
+import constraints.Z3Constraint
+import dex.{DexApp, DexClass, DexMethod}
+import domain.AbstractDomainsCollection
+import org.jf.dexlib2.Opcode
+import org.jf.dexlib2.iface.instruction.Instruction
+import org.jf.dexlib2.iface.instruction.formats._
+
+import scala.collection.mutable.ArrayBuffer
+
+class Analyzer(
+    ctx: Context,
+    domains: AbstractDomainsCollection,
+    app: DexApp,
+    preAnalysisResult: PreAnalysisResult
+) extends StrictLogging {
+
+  /**
+    * Methods to analyze. This collection is populated while analyzing each instruction.
+    */
+  private var methodsToAnalyze: ArrayBuffer[(DexClass, DexMethod)] =
+    ArrayBuffer[(DexClass, DexMethod)]()
+
+  /**
+    * Analyze the program.
+    * @return the z3 constraints.
+    */
+  def analyze: Seq[Z3Constraint] = {
+    /*
+      Add all the entry points (from both manifest and callbacks)
+      to the methods to analyze.
+     */
+    val entryPoints = app.manifest.entryPoints ++ app.entryPoints
+    methodsToAnalyze = ArrayBuffer(entryPoints: _*)
+    val env = new Environment(ctx, domains, app, preAnalysisResult)
+    analyzeAux(env, 0, List())
+  }
+
+  /**
+    * Analyze the methods, starting from the given index, until there are no more methods to analyze.
+    */
+  def analyzeAux(env: Environment,
+                 index: Int,
+                 constraints: Seq[Z3Constraint]): Seq[Z3Constraint] = {
+    if (index >= methodsToAnalyze.length) {
+      // No more methods to analyze.
+      return constraints
+    }
+    val (c, m) = methodsToAnalyze(index)
+    logger.debug(s"Analyzing method '${m.name}' of class '${c.name}'")
+    val newConstraints: Seq[Z3Constraint] =
+      m.instructions.zipWithIndex.flatMap {
+        case (i: Instruction, pc: Int) =>
+          logger.info(s"$pc - ${i.getOpcode}")
+          val pp = PP(c, m, pc)
+          i.getOpcode match {
+            case Opcode.CONST_4 =>
+              InstructionAnalyzer.const4(
+                i.asInstanceOf[Instruction11n],
+                pp,
+                env
+              )
+            case Opcode.CONST_STRING =>
+              InstructionAnalyzer.constString(
+                i.asInstanceOf[Instruction21c],
+                pp,
+                env
+              )
+            case Opcode.CONST_STRING_JUMBO =>
+              InstructionAnalyzer.constStringJumbo(
+                i.asInstanceOf[Instruction31c],
+                pp,
+                env
+              )
+            case Opcode.IPUT =>
+              InstructionAnalyzer.iput(
+                i.asInstanceOf[Instruction22c],
+                pp,
+                env
+              )
+            case Opcode.SGET_OBJECT =>
+              InstructionAnalyzer.sgetObject(
+                i.asInstanceOf[Instruction21c],
+                pp,
+                env
+              )
+            case Opcode.SPUT_OBJECT =>
+              InstructionAnalyzer.sputObject(
+                i.asInstanceOf[Instruction21c],
+                pp,
+                env
+              )
+            case Opcode.MOVE_OBJECT =>
+              InstructionAnalyzer.move(
+                i.asInstanceOf[Instruction12x],
+                pp,
+                env
+              )
+            case Opcode.MOVE_RESULT | Opcode.MOVE_RESULT_OBJECT =>
+              InstructionAnalyzer.moveResult(
+                i.asInstanceOf[Instruction11x],
+                pp,
+                env
+              )
+            case Opcode.IF_EQ =>
+              InstructionAnalyzer.ifEq(i.asInstanceOf[Instruction22t], pp, env)
+            case Opcode.IF_NE =>
+              InstructionAnalyzer.ifEq(i.asInstanceOf[Instruction22t], pp, env)
+            case Opcode.GOTO =>
+              InstructionAnalyzer.goto(i.asInstanceOf[Instruction10t], pp, env)
+            case Opcode.NEW_INSTANCE =>
+              InstructionAnalyzer.newInstance(
+                i.asInstanceOf[Instruction21c],
+                pp,
+                env
+              )
+            case Opcode.INVOKE_DIRECT =>
+              InstructionAnalyzer.invokeDirect(
+                i.asInstanceOf[Instruction35c],
+                pp,
+                env,
+                (c, m) => this.addMethodToAnalyze(c, m)
+              )
+            case Opcode.INVOKE_VIRTUAL =>
+              InstructionAnalyzer.invokeVirtual(
+                i.asInstanceOf[Instruction35c],
+                pp,
+                env,
+                (c, m) => this.addMethodToAnalyze(c, m)
+              )
+            case Opcode.RETURN_VOID =>
+              InstructionAnalyzer.retVoid(
+                i.asInstanceOf[Instruction10x],
+                pp,
+                env
+              )
+            case Opcode.RETURN =>
+              InstructionAnalyzer.ret(i.asInstanceOf[Instruction11x], pp, env)
+            case Opcode.CHECK_CAST | Opcode.MOVE_EXCEPTION =>
+              InstructionAnalyzer.nop(i, pp, env)
+            case _ =>
+              logger.warn(s"Not implemented: ${i.getOpcode}, changed to NOP")
+              InstructionAnalyzer.nop(i, pp, env)
+          }
+      }
+    analyzeAux(env, index + 1, constraints ++ newConstraints)
+  }
+
+  private def addMethodToAnalyze(dexClass: DexClass,
+                                 dexMethod: DexMethod): Unit =
+    if (!methodsToAnalyze.contains((dexClass, dexMethod))) {
+      methodsToAnalyze += ((dexClass, dexMethod))
+    }
+
+}

src/main/scala/analysis/Environment.scala

@@ -0,0 +1,334 @@
+package analysis
+
+import com.microsoft.z3._
+import dex.DexType.{ObjectType, PrimitiveType, VoidType}
+import dex.{DexApp, DexClass, DexField, DexMethod}
+import domain.{AbstractDomain, AbstractDomainsCollection}
+
+/**
+  * Environment for the analysis.
+  */
+class Environment(
+    val ctx: Context,
+    val domains: AbstractDomainsCollection,
+    val app: DexApp,
+    val preAnalysisResult: PreAnalysisResult
+) {
+
+  val z3Obj = new Z3Object(ctx, domains)
+
+  /**
+    * Abstract registers.
+    */
+  object R {
+
+    /**
+      * Index of the ret register.
+      */
+    val retIdx: Int = -1
+
+    /**
+      * Approximation of a register.
+      */
+    class RApprox(
+        val numApprox: BoolExpr,
+        val referenceApprox: BoolExpr,
+        val taintApprox: BoolExpr
+    ) {}
+
+    /**
+      * Register at a program point.
+      */
+    class RAtPP(
+        private val regCount: Int,
+        val numbers: Int => domains.primitiveDomain.Element,
+        val references: Int => domains.referenceDomain.Element,
+        val taints: Int => domains.taintDomain.Element,
+    ) {
+
+      /**
+        * Approximate the register to top (taint excluded).
+        * @param i index of the register.
+        * @return a register approximation.
+        */
+      def top(i: Int): RApprox =
+        new RApprox(
+          domains.primitiveDomain.approx(
+            domains.primitiveDomain.top,
+            this.numbers(i),
+          ),
+          domains.referenceDomain.approx(
+            domains.referenceDomain.top,
+            this.references(i),
+          ),
+          ctx.mkTrue()
+        )
+
+      /**
+        * Approximate a register to another.
+        * @param i index of the register that must be approximated.
+        * @param j index of the register that must approximates.
+        * @param r register at the desired program point.
+        * @return a register approximation.
+        */
+      def <=(i: Int, j: Int)(r: RAtPP): RApprox =
+        new RApprox(
+          domains.primitiveDomain.approx(
+            this.numbers(i),
+            r.numbers(j)
+          ),
+          domains.referenceDomain.approx(
+            this.references(i),
+            r.references(j)
+          ),
+          domains.taintDomain.approx(
+            this.taints(i),
+            r.taints(j)
+          )
+        )
+
+      /**
+        * Approximate all the registers between two program points.
+        * @param r registers at the desider program point.
+        * @return registers approximations.
+        */
+      def <=(r: RAtPP): List[RApprox] =
+        (-1 until this.regCount)
+          .map(i => this.<=(i, i)(r))
+          .toList
+
+      /**
+        * Approximate all the registers between two program points except for the register at the given index.
+        * @param n index of the register to exclude.
+        * @param r registers at the desider program point.
+        * @return registers approximations.
+        */
+      def <=(n: Int)(r: RAtPP): List[RApprox] =
+        (-1 until this.regCount)
+          .filter(i => i != n)
+          .map(i => this.<=(i, i)(r))
+          .toList
+
+    }
+
+    /**
+      * Returns the registers at the given program points.
+      * @param pp the program point.
+      * @return the registers.
+      */
+    def apply(pp: PP): RAtPP =
+      new RAtPP(
+        pp.m.registersCount,
+        rTypeAtPP(pp, domains.primitiveDomain, "R-prim"),
+        rTypeAtPP(pp, domains.referenceDomain, "R-ref"),
+        rTypeAtPP(pp, domains.taintDomain, "R-taint")
+      )
+
+    /**
+      * Returns a function that maps a register index to the given domain Element.
+      * @param pp program point of the registers.
+      * @param domain the chosen domain.
+      * @param prefix prefix to distinguish between Elements of different domains.
+      * @tparam E the domain Element type.
+      * @return function that maps the index to the Element.
+      */
+    private def rTypeAtPP[E](
+        pp: PP,
+        domain: AbstractDomain,
+        prefix: String
+    ): Int => E =
+      (i) =>
+        ctx
+          .mkApp(
+            ctx.mkFuncDecl(
+              s"$prefix-${pp.c.name}-${pp.m.name}-${pp.pc}",
+              Array[Sort](ctx.mkIntSort()),
+              domain.sort
+            ),
+            ctx.mkInt(i)
+          )
+          .asInstanceOf[E]
+
+    /**
+      * Convert a list of registers approximations into a list of Z3 constraints.
+      */
+    implicit def toBoolExpr(approxMap: List[RApprox]): List[BoolExpr] =
+      approxMap
+        .flatMap(v => toBoolExpr(v))
+
+    /**
+      * Convert a register approximation into a list of Z3 constraints.
+      */
+    implicit def toBoolExpr(approx: RApprox): List[BoolExpr] =
+      List(approx.numApprox, approx.referenceApprox, approx.taintApprox)
+
+  }
+
+  /**
+    * Abstract heap.
+    */
+  object H {
+
+    /**
+      * Returns the heap that maps references to objects.
+      */
+    def obj(): FuncDecl = {
+      val z3Obj = new Z3Object(ctx, domains)
+      ctx.mkFuncDecl(
+        "H",
+        Array[Sort](ctx.mkStringSort()),
+        z3Obj.sort
+      )
+    }
+  }
+
+  /**
+    * Abstract static heap.
+    */
+  object SH {
+
+    /**
+      * Returns the class field value.
+      * @param dexClass the class.
+      * @param dexField the field.
+      * @return a tuple where the first element is the value and the second the taint.
+      */
+    def apply(dexClass: DexClass, dexField: DexField): (Expr, Expr) = {
+      (
+        dexField.dexType match {
+          case PrimitiveType() =>
+            const(dexClass, dexField, domains.primitiveDomain.sort, "SH-prim")
+          case ObjectType(_) =>
+            const(dexClass, dexField, domains.referenceDomain.sort, "SH-ref")
+        },
+        const(dexClass, dexField, domains.taintDomain.sort, "SH-taint")
+      )
+    }
+
+    /**
+      * Returns the constant that represent the class field.
+      * @param dexClass the class.
+      * @param dexField the field.
+      * @param sort the type of the constant domain.
+      * @param prefix prefix to distinguish between the same constant in different domains.
+      * @return the constant.
+      */
+    private def const(
+        dexClass: DexClass,
+        dexField: DexField,
+        sort: Sort,
+        prefix: String
+    ): Expr = {
+      ctx.mkConst(s"$prefix-${dexClass.name}-${dexField.name}", sort)
+    }
+  }
+
+  /**
+    * Method return value.
+    */
+  object M {
+
+    /**
+      * Value returned by the given class method.
+      * @param dexClass the class.
+      * @param dexMethod the method.
+      * @return the value.
+      */
+    def apply(dexClass: DexClass, dexMethod: DexMethod): Option[Expr] = {
+      dexMethod.returnType match {
+        case PrimitiveType() =>
+          Option(
+            typeReturn(
+              dexClass,
+              dexMethod,
+              domains.primitiveDomain.sort,
+              "M-prim"
+            )
+          )
+        case ObjectType(_) =>
+          Option(
+            typeReturn(
+              dexClass,
+              dexMethod,
+              domains.referenceDomain.sort,
+              "M-ref"
+            )
+          )
+        case VoidType() => Option.empty
+      }
+    }
+
+    /**
+      * Method result in the given domain.
+      */
+    private def typeReturn(
+        dexClass: DexClass,
+        dexMethod: DexMethod,
+        sort: Sort,
+        prefix: String
+    ): Expr = {
+      ctx.mkConst(
+        s"$prefix-${dexClass.name}-${dexMethod.name}",
+        sort
+      )
+    }
+
+  }
+
+  /**
+    * Method invocation helper.
+    */
+  object Dispatch {
+
+    /**
+      * Returns a map where the key is the class that has the given
+      * method, either because it implements it or because it is inherited,
+      * and the value is the corresponding class with the method implementation.
+      */
+    def apply(dexMethod: String,
+              definingClass: String): Map[DexClass, DexClass] = {
+      dispatchAux(dexMethod, definingClass).toMap
+    }
+
+    /**
+      * Tail recursive search of method implementations.
+      */
+    private def dispatchAux(
+        dexMethod: String,
+        definingClass: String): Seq[(DexClass, DexClass)] = {
+      val defClass = app.classes.find(c => c.name == definingClass)
+      val impl: Option[DexClass] =
+        defClass match {
+          case Some(c) => firstImpl(dexMethod, c)
+          case None    => Option.empty
+        }
+      val impls = app.classes
+        .filter(c => c.superClass == definingClass)
+        .flatMap(
+          c => dispatchAux(dexMethod, c.name)
+        )
+        .toList
+      impl match {
+        case Some(c) => (defClass.get -> c) :: impls
+        case None    => impls
+      }
+    }
+
+    /**
+      * Returns the first implementation (if present) of the given method when invoked to the given class.
+      */
+    private def firstImpl(dexMethod: String,
+                          dexClass: DexClass): Option[DexClass] = {
+      dexClass.methods.find(m => m.name == dexMethod) match {
+        case Some(_) => Option(dexClass)
+        case None =>
+          app.classes.find(c => c.name == dexClass.superClass) match {
+            case Some(c) => firstImpl(dexMethod, c)
+            case None    => Option.empty
+          }
+      }
+    }
+
+  }
+
+}

src/main/scala/analysis/InstructionAnalyzer.scala

@@ -0,0 +1,842 @@
+package analysis
+
+import com.microsoft.z3._
+import com.typesafe.scalalogging.StrictLogging
+import constraints.Z3Constraint
+import dex.DexType.{PrimitiveType, ObjectType, VoidType}
+import dex.{DexClass, DexMethod, DexType}
+import org.jf.dexlib2.dexbacked.reference.{
+  DexBackedStringReference,
+  DexBackedTypeReference
+}
+import org.jf.dexlib2.iface.instruction.Instruction
+import org.jf.dexlib2.iface.instruction.formats._
+import org.jf.dexlib2.iface.reference.MethodReference
+import utils.Utils
+
+object InstructionAnalyzer extends StrictLogging {
+
+  /**
+    * Do nothing. All registers at pp+ approximates the registers at pp.
+    */
+  def nop(i: Instruction, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(r <= rPlus: _*),
+        s"R($pp) <= R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def const4(i: Instruction11n, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val rApprox = r.<=(i.getRegisterA)(rPlus)
+    Seq(
+      Z3Constraint(
+        env.domains.primitiveDomain.approx(
+          env.domains.primitiveDomain.toElement(i.getWideLiteral.toInt),
+          rPlus.numbers(i.getRegisterA)
+        ),
+        s"${i.getWideLiteral} <= R(${pp +})(${i.getRegisterA})",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(rApprox: _*),
+        s"R($pp) <={${i.getRegisterA}} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def constString(i: Instruction21c,
+                  pp: PP,
+                  env: Environment): Seq[Z3Constraint] = {
+    constString(
+      i.getRegisterA,
+      i.getReference.asInstanceOf[DexBackedStringReference].getString,
+      pp,
+      env
+    )
+  }
+
+  def constStringJumbo(i: Instruction31c,
+                       pp: PP,
+                       env: Environment): Seq[Z3Constraint] = {
+    constString(
+      i.getRegisterA,
+      i.getReference.asInstanceOf[DexBackedStringReference].getString,
+      pp,
+      env
+    )
+  }
+
+  /**
+    * Make the register A approximates str.
+    * Constant strings are treated like instances of Ljava/lang/String;
+    */
+  private def constString(registerA: Int,
+                          str: String,
+                          pp: PP,
+                          env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    Seq(
+      Z3Constraint(
+        env.domains.referenceDomain.approx(
+          env.domains.referenceDomain.toElement(pp.toString),
+          rPlus.references(registerA)
+        ),
+        s"($pp) <= R(${pp +})($registerA)",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(r.<=(registerA)(rPlus): _*),
+        s"R($pp) <={$registerA} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def iput(i: Instruction22c, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val rApprox = r.<=(rPlus)
+    val fieldRef = i.getReference.toString
+    val cName = Utils.classPrefix(fieldRef)
+    val fieldName = Utils.removeClassPrefix(fieldRef)
+    val fieldType = DexType(fieldName.substring(fieldName.indexOf(":") + 1))
+    val classes = classAndSubclasses(env)(cName)
+    val obj: FuncDecl = env.H.obj()
+    val objApp = env.ctx.mkApp(obj, env.ctx.mkString(pp.toString))
+    val accessor: FuncDecl = fieldType match {
+      case PrimitiveType() =>
+        env.z3Obj.primAccessor
+    }
+    val objFields =
+      env.ctx.mkApp(accessor, objApp).asInstanceOf[ArrayExpr]
+    val constraints: Seq[Z3Constraint] = classes.flatMap(
+      c =>
+        env.preAnalysisResult.objectCreation
+          .filter(p => p._2 == c.name)
+          .map(objPP => {
+            Z3Constraint(
+              env.ctx.mkImplies(
+                env.ctx.mkAnd(
+                  env.domains.referenceDomain.approx(
+                    env.domains.referenceDomain.toElement(objPP._1.toString),
+                    r.references(i.getRegisterB)
+                  )
+                ),
+                fieldType match {
+                  case PrimitiveType() =>
+                    env.domains.primitiveDomain.approx(
+                      r.numbers(i.getRegisterA),
+                      env.ctx
+                        .mkSelect(objFields, env.ctx.mkString(fieldName))
+                        .asInstanceOf[env.domains.primitiveDomain.Element]
+                    )
+                }
+              ),
+              s"${objPP._1.toString} <= R($pp)(${i.getRegisterB}) => " +
+                s"R($pp)(${i.getRegisterA}) <= H($objPP).$fieldName",
+              pp
+            )
+          })
+    )
+    constraints ++ Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(rApprox: _*),
+        s"R($pp) <= R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def sgetObject(i: Instruction21c,
+                 pp: PP,
+                 env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val sFieldRef = i.getReference.toString
+    val cName = Utils.classPrefix(sFieldRef)
+    val sFieldName = Utils.removeClassPrefix(sFieldRef)
+    val sFieldType = DexType(sFieldName.substring(sFieldName.indexOf(":") + 1))
+    val dexClass = env.app.classes.find(c => c.name == cName)
+    val (sFieldVal, sFieldTaint): (Expr, Expr) = dexClass match {
+      case Some(c) =>
+        val f = c.fields.find(dexField => dexField.name == sFieldName).get
+        env.SH(c, f)
+      case None =>
+        // Unknown class, use top as value.
+        sFieldType match {
+          case PrimitiveType() =>
+            (env.domains.primitiveDomain.top, env.domains.taintDomain.top)
+          case ObjectType(_) =>
+            (env.domains.referenceDomain.top, env.domains.taintDomain.top)
+        }
+    }
+    Seq(
+      Z3Constraint(
+        sFieldType match {
+          case PrimitiveType() =>
+            env.domains.primitiveDomain.approx(
+              sFieldVal.asInstanceOf[env.domains.primitiveDomain.Element],
+              rPlus.numbers(i.getRegisterA)
+            )
+          case ObjectType(_) =>
+            env.domains.referenceDomain.approx(
+              sFieldVal.asInstanceOf[env.domains.referenceDomain.Element],
+              rPlus.references(i.getRegisterA)
+            )
+        },
+        s"SH($cName,$sFieldName) <= R(${pp +})(${i.getRegisterA})",
+        pp
+      ),
+      Z3Constraint(
+        env.domains.taintDomain.approx(
+          sFieldTaint.asInstanceOf[env.domains.taintDomain.Element],
+          rPlus.taints(i.getRegisterA)
+        ),
+        s"Taint R($pp)(${i.getRegisterA}) if SH($cName,$sFieldName) is tainted",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(r.<=(i.getRegisterA)(rPlus): _*),
+        s"R($pp) <={${i.getRegisterA}} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def sputObject(i: Instruction21c,
+                 pp: PP,
+                 env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val sFieldRef = i.getReference.toString
+    val cName = Utils.classPrefix(sFieldRef)
+    val sFieldName = Utils.removeClassPrefix(sFieldRef)
+    val sFieldType = DexType(sFieldName.substring(sFieldName.indexOf(":") + 1))
+    val dexClass = env.app.classes.find(c => c.name == cName)
+    val (sFieldVal, sFieldTaint): (Expr, Expr) = dexClass match {
+      case Some(c) =>
+        val f = c.fields.find(dexField => dexField.name == sFieldName).get
+        env.SH(c, f)
+      case None =>
+        // Unknown class, use top as value.
+        sFieldType match {
+          case PrimitiveType() =>
+            (env.domains.primitiveDomain.top, env.domains.taintDomain.top)
+          case ObjectType(_) =>
+            (env.domains.referenceDomain.top, env.domains.taintDomain.top)
+        }
+    }
+    Seq(
+      Z3Constraint(
+        sFieldType match {
+          case PrimitiveType() =>
+            env.domains.primitiveDomain.approx(
+              r.numbers(i.getRegisterA),
+              sFieldVal.asInstanceOf[env.domains.primitiveDomain.Element]
+            )
+          case ObjectType(_) =>
+            env.domains.referenceDomain.approx(
+              r.references(i.getRegisterA),
+              sFieldVal.asInstanceOf[env.domains.referenceDomain.Element]
+            )
+        },
+        s"R($pp)(${i.getRegisterA}) <= SH($cName,$sFieldName)",
+        pp
+      ),
+      Z3Constraint(
+        env.domains.taintDomain.approx(
+          r.taints(i.getRegisterA),
+          sFieldTaint.asInstanceOf[env.domains.taintDomain.Element]
+        ),
+        s"Taint SH($cName,$sFieldName) if R($pp)(${i.getRegisterA}) is tainted",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(r <= rPlus: _*),
+        s"R($pp) <= R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def move(i: Instruction12x, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val rApprox = r.<=(i.getRegisterA)(rPlus)
+    Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(
+          r.<=(i.getRegisterB, i.getRegisterA)(rPlus): _*
+        ),
+        s"R($pp)(${i.getRegisterB}) <= R(${pp +})(${i.getRegisterA})",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(rApprox: _*),
+        s"R($pp) <={${i.getRegisterA}} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def moveResult(i: Instruction11x,
+                 pp: PP,
+                 env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val rApprox = r.<=(i.getRegisterA)(rPlus)
+    Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(
+          r.<=(env.R.retIdx, i.getRegisterA)(rPlus): _*
+        ),
+        s"R($pp)(ret) <= R(${pp +})(${i.getRegisterA})",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(rApprox: _*),
+        s"R($pp) <={${i.getRegisterA}} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def goto(i: Instruction10t, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val ppGoto = pp.copy(pc = pp.pc + i.getCodeOffset)
+    Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(env.R(pp) <= env.R(ppGoto): _*),
+        s"$pp: R($pp) <= R($ppGoto)",
+        pp
+      )
+    )
+  }
+
+  def retVoid(i: Instruction10x,
+              pp: PP,
+              env: Environment): Seq[Z3Constraint] = {
+    Seq()
+  }
+
+  def ret(i: Instruction11x, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val mResult = env.M(pp.c, pp.m).get
+    pp.m.returnType match {
+      case PrimitiveType() =>
+        Seq(
+          Z3Constraint(
+            env.domains.primitiveDomain.approx(
+              r.numbers(i.getRegisterA),
+              mResult.asInstanceOf[env.domains.primitiveDomain.Element]
+            ),
+            s"$pp: R($pp)(${i.getRegisterA}) <= M(${pp.c.name}, ${pp.m.name})",
+            pp
+          )
+        )
+    }
+  }
+
+  def ifEq(i: Instruction22t, pp: PP, env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val ppGoto = pp.copy(pc = pp.pc + i.getCodeOffset)
+    Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(r <= env.R(ppGoto): _*),
+        s"$pp: R($pp) <= R(${pp +})",
+        pp
+      ),
+      Z3Constraint(
+        env.ctx.mkAnd(r <= env.R(pp +): _*),
+        s"$pp: R($pp) <= R($ppGoto)",
+        pp
+      )
+    )
+  }
+
+  def newInstance(i: Instruction21c,
+                  pp: PP,
+                  env: Environment): Seq[Z3Constraint] = {
+    val r = env.R(pp)
+    val objType = i.getReference.asInstanceOf[DexBackedTypeReference].getType
+    val obj: FuncDecl = env.H.obj()
+    val objApp = env.ctx.mkApp(obj, env.ctx.mkString(pp.toString))
+    val objName =
+      env.ctx.mkApp(env.z3Obj.nameAccessor, objApp).asInstanceOf[SeqExpr]
+    val primFields =
+      env.ctx.mkApp(env.z3Obj.primAccessor, objApp).asInstanceOf[ArrayExpr]
+    val fieldsInitialization: List[Z3Constraint] =
+      env.app.classes.find(c => c.name == objType) match {
+        case Some(dexClass) =>
+          dexClass.fields
+            .map(dexField =>
+              dexField.dexType match {
+                case PrimitiveType() =>
+                  Z3Constraint(
+                    env.domains.primitiveDomain.approx(
+                      env.domains.primitiveDomain.toElement(0),
+                      env.ctx
+                        .mkSelect(primFields, env.ctx.mkString(dexField.name))
+                        .asInstanceOf[env.domains.primitiveDomain.Element]
+                    ),
+                    s"0 <= H($pp).${dexField.name}",
+                    pp
+                  )
+                case ObjectType(_) =>
+                  Z3Constraint(
+                    env.ctx.mkTrue(),
+                    "true",
+                    pp
+                  )
+            })
+            .toList
+        case None => List()
+      }
+    val instanceClass = Z3Constraint(
+      env.ctx.mkEq(objName, env.ctx.mkString(objType)),
+      s"H($pp) = {'$objType',(f->_)^*}",
+      pp
+    )
+    val rPlus = env.R(pp +)
+    // Register A of pp+ contains the object pointer (pp).
+    val storeReference =
+      Z3Constraint(
+        env.domains.referenceDomain.approx(
+          env.domains.referenceDomain.toElement(pp.toString),
+          rPlus.references(i.getRegisterA)
+        ),
+        s"($pp) <= R(${pp +})(${i.getRegisterA})",
+        pp
+      )
+    val regApprox = Z3Constraint(
+      env.ctx.mkAnd(r.<=(i.getRegisterA)(rPlus): _*),
+      s"R($pp) <={${i.getRegisterA}} R(${pp +})",
+      pp
+    )
+    Seq(
+      instanceClass,
+      storeReference,
+      regApprox
+    ) ++ fieldsInitialization
+  }
+
+  private def approxParam(env: Environment)(
+      pp: PP,
+      register: Int,
+      dexClass: DexClass,
+      dexMethod: DexMethod,
+      paramIdx: Int
+  ): Z3Constraint = {
+    val r = env.R(pp)
+    val ppMethod = PP(dexClass, dexMethod, 0)
+    val rMethod = env.R(ppMethod)
+    val methodParamIdx = dexMethod.localRegistersCount + paramIdx
+    Z3Constraint(
+      env.ctx.mkAnd(
+        r.<=(register, methodParamIdx)(rMethod): _*
+      ),
+      s"R($pp)($register) <= R($ppMethod)($methodParamIdx)",
+      pp
+    )
+  }
+
+  private def approxParameters(env: Environment)(
+      i: Instruction35c,
+      pp: PP,
+      dexClass: DexClass,
+      dexMethod: DexMethod): List[Z3Constraint] = {
+    var paramApprox: List[Z3Constraint] = List()
+    val regCount = i.getRegisterCount
+    if (regCount > 1) {
+      paramApprox = approxParam(env)(pp, i.getRegisterD, dexClass, dexMethod, 0) :: paramApprox
+      if (regCount > 2) {
+        paramApprox = approxParam(env)(
+          pp,
+          i.getRegisterE,
+          dexClass,
+          dexMethod,
+          1
+        ) :: paramApprox
+        if (regCount > 3) {
+          paramApprox = approxParam(env)(
+            pp,
+            i.getRegisterF,
+            dexClass,
+            dexMethod,
+            2
+          ) :: paramApprox
+          if (regCount > 4) {
+            paramApprox = approxParam(env)(
+              pp,
+              i.getRegisterG,
+              dexClass,
+              dexMethod,
+              3
+            ) :: paramApprox
+          }
+        }
+      }
+    }
+    paramApprox.reverse
+  }
+
+  private def checkParamLeak(env: Environment)(pp: PP,
+                                               register: Int): Z3Constraint = {
+    val r = env.R(pp)
+    Z3Constraint(
+      env.ctx.mkNot(
+        env.domains.taintDomain.approx(
+          env.domains.taintDomain.top,
+          r.taints(register)
+        )
+      ),
+      s"Check R($pp)($register) LEAK",
+      pp
+    )
+  }
+
+  private def checkParametersLeak(env: Environment)(
+      i: Instruction35c,
+      pp: PP
+  ): List[Z3Constraint] = {
+    var paramsLeak: List[Z3Constraint] = List()
+    val regCount = i.getRegisterCount
+    if (regCount > 1) {
+      paramsLeak = checkParamLeak(env)(pp, i.getRegisterD) :: paramsLeak
+      if (regCount > 2) {
+        paramsLeak = checkParamLeak(env)(pp, i.getRegisterE) :: paramsLeak
+        if (regCount > 3) {
+          paramsLeak = checkParamLeak(env)(pp, i.getRegisterF) :: paramsLeak
+          if (regCount > 4) {
+            paramsLeak = checkParamLeak(env)(pp, i.getRegisterG) :: paramsLeak
+          }
+        }
+      }
+    }
+    paramsLeak.reverse
+  }
+
+  private def taintRegisterBasedOnParam(env: Environment)(
+      pp: PP,
+      register: Int,
+      paramRegister: Int): Z3Constraint = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    Z3Constraint(
+      env.domains.taintDomain.approx(
+        r.taints(paramRegister),
+        rPlus.taints(register)
+      ),
+      s"Taint R(${pp +})($register) if R($pp)($paramRegister) is tainted",
+      pp
+    )
+  }
+
+  private def taintRegisterBasedOnParameters(env: Environment)(
+      i: Instruction35c,
+      pp: PP,
+      register: Int
+  ): List[Z3Constraint] = {
+    var registerTaint: List[Z3Constraint] = List()
+    val paramsCount = i.getRegisterCount
+    if (paramsCount > 1) {
+      registerTaint = taintRegisterBasedOnParam(env)(
+        pp,
+        register,
+        i.getRegisterD) :: registerTaint
+      if (paramsCount > 2) {
+        registerTaint = taintRegisterBasedOnParam(env)(
+          pp,
+          register,
+          i.getRegisterE) :: registerTaint
+        if (paramsCount > 3) {
+          registerTaint = taintRegisterBasedOnParam(env)(
+            pp,
+            register,
+            i.getRegisterF) :: registerTaint
+          if (paramsCount > 4) {
+            registerTaint = taintRegisterBasedOnParam(env)(
+              pp,
+              register,
+              i.getRegisterG) :: registerTaint
+          }
+        }
+      }
+    }
+    registerTaint.reverse
+  }
+
+  private def taintResBasedOnParam(
+      env: Environment)(pp: PP, register: Int): Z3Constraint = {
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    Z3Constraint(
+      env.domains.taintDomain.approx(
+        r.taints(register),
+        rPlus.taints(env.R.retIdx)
+      ),
+      s"Taint R(${pp +})(ret) if R($pp)($register) is tainted",
+      pp
+    )
+  }
+
+  private def taintResultBasedOnParameters(env: Environment)(
+      i: Instruction35c,
+      pp: PP
+  ): List[Z3Constraint] = {
+    var resultTaint: List[Z3Constraint] = List()
+    val paramsCount = i.getRegisterCount
+    if (paramsCount > 1) {
+      resultTaint = taintResBasedOnParam(env)(pp, i.getRegisterD) :: resultTaint
+      if (paramsCount > 2) {
+        resultTaint = taintResBasedOnParam(env)(pp, i.getRegisterE) :: resultTaint
+        if (paramsCount > 3) {
+          resultTaint = taintResBasedOnParam(env)(pp, i.getRegisterF) :: resultTaint
+          if (paramsCount > 4) {
+            resultTaint = taintResBasedOnParam(env)(pp, i.getRegisterG) :: resultTaint
+          }
+        }
+      }
+    }
+    resultTaint.reverse
+  }
+
+  def invokeDirect(
+      i: Instruction35c,
+      pp: PP,
+      env: Environment,
+      addMethodToAnalyze: (DexClass, DexMethod) => Unit): Seq[Z3Constraint] = {
+    val mRef = i.getReference.asInstanceOf[MethodReference]
+    // RegisterD: parameter
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val constraints: Seq[Z3Constraint] =
+      env.app.classes.find(c => c.name == mRef.getDefiningClass) match {
+        case Some(dexClass) =>
+          val method =
+            dexClass.methods
+              .find(m => m.name == Utils.removeClassPrefix(mRef.toString))
+              .get
+          addMethodToAnalyze(dexClass, method)
+          val ppMethod = PP(dexClass, method, 0)
+          val thisApprox = Z3Constraint(
+            env.ctx.mkAnd(
+              r.<=(
+                i.getRegisterC,
+                method.registersCount
+              )(env.R(ppMethod)): _*
+            ),
+            s"R($pp)(${i.getRegisterC}) <= R($ppMethod)(${method.registersCount})",
+            pp
+          )
+          val paramApprox = approxParameters(env)(i, pp, dexClass, method)
+          val returnApprox: Z3Constraint =
+            Z3Constraint(
+              env.ctx.mkAnd(
+                env
+                  .M(dexClass, method)
+                  .map(mResult => {
+                    method.returnType match {
+                      case PrimitiveType() =>
+                        env.domains.primitiveDomain.approx(
+                          mResult.asInstanceOf[env.domains.primitiveDomain.Element],
+                          rPlus
+                            .numbers(env.R.retIdx)
+                        )
+                    }
+                  })
+                  .getOrElse(env.ctx.mkTrue())
+              ),
+              s"M(${dexClass.name},${method.name}) <= R(${pp +})(ret)",
+              pp
+            )
+          (thisApprox :: paramApprox) ++ Seq(returnApprox)
+        case None =>
+          taintRegisterBasedOnParameters(env)(i, pp, i.getRegisterC) ++
+            taintResultBasedOnParameters(env)(i, pp)
+      }
+    constraints ++ Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(
+          r.<=(env.R.retIdx)(rPlus): _*
+        ),
+        s"R($pp) <={ret} R(${pp +})",
+        pp
+      )
+    )
+  }
+
+  def invokeVirtual(
+      i: Instruction35c,
+      pp: PP,
+      env: Environment,
+      addMethodToAnalyze: (DexClass, DexMethod) => Unit): Seq[Z3Constraint] = {
+    val mRef = i.getReference.asInstanceOf[MethodReference]
+    val r = env.R(pp)
+    val rPlus = env.R(pp +)
+    val cName = Utils.classPrefix(mRef.toString)
+    val mName = Utils.removeClassPrefix(mRef.toString)
+    val impls: Map[DexClass, DexClass] =
+      env.Dispatch(mName, mRef.getDefiningClass)
+    val constraints: Seq[Z3Constraint] =
+      if (impls.isEmpty) {
+        val returnApprox: Z3Constraint =
+          Z3Constraint(
+            DexType(mName.substring(mName.indexOf(")") + 1)) match {
+              case PrimitiveType() =>
+                env.domains.primitiveDomain.approx(
+                  env.domains.primitiveDomain.top,
+                  rPlus
+                    .numbers(env.R.retIdx)
+                    .asInstanceOf[env.domains.primitiveDomain.Element]
+                )
+              case ObjectType(_) =>
+                env.domains.referenceDomain.approx(
+                  env.domains.referenceDomain.top,
+                  rPlus
+                    .references(env.R.retIdx)
+                    .asInstanceOf[env.domains.referenceDomain.Element]
+                )
+              case VoidType() =>
+                env.ctx.mkTrue()
+            },
+            s"T <= R(${pp +})(ret)",
+            pp
+          )
+        Seq(returnApprox) ++ taintResultBasedOnParameters(env)(i, pp)
+      } else
+        impls
+          .flatMap(impl => {
+            val dexClass = impl._2
+            env.preAnalysisResult.objectCreation
+              .filter(p => p._2 == impl._1.name)
+              .map(objPP => {
+                val method = dexClass.methods
+                  .find(m => m.name == Utils.removeClassPrefix(mRef.toString))
+                  .get
+                addMethodToAnalyze(dexClass, method)
+                val ppMethod = PP(dexClass, method, 0)
+                val thisApprox = Z3Constraint(
+                  env.ctx.mkAnd(
+                    r.<=(
+                      i.getRegisterC,
+                      method.registersCount
+                    )(env.R(ppMethod)): _*
+                  ),
+                  s"R($pp)(${i.getRegisterC}) <= R($ppMethod)(${method.registersCount})",
+                  pp
+                )
+                val paramApprox = approxParameters(env)(i, pp, dexClass, method)
+                val returnApprox: Z3Constraint =
+                  Z3Constraint(
+                    env.ctx.mkAnd(
+                      env
+                        .M(dexClass, method)
+                        .map(mResult => {
+                          method.returnType match {
+                            case PrimitiveType() =>
+                              env.domains.primitiveDomain.approx(
+                                mResult.asInstanceOf[env.domains.primitiveDomain.Element],
+                                rPlus
+                                  .numbers(env.R.retIdx)
+                              )
+                          }
+                        })
+                        .getOrElse(env.ctx.mkTrue())
+                    ),
+                    s"M(${dexClass.name},${method.name}) <= R(${pp +})(ret)",
+                    pp
+                  )
+                Z3Constraint(
+                  env.ctx.mkImplies(
+                    env.ctx.mkAnd(
+                      env.domains.referenceDomain.approx(
+                        env.domains.referenceDomain.toElement(
+                          objPP._1.toString),
+                        r.references(i.getRegisterC)
+                      )
+                    ),
+                    env.ctx.mkAnd(
+                      env.ctx.mkAnd(
+                        paramApprox.map(c => c.boolExpr): _*
+                      ),
+                      env.ctx.mkAnd(
+                        thisApprox.boolExpr
+                      ),
+                      returnApprox.boolExpr
+                    )
+                  ),
+                  s"${objPP._1.toString} <= R($pp)(${i.getRegisterC}) => " +
+                    (if (paramApprox.isEmpty) ""
+                     else
+                       paramApprox
+                         .map(c => c.description)
+                         .mkString(" ∧ ") + " ∧ ") + thisApprox.description +
+                    " ∧ " + returnApprox.description,
+                  pp
+                )
+              })
+          })
+          .toList
+    var taintConstraints = List[Z3Constraint]()
+    if (env.app.sourcesSinks.isSource(cName, mName)) {
+      taintConstraints = Z3Constraint(
+        env.domains.taintDomain.approx(
+          env.domains.taintDomain.top,
+          rPlus.taints(env.R.retIdx)
+        ),
+        s"Taint R(${pp +})(ret)",
+        pp
+      ) :: taintConstraints
+    }
+    if (env.app.sourcesSinks.isSink(cName, mName)) {
+      taintConstraints = taintConstraints ++ (
+        Z3Constraint(
+          env.ctx.mkNot(
+            env.domains.taintDomain.approx(
+              env.domains.taintDomain.top,
+              r.taints(i.getRegisterC)
+            )
+          ),
+          s"Check R($pp)(${i.getRegisterC}) LEAK",
+          pp
+        ) :: checkParametersLeak(env)(i, pp)
+      )
+    }
+    constraints ++ taintConstraints ++ Seq(
+      Z3Constraint(
+        env.ctx.mkAnd(
+          r.<=(env.R.retIdx)(rPlus): _*
+        ),
+        s"R($pp) <={ret} R(${pp +})",
+        pp
+      )
+    )
+
+  }
+
+  private def classAndSubclasses(env: Environment)(
+      definingClass: String): List[DexClass] = {
+    env.app.classes.find(c => c.name == definingClass) match {
+      case Some(dexClass) => dexClass :: subclasses(env)(dexClass)
+      case None           => List()
+    }
+  }
+
+  private def subclasses(env: Environment)(
+      dexClass: DexClass): List[DexClass] = {
+    env.app.classes
+      .filter(c => c.superClass == dexClass.name)
+      .flatMap(c => subclasses(env)(c))
+      .toList
+  }
+
+}

src/main/scala/analysis/PP.scala

@@ -0,0 +1,20 @@
+package analysis
+
+import dex.{DexClass, DexMethod}
+
+/**
+  * Program point.
+  */
+case class PP(c: DexClass, m: DexMethod, pc: Int) {
+
+  /**
+    * Returns a new program point with the program counter increased by 1.
+    */
+  def + : PP = {
+    this.copy(pc = this.pc + 1)
+  }
+
+  override def toString: String =
+    s"${c.name},${m.name},$pc"
+
+}

src/main/scala/analysis/PreAnalysisResult.scala

@@ -0,0 +1,8 @@
+package analysis
+
+/**
+  * Result of the pre analysis.
+  * @param objectCreation map where the key is the program point where the object is created,
+  *                       and the key is the class name.
+  */
+case class PreAnalysisResult(objectCreation: Map[PP, String]) {}

src/main/scala/analysis/PreAnalyzer.scala

@@ -0,0 +1,39 @@
+package analysis
+
+import dex.DexClass
+import org.jf.dexlib2.Opcode
+import org.jf.dexlib2.dexbacked.reference.DexBackedTypeReference
+import org.jf.dexlib2.iface.instruction.{Instruction, ReferenceInstruction}
+
+class PreAnalyzer(classes: Seq[DexClass]) {
+
+  /**
+    * Pre analysis.
+    */
+  def analyze: PreAnalysisResult = {
+    /*
+      Find all the NEW_INSTANCE instructions and create a map
+      where the key is the program point and the key the class name.
+     */
+    val objectCreation: Map[PP, String] = classes
+      .flatMap(c => {
+        c.methods.flatMap(m => {
+          m.instructions
+            .filter(i => i.getOpcode == Opcode.NEW_INSTANCE)
+            .zipWithIndex
+            .map {
+              case (i: Instruction, pc: Int) =>
+                val objType = i
+                  .asInstanceOf[ReferenceInstruction]
+                  .getReference
+                  .asInstanceOf[DexBackedTypeReference]
+                  .getType
+                (PP(c, m, pc), objType)
+            }
+        })
+      })
+      .toMap
+    PreAnalysisResult(objectCreation)
+  }
+
+}

src/main/scala/analysis/Z3Object.scala

@@ -0,0 +1,39 @@
+package analysis
+
+import com.microsoft.z3._
+import domain.AbstractDomainsCollection
+
+/**
+  * Abstract object Z3 representation.
+  */
+class Z3Object(ctx: Context, domains: AbstractDomainsCollection) {
+
+  private val constructor: Constructor =
+    ctx.mkConstructor(
+      "mk-object",
+      "is-object",
+      Array("name", "prim", "ref", "taint"),
+      Array[Sort](
+        ctx.mkStringSort(),
+        ctx.mkArraySort(ctx.mkStringSort(), domains.primitiveDomain.sort),
+        ctx.mkArraySort(ctx.mkStringSort(), domains.referenceDomain.sort),
+        ctx.mkArraySort(ctx.mkStringSort(), domains.taintDomain.sort)
+      ),
+      Array(0, 0, 0, 0)
+    )
+
+  val sort: DatatypeSort =
+    ctx.mkDatatypeSort(
+      "Object",
+      Array(
+        constructor
+      )
+    )
+
+  private val accessors = constructor.getAccessorDecls
+
+  val nameAccessor: FuncDecl = accessors(0)
+  val primAccessor: FuncDecl = accessors(1)
+  val refAccessor: FuncDecl = accessors(2)
+  val taintAccessor: FuncDecl = accessors(3)
+}

src/main/scala/constraints/Z3Constraint.scala

@@ -0,0 +1,12 @@
+package constraints
+
+import analysis.PP
+import com.microsoft.z3.BoolExpr
+
+/**
+  * Constraint to give to Z3.
+  * @param boolExpr the Z3 boolean expression.
+  * @param description text description of the rule.
+  * @param pp the program point where the rule has been generated.
+  */
+case class Z3Constraint(boolExpr: BoolExpr, description: String, pp: PP) {}

src/main/scala/dex/DexApp.scala

@@ -0,0 +1,11 @@
+package dex
+
+import taint.SourcesSinks
+
+class DexApp(
+    val manifest: Manifest,
+    val classes: Seq[DexClass],
+    val entryPoints: Seq[(DexClass, DexMethod)],
+    val sourcesSinks: SourcesSinks
+) {
+}

src/main/scala/dex/DexClass.scala

@@ -0,0 +1,25 @@
+package dex
+
+import org.jf.dexlib2.iface.instruction.Instruction
+
+case class DexClass(
+    name: String,
+    superClass: String,
+    interfaces: Seq[String],
+    fields: Seq[DexField],
+    methods: Seq[DexMethod]
+) {}
+
+case class DexField(shortName: String, name: String, dexType: DexType) {}
+
+case class DexMethod(
+    shortName: String,
+    name: String,
+    paramTypes: Seq[DexType],
+    returnType: DexType,
+    registersCount: Int,
+    paramsCount: Int,
+    instructions: Seq[Instruction]
+) {
+  val localRegistersCount: Int = registersCount - paramsCount
+}

src/main/scala/dex/DexType.scala

@@ -0,0 +1,33 @@
+package dex
+
+sealed trait DexType {}
+
+object DexType {
+
+  case class VoidType private[DexType] () extends DexType {}
+
+  case class PrimitiveType private[DexType] () extends DexType {}
+
+  case class ObjectType private[DexType] (className: String) extends DexType {}
+
+  case class ArrayType private[DexType] (dexType: DexType) extends DexType {}
+
+  def apply(param: String): DexType = {
+    param match {
+      case "V" => VoidType()
+      case "Z" // Boolean
+          | "B" // Byte
+          | "S" // Short
+          | "C" // Char
+          | "I" // Integer
+          | "J" // Long
+          | "F" // Float
+          | "D" // Double
+          =>
+        PrimitiveType()
+      case className if className.startsWith("L") => ObjectType(className)
+      case arrayType if arrayType.startsWith("[") =>
+        ArrayType(apply(arrayType.substring(1)))
+    }
+  }
+}

src/main/scala/dex/Manifest.scala

@@ -0,0 +1,6 @@
+package dex
+
+class Manifest(
+    val entryPoints: Seq[(DexClass, DexMethod)],
+    val activities: Seq[DexClass]
+) {}

src/main/scala/domain/AbstractDomain.scala

@@ -0,0 +1,24 @@
+package domain
+
+import com.microsoft.z3.{BoolExpr, Expr, Sort}
+
+/**
+  * Lattice.
+  */
+trait AbstractDomain {
+
+  type Element <: Expr
+
+  def sort: Sort
+
+  def top: Element
+
+  def bottom: Element
+
+  def meet(e1: Element, e2: Element): Element
+
+  def join(e1: Element, e2: Element): Element
+
+  def approx(e1: Element, e2: Element): BoolExpr
+
+}

src/main/scala/domain/AbstractDomainsCollection.scala

@@ -0,0 +1,7 @@
+package domain
+
+case class AbstractDomainsCollection(
+    primitiveDomain: PrimitiveDomain,
+    referenceDomain: ReferenceDomain,
+    taintDomain: TaintDomain
+) {}

src/main/scala/domain/BitVectorSetDomain.scala

@@ -0,0 +1,59 @@
+package domain
+
+import com.microsoft.z3._
+
+class BitVectorSetDomain(ctx: Context) extends PrimitiveDomain {
+
+  override type Element = ArrayExpr
+
+  private val size: Int = 32
+  private val bv: BitVecSort = ctx.mkBitVecSort(size)
+  private val bvSet: SetSort = ctx.mkSetSort(ctx.mkBitVecSort(size))
+
+  override def sort: Sort = bvSet
+
+  override def top: Element = ctx.mkFullSet(bv)
+
+  override def bottom: Element = ctx.mkEmptySet(bv)
+
+  override def meet(e1: Element, e2: Element): Element =
+    ctx.mkSetIntersection(e1, e2)
+
+  override def join(e1: Element, e2: Element): Element =
+    ctx.mkSetUnion(e1, e2)
+
+  override def approx(e1: Element, e2: Element): BoolExpr =
+    ctx.mkSetSubset(
+      e1,
+      e2
+    )
+
+  override def toElement(n: Long): Element =
+    ctx.mkSetAdd(
+      ctx.mkEmptySet(bv),
+      ctx.mkBV(n, size)
+    )
+
+  override def toElement(n: Double): ArrayExpr =
+    ctx.mkSetAdd(
+      ctx.mkEmptySet(bv),
+      ctx.mkFPToIEEEBV(
+        ctx.mkFP(n, ctx.mkFPSort32())
+      )
+    )
+
+  override def sum(e1: ArrayExpr, e2: ArrayExpr): ArrayExpr =
+    top
+
+  override def neg(e: ArrayExpr): ArrayExpr =
+    top
+
+  override def div(e1: ArrayExpr, e2: ArrayExpr): ArrayExpr =
+    top
+
+  override def mult(e1: ArrayExpr, e2: ArrayExpr): ArrayExpr =
+    top
+
+  override def rem(e1: ArrayExpr, e2: ArrayExpr): ArrayExpr =
+    top
+}

src/main/scala/domain/PrimitiveDomain.scala

@@ -0,0 +1,21 @@
+package domain
+
+/**
+  * Abstract domain for primitive values.
+  */
+trait PrimitiveDomain extends AbstractDomain {
+
+  def toElement(n: Long): Element
+
+  def toElement(n: Double): Element
+
+  def neg(e: Element): Element
+
+  def sum(e1: Element, e2: Element): Element
+
+  def div(e1: Element, e2: Element): Element
+
+  def mult(e1: Element, e2: Element): Element
+
+  def rem(e1: Element, e2: Element): Element
+}

src/main/scala/domain/ReferenceDomain.scala

@@ -0,0 +1,39 @@
+package domain
+
+import com.microsoft.z3._
+
+/**
+  * Abstract domain for references.
+  */
+class ReferenceDomain(ctx: Context) extends AbstractDomain {
+
+  override type Element = ArrayExpr
+
+  private val stringSort: SeqSort = ctx.mkStringSort()
+  private val stringSet: SetSort = ctx.mkSetSort(stringSort)
+
+  override def sort: Sort = stringSet
+
+  override def top: Element = ctx.mkFullSet(stringSort)
+
+  override def bottom: Element = ctx.mkEmptySet(stringSort)
+
+  override def meet(e1: Element, e2: Element): Element =
+    ctx.mkSetIntersection(e1, e2)
+
+  override def join(e1: Element, e2: Element): Element =
+    ctx.mkSetUnion(e1, e2)
+
+  override def approx(e1: Element, e2: Element): BoolExpr =
+    ctx.mkSetSubset(
+      e1,
+      e2
+    )
+
+  def toElement(pp: String): Element =
+    ctx.mkSetAdd(
+      ctx.mkEmptySet(stringSort),
+      ctx.mkString(pp)
+    )
+
+}

src/main/scala/domain/TaintDomain.scala

@@ -0,0 +1,34 @@
+package domain
+
+import com.microsoft.z3._
+
+/**
+  * Domain to track taint information.
+  */
+class TaintDomain(ctx: Context) extends AbstractDomain {
+
+  override type Element = BoolExpr
+
+  override def sort: Sort = ctx.mkBoolSort()
+
+  override def top: Element = ctx.mkTrue()
+
+  override def bottom: Element = ctx.mkFalse()
+
+  override def meet(e1: Element, e2: Element): Element =
+    ctx.mkNot(
+      ctx.mkXor(e1, e2)
+    )
+
+  override def join(e1: Element, e2: Element): Element =
+    ctx.mkNot(
+      ctx.mkXor(e1, e2)
+    )
+
+  override def approx(e1: Element, e2: Element): BoolExpr =
+    ctx.mkOr(
+      ctx.mkNot(e1),
+      e2
+    )
+
+}

src/main/scala/domain/TopDomain.scala

@@ -0,0 +1,47 @@
+package domain
+
+import com.microsoft.z3._
+
+/**
+  * Domain that maps everything to top.
+  */
+class TopDomain(ctx: Context) extends PrimitiveDomain {
+
+  override type Element = BoolExpr
+
+  override def sort: Sort = ctx.mkBoolSort()
+
+  override def top: Element = ctx.mkTrue()
+
+  override def bottom: Element = ctx.mkTrue()
+
+  override def meet(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+
+  override def join(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+
+  override def approx(e1: Element, e2: Element): BoolExpr =
+    ctx.mkTrue()
+
+  override def toElement(n: Long): Element =
+    ctx.mkTrue()
+
+  override def toElement(n: Double): Element =
+    ctx.mkTrue
+
+  override def sum(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+
+  override def neg(e: Element): Element =
+    ctx.mkTrue()
+
+  override def div(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+
+  override def mult(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+
+  override def rem(e1: Element, e2: Element): Element =
+    ctx.mkTrue()
+}

src/main/scala/parser/AndroidXmlParser.scala

@@ -0,0 +1,19 @@
+package parser
+
+import dex.{DexClass, Manifest}
+
+/**
+  * Class to parse the manifest and the resources xmls.
+  */
+// TODO: parse xml files.
+class AndroidXmlParser(apkLocation: String, classes: Seq[DexClass]) {
+
+  def parseManifest(): Manifest = {
+    val mainActivity =
+    classes.filter(c => c.name.contains("MyActivity;")).head
+    new Manifest(
+      Seq(),
+      Seq(mainActivity)
+    )
+  }
+}

src/main/scala/parser/EntryPointsProvider.scala

@@ -0,0 +1,18 @@
+package parser
+
+import dex.{DexClass, DexMethod}
+
+// TODO: read from EntryPoints.txt file
+class EntryPointsProvider(classes: Seq[DexClass]) {
+
+  def entryPoints(): Seq[(DexClass, DexMethod)] = {
+    classes.flatMap(
+      c =>
+        c.methods
+          .filter(m =>
+            m.name == "onCreate(Landroid/os/Bundle;)V"
+              || m.name == "onStart()V")
+          .map(m => (c, m))
+    )
+  }
+}

src/main/scala/parser/Parser.scala

@@ -0,0 +1,79 @@
+package parser
+
+import java.io.File
+
+import dex._
+import org.jf.dexlib2.dexbacked.{
+  DexBackedClassDef,
+  DexBackedDexFile,
+  DexBackedField,
+  DexBackedMethod
+}
+import org.jf.dexlib2.{DexFileFactory, Opcodes}
+import utils.Utils
+
+import scala.collection.JavaConverters._
+
+class Parser(apkLocation: String) {
+
+  val apkFile = new File(apkLocation)
+  val dexFile: DexBackedDexFile =
+    DexFileFactory.loadDexFile(apkFile, Opcodes.forApi(21))
+
+  def dexApp: DexApp = {
+    val classes = parseClasses
+    new DexApp(
+      new AndroidXmlParser(apkLocation, classes).parseManifest(),
+      classes,
+      new EntryPointsProvider(classes).entryPoints(),
+      new SourcesSinksProvider().sourcesSinks()
+    )
+  }
+
+  private def parseClasses: Seq[DexClass] = {
+    dexFile.getClasses.asScala.toSeq
+      .filter(classFilter())
+      .map(
+        c =>
+          DexClass(
+            c.getType,
+            c.getSuperclass,
+            c.getInterfaces.asScala,
+            classFields(c.getFields.asScala.toSeq),
+            classMethods(c.getMethods.asScala.toSeq)
+        ))
+  }
+
+  private def classFilter(): DexBackedClassDef => Boolean =
+    (t: DexBackedClassDef) => !t.getType.startsWith("Landroid/support")
+
+  private def methodFilter(): DexBackedMethod => Boolean =
+    (m: DexBackedMethod) => m.getImplementation != null
+
+  private def classFields(fields: Seq[DexBackedField]): Seq[DexField] =
+    fields
+      .map(
+        f =>
+          DexField(
+            f.getName,
+            Utils.removeClassPrefix(f.toString),
+            DexType(f.getType)
+        ))
+
+  private def classMethods(methods: Seq[DexBackedMethod]): Seq[DexMethod] = {
+    methods
+      .filter(methodFilter())
+      .map(
+        m =>
+          DexMethod(
+            m.getName,
+            Utils.removeClassPrefix(m.toString),
+            m.getParameterTypes.asScala.map(t => DexType(t)),
+            DexType(m.getReturnType),
+            m.getImplementation.getRegisterCount,
+            m.getParameters.size(),
+            m.getImplementation.getInstructions.asScala.toSeq
+        ))
+  }
+
+}

src/main/scala/parser/SourcesSinksProvider.scala

@@ -0,0 +1,27 @@
+package parser
+
+import taint.{Sink, Source, SourcesSinks}
+
+// TODO: read from SourcesAndSinks.txt file
+class SourcesSinksProvider() {
+
+  def sourcesSinks(): SourcesSinks =
+    new SourcesSinks(
+      Seq(
+        Source(
+          "Landroid/telephony/TelephonyManager;",
+          "getDeviceId()Ljava/lang/String;"
+        )
+      ),
+      Seq(
+        Sink(
+          "Ljava/net/URL;",
+          "openConnection()Ljava/net/URLConnection;"
+        ),
+        Sink(
+          "Landroid/telephony/SmsManager;",
+          "sendTextMessage(Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Landroid/app/PendingIntent;Landroid/app/PendingIntent;)V"
+        )
+      )
+    )
+}

src/main/scala/taint/SourcesSinks.scala

@@ -0,0 +1,16 @@
+package taint
+
+class SourcesSinks(val sources: Seq[Source], val sinks: Seq[Sink]) {
+
+  def isSource(className: String, methodName: String): Boolean = {
+    sources.exists(s => s.className == className && s.methodName == methodName)
+  }
+
+  def isSink(className: String, methodName: String): Boolean = {
+    sinks.exists(s => s.className == className && s.methodName == methodName)
+  }
+}
+
+case class Source(className: String, methodName: String) {}
+
+case class Sink(className: String, methodName: String) {}

src/main/scala/utils/Utils.scala

@@ -0,0 +1,12 @@
+package utils
+
+object Utils {
+
+  def classPrefix(str: String): String = {
+    str.substring(0, str.indexOf("->"))
+  }
+
+  def removeClassPrefix(str: String): String = {
+    str.substring(str.indexOf("->") + 2)
+  }
+}