Module Bap_c_abi.Arg

A monadic eDSL for argument passing semantics specification.

eDSL, built on top of the primitives described below.

This DSL helps in defining the abi processor's insert_args function. The DSL describes the semantics of argument passing that is then reified to the args structure. The DSL is a choice monad that enables describing the argument passing grammar using backtracking when the chosen strategy doesn't fit. The reject () operator will reject the current computation up until the nearest choice prompt, e.g., in the following example, computations e1, e2, and e3 are rejected and any side-effects that they might had are ignored and, instead the option2 computation is tried as if the previous sequence had never happend.

choice [
  sequence [e1; e2; e3; reject ()];
  option2;
]

Since the purpose of this DSL is to describe how the passed arguments are read in terms of BIL expressions, the generated specification could be seen as a grammar and the DSL itself as a parser combinator, specialized for describing ABI.

Example

Below we define the semantics of riscv32 and riscv64 targets. Both targets have fully specified register files with properly assigned roles and the register order matches with register names ordering, so we can use the simplified Arena creating functions. We have four independent arenas, two for passing in and out integer arguments, and two corresponding arenas for floating-point arguments.

We start with defining the integer calling convention by first determining how many register are needed to pass an argument. If the size of the argument couldn't be determined we reject the computation. Otherwise, if it fits into one register we try to pass it via a register fallback to memory if there are no registers available. If it requires two registers we first try to pass it as an aligned register pair (with the first part going through the nearest available even register). If we don't have enough aligned registers, we then split it in two parts and pass the first part in a register and the second part in the memory. Finally, if the size is greater than two words we pass it as an implicit reference.

The floating-point calling convention assumes the presence of the hardware floating-point registers but the specification is general enough to handle the soft floats convention, as any attempt to pass an argument via the hardware floating-point registers will be rejected since the corresponding arena will be empty.

The convention tries to pass a floating-point argument via the corresponding register file if it fits into a register otherwise it falls back to the integer registers. When an argument fits into the floating-point register we first try passing it through the floating-point file and if it is out of registers we use available integer registers (in riscv with hardware floating-point registers it is possible to pass 16 floating-point arguments all in registers) and finally use the last resort option of using the memory.

module Arg = C.Abi.Arg
open Arg.Let
open Arg.Syntax

let is_floating = function
  | `Basic {C.Type.Spec.t=#C.Type.real} -> true
  | _ -> false

let data_model t =
  let bits = Theory.Target.bits t in
  new C.Size.base (if bits = 32 then `ILP32 else `LP64)

let define t =
  let model = data_model t in
  C.Abi.define t model @@ fun _ {C.Type.Proto.return=r; args} ->
  let* iargs = Arg.Arena.iargs t in
  let* irets = Arg.Arena.irets t in
  let* fargs = Arg.Arena.fargs t in
  let* frets = Arg.Arena.frets t in

  (* integer calling convention *)
  let integer regs t =
    Arg.count regs t >>= function
    | None -> Arg.reject ()
    | Some 1 -> Arg.choice [
        Arg.register regs t;
        Arg.memory t;
      ]
    | Some 2 -> Arg.choice [
        Arg.sequence [
          Arg.align_even regs;
          Arg.registers ~limit:2 regs t;
        ];
        Arg.split_with_memory regs t;
        Arg.memory t;
      ]
    | Some _ -> Arg.reference regs t in

  (* floating-point calling convention *)
  let float iregs fregs t =
    Arg.count fregs t >>= function
    | Some 1 -> Arg.choice [
        Arg.register fregs t;
        Arg.register iregs t;
        Arg.memory t;
      ]
    | _ -> integer iregs t in

  let arg iregs fregs r =
    if is_floating r
    then float iregs fregs r
    else integer iregs r in

  Arg.define ?return:(match r with
      | `Void -> None
      | r -> Some (arg irets frets r))
    (Arg.List.iter args ~f:(fun (_,t) ->
         arg iargs fargs t));

  let () = List.iter ~f:define Bap_risv_target.[riscv32; riscv64]
type 'a t
type arena

an ordered expendable collection of registers

type semantics
type ctype = Bap_c_type.t
val define : ?return:unit t -> unit t -> semantics t

define ?return args the toplevel function for defining argument passing semantics.

The function has two entries, the optional return entry describes the semantics of passing of the return value, and the second section describes the semantics of passing the list of arguments.

The semantics is defined as a sequence of these two rules, with the return rule evaluated first. Therefore, if return is rejected the whole semantics will be rejected.

val register : arena -> ctype -> unit t

register arena t passes the argument of type t using the next available register in arena.

The computation is rejected if no registers are available; if t doesn't fit into a register in arena; or if size of t can't be determined.

val registers : ?rev:bool -> ?limit:int -> arena -> ctype -> unit t

registers arena t passes the argument in consecutive registers from arena.

Rejects the computation if arena doesn't have the necessary number of registers; the number of required registers is greater than limit; or if the size of t is unknown.

If rev is true, then the allocated registers will be used in the reversed order.

  • since 2.5.0 accepts the optional [rev] parameter.
val align_even : arena -> unit t

align_even arena ensures that the first available register in arena has even number.

Registers in an arena are enumerated from zero in the order of their appearence in the arena specification. This function removes, when necessary, a register form the arena, so that the next available register has an even number.

The computation is rejected if there are no more even registers in arena.

val deplet : arena -> unit t

deplet arena unconditionally consumes all registers in arena.

The computation is never rejected.

val discard : ?n:int -> arena -> unit t

discard arena discards one location from arena.

  • parameter n

    if specified discards n registers instead of one.

    The computation is never rejected, if the arena is empty nothing is changed.

  • since 2.5.0
val reference : arena -> ctype -> unit t

reference arena t passes a hidden pointer to t via the first available register in arena.

Rejects the computation if there are no available registers in arena. The size of t is not required.

Note, that reference and hidden are increasing the number of hidden arguments of a subroutine, but do not add the actual arguments.

val pointer : arena -> ctype -> unit t

pointer arena t passes argument t as a pointer.

Rejects the computation if arena is empty. The size of t is not required.

  • since 2.5.0
val hidden : ctype -> unit t

hidden t inserts a hidden pointer to t into the next available stack slot.

The computation is rejected if the target doesn't have a stack.

  • since 2.5.0
val memory : ctype -> unit t

memory t passes the argument of type t in the next available stack slot.

Rejects the computation if the size of t is not known or if the target doesn't have a register with the stack pointer role.

The address of the slot is aligned corresponding to the alignment requirements of t but no less than the minimal data alignment requirements of the architecture or the natural alignment of the stack pointer.

Note, passing a number arguments via a descending stack using memory will pass the arguments in the right-to-left (RTL aka C) order, i.e., the first passed argument will end up at the bottom (will have the minimal address). Use push if you want the left-to-right order.

val rebase : int -> unit t

rebase off rebases the stack position by n words.

  • since 2.5.0
val split : arena -> arena -> ctype -> unit t

split a1 a2 t passes the lower half of the value via registers in the arena a1 and the higher via the registers in the arena a2.

The compuation is rejected if either arean doesn't have enough registers to pass its half, or if the size of t is odd or unknown.

  • since 2.5.0
val split_with_memory : ?rev:bool -> ?limit:int -> arena -> ctype -> unit t

split_with_memory arena t passes the low order part of the value in a registers (if available) and the rest in the memory.

The size of the part that is passed via the registers is equal to the number of avaliable registers, but not greater than the limit (if specified). The part that is passed via the stack is aligned to the stack boundary.

If rev is true then pass the object in the reversed order.

Rejects the computation if the size of t is not known; if arena is empty; or if some other argument is already passed via memory.

@after 2.5.0 accepts the rev parameter. @after 2.5.0 accepts the limit parameter.

@after 2.5.0 passes as much as possible (up to the limit) of the object via registers.

  • before 2.5.0

    was passing at most one word via registers.

val push : ctype -> unit t

push t pushes the argument of type t via stack.

Rejects the computation if the size of t is not known.

The address of the slot is aligned corresponding to the alignment requirements of t but no less than the minimal data alignment requirements of the architecture or the natural alignment of the stack pointer.

When passing a number of arguments via a descending stack, the last pushed argument will be at the bottom of the stack, i.e., will have the minimal address. This corresponds to the LTR aka Pascal ordering.

val count : arena -> ctype -> int option t

count arena t counts the number of registers need to pass a value of type t.

Returns None if the size of t is not known or if the arena size is empty.

val size : ctype -> int t

size t is the size in bits of an object of type t.

The computation is rejected if the size is unknown, i.e., the type is incomplete.

  • since 2.5.0
val require : bool -> unit t

require cnd rejects the computation if cnd doesn't hold.

  • since 2.5.0
val either : 'a t -> 'a t -> 'a t

either option1 option2 tries to pass using option1 and if it is rejected uses option2.

For example, either (register x) (memory x) tries to pass x via a register and if it is not possible (either because x doesn't fit into a register or there are no registers available) tries to pass it via memory.

val choice : 'a t list -> 'a t

choice [o1 o2 ... oN] tries options in order until the first one that is not rejected.

module Language : sig ... end

A high-level ABI-specification language.

reify t size args compiles the argument passing specification.

If the spec is not rejected the returned structure will contain the reification of the argument passing semantics.

include Monads.Std.Monad.S with type 'a t := 'a t
val void : 'a t -> unit t

void m computes m and discrards the result.

val sequence : unit t list -> unit t

sequence xs computes a sequence of computations xs in the left to right order.

val forever : 'a t -> 'b t

forever xs creates a computationt that never returns.

module Fn : sig ... end

Various function combinators lifted into the Kleisli category.

module Pair : sig ... end

The pair interface lifted into the monad.

module Triple : sig ... end

The triple interface lifted into a monad.

module Lift : sig ... end

Lifts functions into the monad.

module Exn : sig ... end

Interacting between monads and language exceptions

module Collection : sig ... end

Lifts collection interface into the monad.

module List : Collection.S with type 'a t := 'a list

The Monad.Collection.S interface for lists

module Seq : Collection.S with type 'a t := 'a Core_kernel.Sequence.t

The Monad.Collection.S interface for sequences

include Monads.Std.Monad.Syntax.S with type 'a t := 'a t
val (>=>) : ('a -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t

f >=> g is fun x -> f x >>= g

val (!!) : 'a -> 'a t

!!x is return x

val (!$) : ('a -> 'b) -> 'a t -> 'b t

!$f is Lift.unary f

val (!$$) : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t

!$$f is Lift.binary f

val (!$$$) : ('a -> 'b -> 'c -> 'd) -> 'a t -> 'b t -> 'c t -> 'd t

!$$$f is Lift.ternary f

val (!$$$$) : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a t -> 'b t -> 'c t -> 'd t -> 'e t

!$$$$f is Lift.quaternary f

val (!$$$$$) : ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a t -> 'b t -> 'c t -> 'd t -> 'e t -> 'f t

!$$$$$f is Lift.quinary f

include Monads.Std.Monad.Syntax.Let.S with type 'a t := 'a t
val let* : 'a t -> ('a -> 'b t) -> 'b t

let* r = f x in b is f x >>= fun r -> b

val and* : 'a t -> 'b t -> ('a * 'b) t

monoidal product

val let+ : 'a t -> ('a -> 'b) -> 'b t

let+ r = f x in b is f x >>| fun r -> b

val and+ : 'a t -> 'b t -> ('a * 'b) t

monoidal product

include Core_kernel.Monad.S with type 'a t := 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val (>>|) : 'a t -> ('a -> 'b) -> 'b t
module Monad_infix : sig ... end
val bind : 'a t -> f:('a -> 'b t) -> 'b t
val return : 'a -> 'a t
val map : 'a t -> f:('a -> 'b) -> 'b t
val join : 'a t t -> 'a t
val ignore_m : 'a t -> unit t
val all : 'a t list -> 'a list t
val all_unit : unit t list -> unit t
module Let_syntax : sig ... end
module Let : Monads.Std.Monad.Syntax.Let.S with type 'a t := 'a t

Monadic operators, see Monad.Syntax.S for more.

module Syntax : Monads.Std.Monad.Syntax.S with type 'a t := 'a t

Monadic operators, see Monad.Syntax.S for more.

include Monads.Std.Monad.Choice.S with type 'a t := 'a t
include Monads.Std.Monad.Choice.Basic with type 'a t := 'a t
val pure : 'a -> 'a t

pure x creates a computation that results in x.

val zero : unit -> 'a t

zero () creates a computation that has no result.

val accept : 'a -> 'a t

accept x accepts x as a result of computation. (Same as pure x.

val reject : unit -> 'a t

reject () rejects the rest of computation sequence, and terminate the computation with the zero result (Same as zero ()

val guard : bool -> unit t

guard cond ensures cond is true in the rest of computation. Otherwise the rest of the computation is rejected.

val on : bool -> unit t -> unit t

on cond x computes x only iff cond is true

val unless : bool -> unit t -> unit t

unless cond x computes x unless cond is true.

module Arena : sig ... end

An ordered collection of locations.