adds experimental Ghidra disassembler and lifting backend (#1326)

* initial scaffolding

* adds support for nameless registers in the disasm backend

We don't want to model unique (temporary) registers as normal physical
registers, so we add an option to set the name to -1 to indicate that
the register is a unique anonymous variable.

* the minimal implementation

* introduces sub-instructions to the disassembler

There was some provision for that in the backend but never fully
implemented. This feature enables seambless integeration of the ghidra
backend but may also used for VLIW architecture, e.g., hexagon llvm
backend is using it.

* fixes the handling of the unique namespace

* implements semantics of sequential instructions

* specifies semantics for most of the pcode instructions

* passes the basic instruction info to the sequential semantics value

* fixes the semantics of LOAD

* improves handling of pcode namespaces

Fixes varnode classification (no longer treating addresses as
registers).

Also to prevent name clashes between virtual variables from different
scopes we use unique prefixes (aka shortcuts in ghidra's parlance) to
distinguish between them. This also makes the generated code more
readable and closer to the originally genereated pcode.

* fixes the subpiece implementation

* puts all pcode opcodes into the pcode namespace

Since they are the same for each architecture and now we have this feature.

* implements support for user-defined opcodes

we translate

`CALLOTHER(<name>,<arg1>,...,<argN>)`

to

`<name>(<arg1>,...,<argN>)`

* translates local (intra-instruction) branches into GOTOs

Branches in p-code are overloaded by the type of destination. If the
destination is a virtual address then it is a normal branch and if
it is a constant (a varnode from the constant namespace) then it is
an intra-instruction branch that represents the inner instruction
logic.

* fixes the satisfies function to account for subinstructions

before that it was only looking into the top-level instruction

* an attempt to pack subinstructions inside an instruction

(breaks lots of stuff)

* publishes subinstructions

I will probably forfeit this approach, still investigating.

* introduces the null object to the knowledge base

It was actually already there, hidden in the [obj] domain. Now it is
properly documented with well defined semantics.

* uses the null object to represent unlabeled blocks in the lifters

Also, more lifters now respect the passed label to the blk operator.

* removes the subinstruction slot from instruction

* adds labels reification to BIL semantics, also reifies gotos

all using special encoding

* implements intra-instruction gotos

* adds the sequence number documentation.

* fixes error hanlding in the goto-subinstruction primitive

* implements a proper disassembler factory that scans for ldefs files

So far not working quite correctly, as the default variables (like
word size, etc) are not properly set. Investigating...

* adds a proper processor initialization

* implements proper command-line interface

Now the plugin is able to list the targets and pass the path to ghidra root.

* adds a tentative --x86-backend option to enable ghidra for x86

* fixes offset and address calculation

* adds `is-symbol` semantic primitive

* fixes overloading of the Primus Lisp semantic definitions

The overloading was prevented by the attributes computation, which
expected no overloads. Also, makes error message more readable.

* tries to overload p-code operations based on their operand types

* passes operands types per each operand, removes extra opcodes

It looks like that not only branches are overloaded in p-code but all
operations, e.g., we can have `INT_ADD (mem:x) (mem:y) (mem:z)` that
represents `mem[x] <- mem[y] + mem[z]`.

We could also resolve this overloading by adding suffixes to
operations, e.g., `INT_ADDmr`, `INT_ADDmm`, and so on, but will
explode the number of opcodes, especially in the presence of
user-defined opcodes.

* catches the bad or unimplemented instructions during decoding

ghidra raises an exception if an instruction is not valid or there is
no semantics for it.

* adds signed ordering Primus Lisp primitives

and implemented corresponding pcode operations

* passes full information about the operand type from the backend

In p-code the semantics of an operation is defined by the types of its
operands. In case of the unique variables the type is not known to us
so we have to pass it. This commit extends the previous approach,
where we were passing only the kind of the operand (mem vs imm) to the
full type qualification, where the type of memory is represented with
Nil and the type of immediates is represented by its size in the
number of bits.

* adds the missing BOOL_NEGATE operation

* fixes the negation operator (pcode represent bool as byte)

* removes aliased registers from the register table

* fixes the selection of the default backend for x86

it should be llvm if not specified otherwise

* switches to caseless ordering of variables

Changes and documents the ordering of variables. Variables are no
compared caseless and the ordering is made loosely compatible with the
caseless lexicographical ordering of the textual representation of
variables' identifiers, e.g.,
```
```

* enables ghidra backend for the arm targets

Right now it is disabled by default, use `--arm-backend=ghidra` to
enable.

* uses pcode-x86 as the CT language for pcode in x86 targets

* adds ghidra backend to mips

* minor pretty-printing tweaks

to make things more readable

* improves primitives performance in Primus Lisp

With this optimization Primus Lisp-based lifters run five times
faster. This especially important for ghidra backend lifters, which
are fully dependent on Primus Lisp.

The idea is to let the primitive implementors provide the body of
their primitive so that every primitive is not computed via the
semantics promise but is invoked directly. Another big idea is to
provide such an interface that will allow to factor out computations
that are common to the target. The same idea could be extrapolated to
all promises.

* optimization: improves name resolution in Primus Lisp

Uses maps for names, not lists. Surprisingly not much of improvement,
something about 5%.

* optimizes unit computatation

by hoisting it out of the loop

* optimization: do not request lisp arguments if not necessary

To compute list arguments we need to invoke the theory and reflect
them into it. The resulting work is discarded if the name is not
bound. The optimization checks if the name is bound by the program and
only after that asks for the list of arguments.

* adds ghidra to powerpc (works out of the box)

* adds the `--x86-64-backend` option

it is just an alias for `--x86-backend`, for consistency

* enables ghidra for riscv (doesn't run out of the box)

* enables the ghidra backend in CI/CD

We will build Ghidra only on supported targets, right now it is Ubuntu
Bionic. We will soon add more targets and more packages. The bap
packages will be now split into `bap-core`, `bap`, and `bap-extra`.

The `bap-core` will contain the minimal part of platform without
analyses. The `bap` package will include most of the analyses, finally,
`bap-extra` will include heavy-weight analysis (in terms of extra
dependencies and build times), e.g., the symbolic executor, and the
ghidra backend.

* moves the ghidra install section lower

* downgrades the ubuntu version on CI/CD

* tries to fix the macOS build

* disables ghidra in the opam/opam used in CI

Author: ivg

.github/workflows/build-and-test.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
 
     env:
       OPAMJOBS: 2
@@ -32,7 +32,13 @@ jobs:
         run: opam pin add bap . --no-action
 
       - name: Install system dependencies
-        run: opam depext -u bap
+        run: opam depext -u bap-extra
+
+      - name: Install Ghidra
+        run: |
+          sudo add-apt-repository ppa:ivg/ghidra -y
+          sudo apt-get install libghidra-dev -y
+          sudo apt-get install libghidra-data -y
 
       - name: Install opam dependencies
         run: |

.github/workflows/build-dev-repo.yml

@@ -43,7 +43,6 @@ jobs:
         if: matrix.os == 'macos-latest'
         run: |
           rm -rf /usr/local/bin/2to3
-          brew unlink gcc@8
           brew unlink gcc@9
           brew update
           brew upgrade

.github/workflows/build-from-opam.yml

@@ -10,7 +10,7 @@ jobs:
           - 4.11.x
           - 4.08.x
 
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-18.04
 
     env:
       OPAMJOBS: 2
@@ -23,11 +23,17 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
           dune-cache: true
 
+      - name: Install Ghidra
+        run: |
+          sudo add-apt-repository ppa:ivg/ghidra -y
+          sudo apt-get install libghidra-dev -y
+          sudo apt-get install libghidra-data -y
+
       - name: Add the testing Repository
         run: opam repo add bap git://github.com/BinaryAnalysisPlatform/opam-repository#testing
 
       - name: Install system dependencies
-        run: opam depext -u bap
+        run: opam depext -u bap-extra
 
       - name: Cleanup the Caches
         run: sudo apt clean --yes
@@ -36,7 +42,7 @@ jobs:
         run: df -h
 
       - name: Build and Install BAP Packages
-        run: opam clean -a; opam install bap
+        run: opam clean -a; opam install bap-extra
 
       - uses: actions/upload-artifact@v2
         if: ${{ always() }}

.github/workflows/nightly-testing.yml

@@ -10,7 +10,7 @@ jobs:
     strategy:
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-18.04
         ocaml-compiler:
           - 4.11.x
           - 4.08.x
@@ -29,30 +29,25 @@ jobs:
           dune-cache: true
           cache-prefix: nightly
 
-      - name: Configure Homebrew
-        if: matrix.os == 'macos-latest'
+      - name: Install Ghidra
         run: |
-          rm -rf /usr/local/bin/2to3
-          brew unlink gcc@8
-          brew unlink gcc@9
-          brew update
-          brew upgrade
-          echo 'LLVM_CONFIG=/usr/local/opt/llvm@9/bin/llvm-config' >> $GITHUB_ENV
+          sudo add-apt-repository ppa:ivg/ghidra -y
+          sudo apt-get install libghidra-dev -y
+          sudo apt-get install libghidra-data -y
 
       - name: Add the Testing Repository
         run: opam repo add bap git://github.com/BinaryAnalysisPlatform/opam-repository#testing
       - name: Install System Dependencies
-        run: opam depext -u bap
+        run: opam depext -u bap-extra
 
       - name: Install radare2 Dependencies
         run: opam depext -u bap-radare2
 
       - name: Cleanup the Caches
-        if: matrix.os == 'ubuntu-latest'
         run: sudo apt clean --yes
 
       - name: Build and Install BAP
-        run: opam install bap bap-radare2
+        run: opam install bap-extra bap-radare2
 
       - name: Checkout the Tests
         uses: actions/checkout@v2

.github/workflows/publish-docker-image.yml

@@ -21,4 +21,4 @@ jobs:
         with:
           push: true
           tags: binaryanalysisplatform/bap:latest
-          file: docker/ubuntu/xenial/Dockerfile
+          file: docker/ubuntu/bionic/Dockerfile

.github/workflows/release.yml

@@ -24,6 +24,12 @@ jobs:
           ocaml-compiler: ocaml-variants.4.11.2+flambda
           dune-cache: true
 
+      - name: Install Ghidra
+        run: |
+          sudo add-apt-repository ppa:ivg/ghidra -y
+          sudo apt-get install libghidra-dev -y
+          sudo apt-get install libghidra-data -y
+
       - name: Add the testing Repository
         run: opam repo add bap git://github.com/BinaryAnalysisPlatform/opam-repository#testing
       - name: Build deb packages

docker/ubuntu/bionic/Dockerfile

@@ -2,13 +2,16 @@ FROM ocaml/opam2:ubuntu-18.04
 
 WORKDIR /home/opam
 
-RUN sudo apt-get update  \
+RUN sudo add-apt-repository ppa:ivg/ghidra -y
+ && sudo apt-get install libghidra-dev -y
+ && sudo apt-get install libghidra-data -y
+ && sudo apt-get update  \
  && opam switch 4.09 \
  && eval "$(opam env)" \
  && opam remote set-url default https://opam.ocaml.org \
  && opam repo add bap git://github.com/BinaryAnalysisPlatform/opam-repository --all \
  && opam update \
- && opam depext --install bap --yes -j 1 \
+ && opam depext --install bap-extra --yes -j 1 \
  && opam clean -acrs \
  && rm -rf /home/opam/.opam/4.0[2-8,10] \
  && rm -rf /home/opam/.opam/4.09/.opam-switch/sources/* \

lib/arm/arm_target.ml

@@ -384,6 +384,7 @@ let enable_arch () =
 let llvm_a32 = CT.Language.declare ~package "llvm-armv7"
 let llvm_t32 = CT.Language.declare ~package "llvm-thumb"
 let llvm_a64 = CT.Language.declare ~package "llvm-aarch64"
+let pcode = CT.Language.declare ~package "pcode-arm"
 
 module Dis = Disasm_expert.Basic
 
@@ -459,6 +460,27 @@ let before_thumb2 t = t < LE.v6t2 || t < EB.v6t2
 let is_64bit t = LE.v8a <= t || EB.v8a <= t || Bi.v8a <= t
 let is_thumb_only t = LE.v7m <= t || EB.v7m <= t || Bi.v7m <= t
 
+let is_big t = Theory.Target.endianness t = Theory.Endianness.eb
+let is_little t = Theory.Target.endianness t = Theory.Endianness.le
+
+let register_pcode () =
+  Dis.register pcode @@ fun t ->
+  let triple = match is_64bit t,is_little t,is_big t with
+    | true,true,_ -> "ARM:LE:32:v8"
+    | true,_,true -> "ARM:BE:32:v8"
+    | true,_,_    -> "ARM:LEBE:32:v8LEInstruction"
+    | false,true,_ -> "ARM:LE:32:v7"
+    | false,_,true -> "ARM:BE:32:v7"
+    | false,_,_    -> "ARM:LEBE:32:v7LEInstruction" in
+  Dis.create ~backend:"ghidra" triple
+
+let enable_pcode () =
+  register_pcode ();
+  KB.promise Theory.Label.encoding @@ fun label ->
+  Theory.Label.target label >>| fun t ->
+  if is_arm t then pcode
+  else Theory.Language.unknown
+
 let guess_encoding interworking label target =
   if is_arm target then
     if is_64bit target then !!llvm_a64 else
@@ -472,7 +494,7 @@ let guess_encoding interworking label target =
         | false -> !!llvm_a32
   else !!CT.Language.unknown
 
-let enable_decoder ?interworking () =
+let enable_llvm ?interworking () =
   let open KB.Syntax in
   register llvm_a32 "armv7";
   register llvm_t32 "thumbv7" ~attrs:"+thumb2";
@@ -481,7 +503,9 @@ let enable_decoder ?interworking () =
   CT.Label.target label >>= guess_encoding interworking label
 
 
-let load ?interworking () =
+let load ?interworking ?(backend="llvm") () =
   enable_loader ();
   enable_arch ();
-  enable_decoder ?interworking ()
+  if String.equal backend "llvm"
+  then enable_llvm ?interworking ()
+  else enable_pcode ()

lib/arm/arm_target.mli

@@ -115,4 +115,4 @@ val llvm_a64 : Theory.language
     a symbol there with an odd address (which is used to indicate
     thumb encoding) then interworking is enabled.
 *)
-val load : ?interworking:bool -> unit -> unit
+val load : ?interworking:bool -> ?backend:string -> unit -> unit

lib/bap/bap.mli

@@ -2412,6 +2412,18 @@ module Std : sig
     val intrinsic: string Attribute.t
 
 
+    (** [label] a named code location.
+
+        @since 2.4.0  *)
+    val label : string Attribute.t
+
+
+    (** [goto] represents a control-flow transfer to a named label.
+
+        @since 2.4.0 *)
+    val goto : string Attribute.t
+
+
     (** Core Theory specification of BIL.  *)
     module Theory : sig
 
@@ -6976,6 +6988,40 @@ module Std : sig
         by evaluating in many languages, e.g. Python, Js, etc *)
     val pp_adt : Format.formatter -> t -> unit
 
+
+    (** Subinstruction Sequence Number.
+
+        A subinstruction sequence number plays the role of an address
+        for sub-instruction (which otherwise share the same physical
+        address).
+
+        Each subinstruction is having a unique address across the
+        whole program (not only unique across to other subinstructions
+        of the same instruction) and much like [Theory.Label.for_addr]
+        it is possible to get a label that corresponds to an
+        instruction with the given sequence number using
+        [Seqnum.label].
+
+        The sequence number is represented with an integer to enable
+        address arithemetics. A subinstruction that follows a
+        subinstruction with the sequence number [N] has the sequence
+        number [N+1].
+
+        @since 2.4.0
+    *)
+    module Seqnum : sig
+      type t = int
+
+
+      (** [label seqnum] returns the program label that corresponds
+          to [seqnum].  *)
+      val label : ?package:string -> t -> Theory.Label.t KB.t
+
+      (** [slot] for accessing the sequence number of a subinstruction.  *)
+      val slot : (Theory.program, t option) KB.slot
+    end
+
+
     (** {3 Prefix Tree}
         This module provides a trie data structure where a sequence of
         instructions is used as a key (and an individual instruction