The Capla language

Capla is a safe domain-specific programming language dedicated to low-level computer algebra programs. It aims at improving the confidence in low-level libraries such as GMP or BLAS by supplying an appropriate way of writing them while guaranteeing memory and temporal safety of the generated code.

Capla’s compiler is mostly written in Coq and uses the CompCert compiler as a backend. The language’s semantics has been formalized in Coq and the compiler’s correctness (correspondance between the behavior of source and generated programs) has been proved in Coq as well as the safety of the language.

It is currently in development. The compiler’s code is split into two parts:

Installation

The following dependencies are needed in order to install Capla’s compiler. The recommended way to install the dependencies is via opam, but using packages from a distribution’s repository might work as well.

The git repository of the compiler can be cloned like this:

git clone --recurse-submodules https://gitlab.inria.fr/fresco/capla/compiler.git

Build without global installation

In order to build and use the compiler without installing it, the following commands can be issued:

./configure x86_64-linux -libdir $(pwd)/runtime -bindir $(pwd)
make

Build with global installation

If one wants to install it globally, the compilation commands are as follows.

./configure x86_64-linux -prefix /usr
make
make install

Supported architectures

The x86-64-linux argument of the configure script can be replaced by another architecture. They can be listed by running ./configure --help. Please note that, currently, only 64-bit architectures are supported. This means that the compiler’s sources won’t compile if a 32-bit architecture is chosen.

Usage

Capla’s file extension is .b. In order to compile a program, the following command can be issued:

ccomp file.b

The usual option -S can be used to generate assembler code. Additionally, options -dnb, -db and -dcminor can be used to output files respectively in languages L1, L2 (described in the paper) and Cminor (CompCert has no C#minor printer but Cminor is very close to C#minor).

An unverified C backend can be used with option -dbc. For each .b file passed to the compiler, it generates a .c file. Option -S or -c must be used to avoid CompCert complaining about a missing main function.

Note that compiling a .b file on its own is of little interest, though, unless one wants to look at the Assembly (option -S) or produce an object file (option -c). Indeed, our language has currently no input/output mechanism. Hence, functions written in Capla may need to be called from another language.

Examples

The abstract syntax of the language can be found at the bottom of this page. Here is an example for the zdotu function of BLAS.

fun zdotu(n: i32, zx: [f64; 1 + (n - 1) * incx, 2], incx: i32,
                  zy: [f64; 1 + (n - 1) * incy, 2], incy: i32,
          res: mut [f64; 2]) {
  res[0] = 0.; res[1] = 0.;
  if n <= 0 return;

  if incx == 1 && incy == 1 {
    // assert (1 + (n - 1) * incx == n);
    // assert (1 + (n - 1) * incy == n);
    for i: i32 = 0 .. n {
      res[0] = res[0] + (zx[i, 0] * zy[i, 0] - zx[i, 1] * zy[i, 1]);
      res[1] = res[1] + (zx[i, 1] * zy[i, 0] + zx[i, 0] * zy[i, 1]);
    }
  } else {
    let ix: i32 = 0;
    let iy: i32 = 0;
    if incx < 0 { ix = (-n+1)*incx; }
    if incy < 0 { iy = (-n+1)*incy; }

    for i: i32 = 0 .. n {
      res[0] = res[0] + (zx[ix, 0] * zy[iy, 0] - zx[ix, 1] * zy[iy, 1]);
      res[1] = res[1] + (zx[ix, 1] * zy[iy, 0] + zx[ix, 0] * zy[iy, 1]);
      ix = ix + incx;
      iy = iy + incy;
    }
  }
}

More examples can be found in test files, and benchmarks files. These files can also be found respectively in the bfrontend/test and bfrontend/benchmarks directories of the cloned compiler repository. Test files can be built with command make b_tests from the bfrontend directory. The output binaries are located in bfrontend/test/output. Benchmarks can be run with command make b_benchmarks. Binaries and C outputs (for GCC and Clang) will be located in /tmp/benchmarks.

Dependencies for benchmarks

Dependencies to run benchmarks are the following ones.

Concrete language syntax

<prog>: <fundef> ...
<fundef>: <function> | <extern-function>
<extern-function>: extern fun <IDENT>( <param>, ... ) -> <TYPE>
<function>: fun <IDENT>( <param>, ... ) { <stmt> }
          | fun <IDENT>( <param>, ... ) -> <TYPE> { <stmt> }
<param>: <IDENT> ... : <typ>
       | <IDENT> ... : mut <typ>
<typ>: <TYPE>
     | [<typ> ; <arith-expr>, ...]
<stmt>: <atom-stmt> ;
      | <structure>
      | <structure> <stmt>
      | <atom-stmt> ; <stmt>
<init>: <expr> | alloc
<var-decl>: <IDENT> ... : <typ>
          | <IDENT> : <typ> = <init>
          | <IDENT> = <init>
<var-decls>: <var-decl>
           | <var-decl> , <var-decls>
<atom-stmt>: skip
           | let <var-decls>
           | <syn-path> = <expr>
           | assert <expr>
           | free <IDENT>
           | <IDENT> = <IDENT> ( <param>, ... )
           | <goto-stmt>
<goto-stmt>: error
           | return <expr>
           | return
           | continue
           | break
<structure>: if <expr> <block> else <block>
           | if <expr> <block>
           | for decr? <IDENT> : <typ> = <arith-expr> .. <arith-expr> <block>
           | for decr? <IDENT> = <arith-expr> .. <arith-expr> <block>
           | for decr? <IDENT> : <typ> = <arith-expr> .. <arith-expr> step <arith-expr> <block>
           | for decr? <IDENT> = <arith-expr> .. <arith-expr> step <arith-expr> <block>
           | while <expr> <block>
<block>: <goto-stmt>
       | <structure>
       | { <stmt> }
<atom>: <BOOL> | <ANNOT-INT> | <INT> | <FLOAT> | <ANNOT-FLOAT>
      | ( <typ> ) <atom>
      | ( <expr> )
      | <syn-path>
      | <IDENT> ( <param>, ... )
<syn-path>: <IDENT> <syn-path-elem> ...
<syn-path-elem>: [ <arith-expr>, ... ]
<expr>: <bor-expr> | <band-expr> | <bool-expr>
<bor-expr>: <bool-expr> || <bool-expr>
          | <bor-expr> || <bool-expr>
<band-expr>: <bool-expr> && <bool-expr>
           | <band-expr> && <bool-expr>
<bool-expr>: <arith-expr>
           | ! <atom>
           | <arith-expr> <binrel> <arith-expr>
<arith-expr>: <atom>
            | <unop> <atom>
            | <arith-expr> <binop> <arith-expr>
<binrel>: == | != | < | <= | > | >=
<binop>: + | - | * | / | & | `|` | ^ | << | >>
<unop>: - | ~
<TYPE>: void | bool | u8 | u16 | u32 | u64 | i8 | i16 | i32 | i64 | f32 | f64
<BOOL>: true | false
<ANNOT-INT>: <INT><TYPE>     # e.g., 4u16, 7i32
<ANNOT-FLOAT>: <FLOAT><TYPE> # e.g., 3.14159f64