Theory LLVM_Syntax

theory LLVM_Syntax
  imports
  "Deriving.Compare_Order_Instances"
  "HOL-Library.Mapping"
begin

(* Based on Haskell package llvm-hs-pure
   <http://hackage.haskell.org/package/llvm-hs-pure-6.2.1/docs/LLVM-AST.html> *)

(* We have to watchout for collisions. What if we have "Name ''%1''"? *)
datatype name = Name String.literal | UnName nat

instantiation name :: linorder
begin

fun less_name :: "name ⇒ name ⇒ bool" where
  "less_name (Name s) (Name s') = (s < s')"
|  "less_name (Name s) (UnName n) = True"
|  "less_name (UnName n) (Name s) = False"
|  "less_name (UnName n) (UnName n') = (n < n')"

definition less_eq_name :: "name ⇒ name ⇒ bool" where
  "less_eq_name x y = (x = y ∨ less x y)"

instance
proof -
  have a: "x < x ⟹ False" for x :: name
    by (cases x, auto)
  have b: "x < y ⟹ y < x ⟹ False" for x y :: name
    by (cases x; cases y; auto)
  have c: "¬ x < z ⟹ x < y ⟹ y < z ⟹ x = z" for x y z :: name
    by (cases x; cases y; cases z; auto)
  have d: "x < y ⟹ y < x ⟹ x = y" for x y :: name
    by (cases x; cases y; auto)
  have e: "x ≠ y ⟹ ¬ x < y ⟹ ¬ y < x ⟹ False" for x y :: name
    by (cases x; cases y; auto)
  show "OFCLASS(name, linorder_class)"
    by (intro_classes) (auto intro: a b c d e simp add: less_eq_name_def)
qed

end

derive (linorder) compare_order name

datatype 'a named = Named (named_name: name) (named_instruction: 'a) | Do (named_instruction: 'a)

(* RELEVANT LEMMAS AND FUNCTION *)

(* TODO:
What would be the best way to define the type here?
* use a nat and use mod in all operations
* IntType1 "1 word", IntType2 "2 word"
* is there a mix between the two possible

The first basic block in a function is special in two ways: it is immediately executed on entrance
to the function, and it is not allowed to have predecessor basic blocks (i.e. there can not be any
branches to the entry block of a function). Because the block can have no predecessors,
it also cannot have any PHI nodes. Should we encode this with the type system or with a predicate?

Should there be a one to one correspondence between llvm-hs and the isabelle types?

Should the map of registers return llvm_constants?

Bah, this sucks.
*)


datatype llvm_type =
  IntType (integerBits : nat) | ― ‹n-bit integer›
  VoidType

datatype llvm_constant =
  IntConstant (integerBits : nat) (integerValue : int)

datatype operand =
  LocalReference name |
  ConstantOperand llvm_constant

datatype parameter =
  Parameter llvm_type (parameter_name: name)

datatype integerPredicate = SLT | SGT | EQ | SGE | SLE | NE

datatype binop_instruction = Add | Sub | Xor | Mul

(* should probably be split into different instruction types *)
datatype instruction =
  Binop binop_instruction (operand0: operand) (operand1: operand) |
  Select operand (operand0: operand) (operand1: operand) |
  Call llvm_type name (arguments: "operand list") |
  Icmp integerPredicate (operand0: operand) (operand1: operand)

datatype terminator =
  Ret (return_operand: "operand option") |
  CondBr (condition: operand) (trueDest: name) (falseDest: name) |
  Br (dest: name)

type_synonym phi = "(name × (operand × name) list)"

datatype basic_block =
  Basic_block
   (name : name)
   (phis : "phi list")
   (instructions : "instruction named list")
   (terminator : "terminator named")

datatype llvm_fun =
  Function llvm_type (fun_name: name) (params: "parameter list") (hd_blocks: basic_block)
           (tl_blocks: "basic_block list")
  | ExternalFunction llvm_type (fun_name: name) (params: "parameter list")

datatype llvm_prog = Llvm_prog (funs : "llvm_fun list")

(* llvm definitions *)

type_synonym pos = "name × name × nat"
hide_type (open) LLVM_Syntax.pos

type_synonym stack = "(name, llvm_constant) mapping"

datatype frame = Frame (pos : LLVM_Syntax.pos) (stack : "stack")

fun update_stack where "update_stack f (Frame p s) = Frame p (f s)"
fun update_pos where "update_pos f (Frame p s) = Frame (f p) s"

lemma pos_update_pos_simp[simp]: "pos (update_pos f s) = f (pos s)"
  by (cases s) simp
lemma stack_update_pos_simp[simp]: "stack (update_pos f s) = stack s"
  by (cases s) simp
lemma pos_update_stack_simp[simp]: "pos (update_stack f s) = pos s"
  by (cases s) simp
lemma stack_update_stack_simp[simp]: "stack (update_stack f s) = f (stack s)"
  by (cases s) simp

datatype llvm_state = Llvm_state (frames : "frame list")

fun update_frames where "update_frames f (Llvm_state fs) = Llvm_state (f fs)"

lemma frames_simp[simp]: "update_frames f s = Llvm_state (f (frames s))"
  by (cases s)  simp

end