Haniel Barbosa

47 papers A 5B 7C 1Journal 10Unranked 19
YearRankTypeTitle / Venue / Authors
2026 B conf
CPP
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2026 conf
TACAS (1)
Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026 J jnl
CoRR
Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026 B conf
VMCAI
Bruno Andreotti, Haniel Barbosa
2026 J jnl
Acta Informatica
Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
2025 B conf
ITP
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025 J jnl
CoRR
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2025 ed.
LSFA
Haniel Barbosa, Christophe Ringeissen
2025 conf
CAV (3)
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2024 ed.
SBMF
Haniel Barbosa, Yoni Zohar
2024 conf
TACAS (1)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024 conf
FM (2)
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024 conf
PAAR+SC²@IJCAR
Bruno Andreotti, Haniel Barbosa, Oliver Flatt
2023 B conf
LPAR
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023 conf
SMT
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023 conf
TACAS (1)
Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa
2023 conf
SC-Square@ISSAC
Haniel Barbosa
2023 J jnl
Commun. ACM
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
2023 ed.
SC-Square@FLoC
Ali Kemal Uncu, Haniel Barbosa
2023 J jnl
J. Autom. Reason.
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2022 conf
CAV (2)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2022 A conf
IJCAR
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2022 B conf
FMCAD
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 conf
TACAS (1)
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
2021 conf
PxTP
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
2021 B conf
FMCAD
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021 J jnl
CoRR
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021 J jnl
J. Comput. Lang.
João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira, Srinivas Vladamani
2020 conf
SMT
Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
2020 conf
IJCAR (1)
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
2020 J jnl
J. Autom. Reason.
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
2019 J jnl
CoRR
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019 A conf
CADE
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
2019 B conf
FMCAD
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
2019 ed.
PxTP
Giselle Reis, Haniel Barbosa
2019 A conf
SAT
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019 conf
CAV (2)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2018 J jnl
CoRR
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018 A conf
IJCAR
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
2018 conf
TACAS (2)
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
2017 conf
TACAS (2)
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2017 conf
PxTP
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
2017
Haniel Barbosa
2017 A conf
CADE
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
2016 conf
PAAR@IJCAR
Haniel Barbosa
2012 conf
SBMF
Haniel Barbosa, David Déharbe
2012 C conf
ABZ
Haniel Barbosa, David Déharbe
redb/extractors/decompiler/apk/smali_parser.py
← Index redb/extractors/decompiler/apk/smali_parser.py python
"""Smali file parser — extracts individual method bodies from apktool output.

Parses .smali files produced by apktool and extracts per-method bodies,
instruction counts, and register counts.
"""

import os
import re
from dataclasses import dataclass, field
from typing import Dict, List, Optional


@dataclass
class SmaliMethod:
    """Parsed smali method data."""
    class_name: str
    method_name: str
    method_signature: str
    body: str
    instruction_count: int = 0
    register_count: int = 0
    access_flags: List[str] = field(default_factory=list)


# Directives start with '.' — these are metadata, not instructions
_DIRECTIVE_RE = re.compile(r"^\s*\.")
# Labels start with ':'
_LABEL_RE = re.compile(r"^\s*:")
# Blank or comment lines
_BLANK_OR_COMMENT_RE = re.compile(r"^\s*(#.*)?$")
# Method declaration
_METHOD_START_RE = re.compile(
    r"^\.method\s+(.*?)\s+(\S+)\(([^)]*)\)(\S+)\s*$"
)
_METHOD_START_SIMPLE_RE = re.compile(
    r"^\.method\s+(.*)"
)
# .registers or .locals directive
_REGISTERS_RE = re.compile(r"^\s*\.registers\s+(\d+)")
_LOCALS_RE = re.compile(r"^\s*\.locals\s+(\d+)")
# .line directive
_LINE_RE = re.compile(r"^\s*\.line\s+\d+")


class SmaliParser:
    """Parser for apktool smali output files."""

    @staticmethod
    def parse_smali_file(filepath: str) -> List[SmaliMethod]:
        """Parse a single .smali file and return list of methods.

        Each .smali file contains one class with all its methods.
        """
        with open(filepath, "r", encoding="utf-8", errors="replace") as f:
            content = f.read()

        return SmaliParser._parse_smali_content(content, filepath)

    @staticmethod
    def _parse_smali_content(content: str, source: str = "") -> List[SmaliMethod]:
        """Parse smali text content and extract methods."""
        lines = content.split("\n")
        methods = []

        # Extract class name from .class directive
        class_name = ""
        for line in lines:
            if line.startswith(".class "):
                parts = line.split()
                class_name = parts[-1]  # Last token is the class descriptor
                break

        in_method = False
        method_lines = []
        method_header = ""
        access_flags = []
        skip_method = False

        for line in lines:
            if line.startswith(".method "):
                in_method = True
                method_lines = []
                method_header = line
                skip_method = False

                # Parse access flags and method signature
                remainder = line[len(".method "):].strip()
                tokens = remainder.split()
                access_flags = []
                method_sig_token = tokens[-1] if tokens else ""

                for t in tokens[:-1]:
                    access_flags.append(t)

                # Skip abstract and native methods (no body)
                if "abstract" in access_flags or "native" in access_flags:
                    skip_method = True

            elif line.startswith(".end method"):
                if in_method and not skip_method:
                    body = "\n".join(method_lines)
                    method_name, signature = SmaliParser._parse_method_sig(
                        method_header
                    )
                    instruction_count = SmaliParser.count_instructions(body)
                    register_count = SmaliParser._extract_register_count(body)

                    methods.append(
                        SmaliMethod(
                            class_name=class_name,
                            method_name=method_name,
                            method_signature=signature,
                            body=body,
                            instruction_count=instruction_count,
                            register_count=register_count,
                            access_flags=access_flags,
                        )
                    )
                in_method = False
                method_lines = []
                access_flags = []

            elif in_method and not skip_method:
                method_lines.append(line)

        return methods

    @staticmethod
    def parse_smali_directory(dirpath: str) -> Dict[str, SmaliMethod]:
        """Parse all .smali files in a directory tree.

        Returns dict keyed by 'ClassName->methodName(signature)ReturnType'.
        """
        result = {}
        for root, _dirs, files in os.walk(dirpath):
            for fname in files:
                if fname.endswith(".smali"):
                    fpath = os.path.join(root, fname)
                    try:
                        methods = SmaliParser.parse_smali_file(fpath)
                        for m in methods:
                            key = SmaliParser.make_method_key(
                                m.class_name, m.method_name, m.method_signature
                            )
                            result[key] = m
                    except Exception:
                        continue
        return result

    @staticmethod
    def normalize_smali_body(body: str) -> str:
        """Normalize smali body for consistent hashing.

        Strips comments, .line directives, normalizes whitespace.
        """
        lines = []
        for line in body.split("\n"):
            stripped = line.strip()
            # Skip empty lines, comments, and .line directives
            if not stripped or stripped.startswith("#"):
                continue
            if _LINE_RE.match(stripped):
                continue
            lines.append(stripped)
        return "\n".join(lines)

    @staticmethod
    def count_instructions(body: str) -> int:
        """Count actual Dalvik instructions (skip directives, labels, blanks)."""
        count = 0
        for line in body.split("\n"):
            stripped = line.strip()
            if not stripped:
                continue
            if _DIRECTIVE_RE.match(stripped):
                continue
            if _LABEL_RE.match(stripped):
                continue
            if _BLANK_OR_COMMENT_RE.match(stripped):
                continue
            count += 1
        return count

    @staticmethod
    def _extract_register_count(body: str) -> int:
        """Extract register count from .registers or .locals directive.

        apktool outputs .locals (local registers only) by default.
        .registers (total = locals + params) is used with --use-registers.
        We return whichever is present.
        """
        for line in body.split("\n"):
            stripped = line.strip()
            m = _REGISTERS_RE.match(stripped)
            if m:
                return int(m.group(1))
            m = _LOCALS_RE.match(stripped)
            if m:
                return int(m.group(1))
        return 0

    @staticmethod
    def _parse_method_sig(header_line: str) -> tuple:
        """Parse method name and signature from .method header line.

        Input: '.method public onCreate(Landroid/os/Bundle;)V'
        Returns: ('onCreate', '(Landroid/os/Bundle;)V')
        """
        remainder = header_line[len(".method "):].strip()
        tokens = remainder.split()
        if not tokens:
            return ("unknown", "()")

        # Last token contains methodName(params)returnType
        method_part = tokens[-1]

        paren_idx = method_part.find("(")
        if paren_idx == -1:
            return (method_part, "()")

        method_name = method_part[:paren_idx]
        signature = method_part[paren_idx:]

        return (method_name, signature)

    @staticmethod
    def make_method_key(class_name: str, method_name: str, signature: str) -> str:
        """Build a canonical method key for cross-tool matching.

        Format: 'Lcom/example/Foo;->methodName(params)ReturnType'
        """
        return f"{class_name}->{method_name}{signature}"