From 85243ada622947fd0d977fc6c310c2554fcb95df Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 23 Aug 2019 07:12:27 -0700 Subject: [PATCH] Update for improved HOL syntax for Datatypes Summary: HOL now lets us omit quotations on Datatypes and make them look more like the other new-style HOL definitions. Reviewed By: jberdine Differential Revision: D16983934 fbshipit-source-id: f8ef3abb5 --- sledge/semantics/llairScript.sml | 75 +++++++++------ sledge/semantics/llvmScript.sml | 114 ++++++++++++++--------- sledge/semantics/llvm_to_llairScript.sml | 5 +- 3 files changed, 116 insertions(+), 78 deletions(-) diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml index 5c6657ce4..0083bbb22 100644 --- a/sledge/semantics/llairScript.sml +++ b/sledge/semantics/llairScript.sml @@ -16,22 +16,25 @@ numLib.prefer_num (); (* ----- Abstract syntax ----- *) -Datatype ` +Datatype: typ = | FunctionT typ (typ list) | IntegerT num | PointerT typ | ArrayT typ num - | TupleT (typ list)`; + | TupleT (typ list) +End -Datatype ` - var = Var_name string`; +Datatype: + var = Var_name string +End -Datatype ` - label = Lab_name string string`; +Datatype: + label = Lab_name string string +End (* Based on the constructor functions in exp.mli rather than the type definition *) -Datatype ` +Datatype: exp = | Var var | Nondet @@ -52,9 +55,10 @@ Datatype ` (* Args: Record, index *) | Select exp exp (* Args: Record, index, value *) - | Update exp exp exp`; + | Update exp exp exp +End -Datatype ` +Datatype: inst = (* Args: the list of variable, expression assignments to do *) | Move ((var # exp) list) @@ -74,9 +78,10 @@ Datatype ` | Free exp (* Args: result reg *) | NondetI var - | Abort`; + | Abort +End -Datatype ` +Datatype: term = (* Args: key, branch table, default exp *) | Switch exp ((num # label) list) label @@ -87,53 +92,62 @@ Datatype ` | Call var label (exp list) typ label label | Return exp | Throw exp - | Unreachable`; + | Unreachable +End -Datatype ` - block = <| cmnd : inst list; term : term |>`; +Datatype: + block = <| cmnd : inst list; term : term |> +End (* The llair code doesn't have params here yet, but it will need to *) -Datatype ` +Datatype: func = <| params : var list; locals : var set; entry : label; cfg : (label, block) alist; freturn : var; - fthrow : var |>`; + fthrow : var |> +End (* The int is how much space the global needs *) -Datatype ` - global = <| var : var; init : (exp # int) option; typ: typ |>`; +Datatype: + global = <| var : var; init : (exp # int) option; typ: typ |> +End -Datatype ` - llair = <| globals : global list; functions : (label, func) alist |>`; +Datatype: + llair = <| globals : global list; functions : (label, func) alist |> +End (* ----- Semantic states ----- *) (* TODO Given the similarities with LLVM, consider moving some definitions into * a common predecessor theory *) -Datatype ` - addr = A num`; +Datatype: + addr = A num +End (* These are the values that can be stored in registers. The implementation uses * integers with a bit-width to represent numbers, and keeps locations and sizes * separate. *) -Datatype ` +Datatype: v = | LocV num | SizeV num | IntV int num - | AggV (v list)`; + | AggV (v list) +End -Datatype ` - pc = <| l : label; i : num |>`; +Datatype: + pc = <| l : label; i : num |> +End -Datatype ` - frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |>`; +Datatype: + frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |> +End -Datatype ` +Datatype: state = <| ip : pc; globals : var |-> word64; @@ -147,7 +161,8 @@ Datatype ` * semantics. *) allocations : (num # num) set; (* A byte addressed heap *) - heap : addr |-> word8 |>`; + heap : addr |-> word8 |> +End (* ----- Semantic transitions ----- *) diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index 7ca53c278..2f679a605 100644 --- a/sledge/semantics/llvmScript.sml +++ b/sledge/semantics/llvmScript.sml @@ -18,47 +18,56 @@ numLib.prefer_num (); (* ----- Abstract syntax ----- *) (* Only support 1, 8, 32, and 64 bit words for now *) -Datatype ` - size = W1 | W8 | W32 | W64`; +Datatype: + size = W1 | W8 | W32 | W64 +End -Datatype ` +Datatype: ty = | FunT ty (ty list) | IntT size | PtrT ty | ArrT num ty - | StrT (ty list)`; + | StrT (ty list) +End -Datatype ` - label = Lab string`; +Datatype: + label = Lab string +End -Datatype ` - reg = Reg string`; +Datatype: + reg = Reg string +End -Datatype ` - glob_var = Glob_var string`; +Datatype: + glob_var = Glob_var string +End -Datatype ` - fun_name = Fn string`; +Datatype: + fun_name = Fn string +End -Datatype ` +Datatype: const = | IntC size int | StrC ((ty # const) list) | ArrC ((ty # const) list) | GepC ty const (ty # const) ((ty # const) list) | GlobalC glob_var - | UndefC`; + | UndefC +End -Datatype ` - arg = Constant const | Variable reg`; +Datatype: + arg = Constant const | Variable reg +End -type_abbrev ("targ", ``:ty # arg``); +Type targ = ``:ty # arg`` -Datatype ` - cond = Eq | Ult | Slt`; +Datatype: + cond = Eq | Ult | Slt +End -Datatype ` +Datatype: instr = (* Terminators *) | Ret targ @@ -82,33 +91,40 @@ Datatype ` | Cxa_throw arg arg arg | Cxa_begin_catch reg arg | Cxa_end_catch - | Cxa_get_exception_ptr reg arg`; + | Cxa_get_exception_ptr reg arg +End -Datatype ` - phi = Phi reg ty ((label option, arg) alist)`; +Datatype: + phi = Phi reg ty ((label option, arg) alist) +End -Datatype ` - clause = Catch targ`; +Datatype: + clause = Catch targ +End -Datatype ` - landingpad = Landingpad ty bool (clause list)`; +Datatype: + landingpad = Landingpad ty bool (clause list) +End -Datatype ` +Datatype: blockHeader = | Entry - | Head (phi list) (landingpad option)`; + | Head (phi list) (landingpad option) +End -Datatype ` - block = <| h : blockHeader; body : instr list |>`; +Datatype: + block = <| h : blockHeader; body : instr list |> +End -Datatype ` +Datatype: def = <| r : ty; params : reg list; (* None -> entry block, and Some name -> non-entry block *) - blocks : (label option, block) alist |>`; + blocks : (label option, block) alist |> +End -type_abbrev ("prog", ``:(fun_name, def) alist``); +Type prog = ``:(fun_name, def) alist`` Definition terminator_def: (terminator (Ret _) ⇔ T) ∧ @@ -120,10 +136,11 @@ End (* ----- Semantic states ----- *) -Datatype ` - addr = A num`; +Datatype: + addr = A num +End -Datatype ` +Datatype: v = | W1V word1 | W8V word8 @@ -131,18 +148,22 @@ Datatype ` | W64V word64 | AggV (v list) | PtrV word64 - | UndefV`; + | UndefV +End -Datatype ` - pv = <| poison : bool; value : v |>`; +Datatype: + pv = <| poison : bool; value : v |> +End -Datatype ` - pc = <| f : fun_name; b : label option; i : num |>`; +Datatype: + pc = <| f : fun_name; b : label option; i : num |> +End -Datatype ` - frame = <| ret : pc; saved_locals : reg |-> pv; result_var : reg; stack_allocs : addr list |>`; +Datatype: + frame = <| ret : pc; saved_locals : reg |-> pv; result_var : reg; stack_allocs : addr list |> +End -Datatype ` +Datatype: state = <| ip : pc; (* Keep the size of the global with its memory address *) @@ -153,7 +174,8 @@ Datatype ` * free-able or not *) allocations : (bool # num # num) set; (* A byte addressed heap, with a poison tag *) - heap : addr |-> bool # word8 |>`; + heap : addr |-> bool # word8 |> +End (* ----- Things about types ----- *) diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml index 5813cf6e5..007a0d4bc 100644 --- a/sledge/semantics/llvm_to_llairScript.sml +++ b/sledge/semantics/llvm_to_llairScript.sml @@ -180,12 +180,13 @@ Definition translate_instr_to_term_def: Iswitch (translate_arg emap a) [translate_label f l2; translate_label f l1] End -Datatype ` +Datatype: instr_class = | Exp reg | Non_exp | Term - | Call`; + | Call +End Definition classify_instr_def: (classify_instr (Call _ _ _ _) = Call) ∧