Module Bap_c_abi.Arg

A monadic eDSL for argument passing semantics specification.

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 backtracing 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]