C: Refactor C backend

Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.

The various parts of the C backend are now in the src/jib/ subdirectory

src/jib/anf.ml         - Sail->ANF translation
src/jib/jib_util.ml    - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml   - Jib->C code generator and optimizations

Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)

The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.

The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.

Additional improvements:

The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.

jib.ott now has some more comments explaining various parts of the Jib
AST.

A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.

1 files changed, 0 insertions, 162 deletions

diff --git a/src/bytecode_interpreter.ml b/src/bytecode_interpreter.ml
deleted file mode 100644
index 398e0c9d..00000000
--- a/src/bytecode_interpreter.ml
+++ /dev/null
@@ -1,162 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-open Ast
-open Ast_util
-open Bytecode
-open Bytecode_util
-
-module StringMap = Map.Make(String)
-
-type 'a frame = {
-    jump_table : int StringMap.t;
-    locals : 'a Bindings.t;
-    pc : int;
-    instrs : instr array
-  }
-
-type 'a gstate = {
-    globals : 'a Bindings.t;
-    cdefs : cdef list
-  }
-
-type 'a stack = {
-    top : 'a frame;
-    ret : ('a -> 'a frame) list
-  }
-
-let make_jump_table instrs =
-  let rec aux n = function
-    | I_aux (I_label label, _) :: instrs -> StringMap.add label n (aux (n + 1) instrs)
-    | _ :: instrs -> aux (n + 1) instrs
-    | [] -> StringMap.empty
-  in
-  aux 0 instrs
-
-let new_gstate cdefs = {
-    globals = Bindings.empty;
-    cdefs = cdefs
-  }
-
-let new_stack instrs = {
-    top = {
-      jump_table = make_jump_table instrs;
-      locals = Bindings.empty;
-      pc = 0;
-      instrs = Array.of_list instrs
-    };
-    ret = []
-  }
-
-let with_top stack f =
-  { stack with top = f (stack.top) }
-
-let eval_fragment gstate locals = function
-  | F_id id ->
-     begin match Bindings.find_opt id locals with
-     | Some vl -> vl
-     | None ->
-        begin match Bindings.find_opt id gstate.globals with
-        | Some vl -> vl
-        | None -> failwith "Identifier not found"
-        end
-     end
-  | F_lit vl -> vl
-  | _ -> failwith "Cannot eval fragment"
-
-let is_function id = function
-  | CDEF_fundef (id', _, _, _) when Id.compare id id' = 0 -> true
-  | _ -> false
-
-let step (gstate, stack) =
-  let I_aux (instr_aux, (_, l)) = stack.top.instrs.(stack.top.pc) in
-  match instr_aux with
-  | I_decl _ ->
-     gstate, with_top stack (fun frame -> { frame with pc = frame.pc + 1 })
-
-  | I_init (_, id, (fragment, _)) ->
-     let vl = eval_fragment gstate stack.top.locals fragment in
-     gstate,
-     with_top stack (fun frame -> { frame with pc = frame.pc + 1; locals = Bindings.add id vl frame.locals })
-
-  | I_jump ((fragment, _), label) ->
-     let vl = eval_fragment gstate stack.top.locals fragment in
-     gstate,
-     begin match vl with
-     | V_bool true ->
-        with_top stack (fun frame -> { frame with pc = StringMap.find label frame.jump_table })
-     | V_bool false ->
-        with_top stack (fun frame -> { frame with pc = frame.pc + 1 })
-     | _ ->
-        failwith "Type error"
-     end
-
-  | I_funcall (clexp, _, id, cvals) ->
-     let args = List.map (fun (fragment, _) -> eval_fragment gstate stack.top.locals fragment) cvals in
-     let params, instrs =
-       match List.find_opt (is_function id) gstate.cdefs with
-       | Some (CDEF_fundef (_, _, params, instrs)) -> params, instrs
-       | _ -> failwith "Function not found"
-     in
-     gstate,
-     {
-       top = {
-         jump_table = make_jump_table instrs;
-         locals = List.fold_left2 (fun locals param arg -> Bindings.add param arg locals) Bindings.empty params args;
-         pc = 0;
-         instrs = Array.of_list instrs;
-       };
-       ret = (fun vl -> { stack.top with pc = stack.top.pc + 1 }) :: stack.ret
-     }
-
-  | I_goto label ->
-     gstate, with_top stack (fun frame -> { frame with pc = StringMap.find label frame.jump_table })
-
-  | _ -> raise (Reporting.err_unreachable l __POS__ "Unhandled instruction")