From 6eab69d0d1ed3ae60be0f877dc98f6b9bb63c406 Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 23 Aug 2019 07:06:22 -0700 Subject: [PATCH] Definie a prelim. AST for llair's semantics Summary: The AST is not complete on expressions, but it should have most of the important features. The representation is in some ways very different from the OCaml implementation, because the OCaml code uses mutation to build the CFG as an actual pointer graph in memory, and also because the expression representation is optimised for the backend. For the former, it should be easy to see that the AST here is isomorphic, representing the CFG with finite maps from block labels. The correspondence is less clear in the latter case, but the point here is not to model or verify implementation optimisations, but to give a semantics to llair as a language. Reviewed By: jberdine Differential Revision: D16807132 fbshipit-source-id: b0f64b3ec --- sledge/semantics/.gitignore | 4 + sledge/semantics/llairScript.sml | 174 +++++++++++++++++++++++++++++++ sledge/semantics/llvmScript.sml | 2 +- 3 files changed, 179 insertions(+), 1 deletion(-) create mode 100644 sledge/semantics/.gitignore create mode 100644 sledge/semantics/llairScript.sml diff --git a/sledge/semantics/.gitignore b/sledge/semantics/.gitignore new file mode 100644 index 000000000..338d9cd37 --- /dev/null +++ b/sledge/semantics/.gitignore @@ -0,0 +1,4 @@ +*Theory.* +.HOLMK +.hollogs +heap diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml new file mode 100644 index 000000000..a7d02aa96 --- /dev/null +++ b/sledge/semantics/llairScript.sml @@ -0,0 +1,174 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(* A mini-LLAIR model, based on the files in sledge/src/llair *) + +open HolKernel boolLib bossLib Parse; +open settingsTheory; + +new_theory "llair"; + +numLib.prefer_num (); + +(* ----- Abstract syntax ----- *) + +Datatype ` + typ = + | FunctionT typ (typ list) + | IntegerT num + | PointerT typ + | ArrayT typ num + | TupleT (typ list)`; + +Datatype ` + var = Var_name string`; + +Datatype ` + label = Lab_name string string`; + +(* Based on the constructor functions in exp.mli rather than the type definition *) +Datatype ` + exp = + | Var var + | Nondet + (* Args: function name, block name *) + | Label label + (* Args: byte, size *) + | Splat exp exp + (* Args: size, byte array *) + | Memory exp exp + (* Byte array concatenation *) + | Concat (exp list) + | Integer int typ + | Eq exp exp + | Lt exp exp + | Ult exp exp + | Sub typ exp exp + | Record (exp list) + (* Args: Record, index *) + | Select exp exp + (* Args: Record, index, value *) + | Update exp exp exp`; + +Datatype ` + inst = + (* Args: the list of variable, expression assignments to do *) + | Move ((var # exp) list) + (* Args: result reg, pointer, length *) + | Load var exp num + (* Args: pointer, value, length *) + | Store exp exp num + (* Args: destination, contents, length *) + | Memset exp exp exp + (* Args: destination, source, length *) + | Memcpy exp exp exp + (* Args: destination, source, length *) + | Memmov exp exp exp + (* Args : result, number of elements, size *) + | Alloc var exp exp + (* Args: pointer *) + | Free exp + (* Args: result reg *) + | NondetI var + | Abort`; + +Datatype ` + term = + (* Args: key, branch table, default exp *) + | Switch exp ((num # label) list) label + (* Args: int to switch on, jump table *) + | Iswitch exp (label list) + (* Args: result reg, function to call, arguments, return type of callee, + * return target, exception target *) + | Call var label (exp list) typ label label + | Return exp + | Throw exp + | Unreachable`; + +Datatype ` + block = <| cmnd : inst list; term : term |>`; + +(* The llair code doesn't have params here yet, but it will need to *) +Datatype ` + func = <| params : var list; + locals : var set; + entry : label; + cfg : label |-> block; + freturn : var; + fthrow : var |>`; + +(* The int is how much space the global needs *) +Datatype ` + global = <| var : var; init : (exp # int) option; typ: typ |>`; + +Datatype ` + llair = <| globals : global list; functions : label |-> func |>`; + +(* ----- Semantic states ----- *) + +(* TODO Given the similarities with LLVM, consider moving some definitions into + * a common predecessor theory *) + +Datatype ` + addr = A num`; + +(* 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 ` + v = + | LocV num + | SizeV num + | IntV int num + | AggV (v list)`; + +Datatype ` + pc = <| l : label; i : num |>`; + +Datatype ` + frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |>`; + +Datatype ` + state = + <| ip : pc; + globals : var |-> word64; + locals : var |-> v; + stack : frame list; + (* The set of allocated ranges. + * The llvm model had a bool to indicate whether the range is free-able + * or not, since the memory that the globals is in should never be freed. + * llair does not currently catch this error, so we won't either. If + * llair wants to catch the error in the future, then we can adapt the + * semantics. *) + allocations : (num # num) set; + (* A byte addressed heap *) + heap : addr |-> word8 |>`; + +(* ----- Semantic transitions ----- *) + +Definition eval_exp_def: + eval_exp = ARB: state -> exp -> v +End + +Definition update_results_def: + update_results xvs s = s with locals := s.locals |++ xvs +End + +Definition inc_pc_def: + inc_pc s = s with ip := (s.ip with i := s.ip.i + 1) +End + +(* +Inductive step_inst: + (step_inst (prog : llair) s + (Assign ves) + (inc_pc (update_results (map (λ(v,e). (v, eval_exp s e)) ves) s))) +End +*) + +export_theory (); diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index 24c473595..6bbef3036 100644 --- a/sledge/semantics/llvmScript.sml +++ b/sledge/semantics/llvmScript.sml @@ -36,7 +36,7 @@ Datatype ` reg = Reg string`; Datatype ` - glob_var = GlobName string`; + glob_var = Glob_var string`; Datatype ` fun_name = Fn string`;