From 05c2d0f45dcc632a11b4868b04776c1916b41454 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 3 Jan 2018 18:50:21 +0000 Subject: Lots of experimental changes on this branch * Changed comment syntax to C-style /* */ and // * References to registers and mutable variables are never created implicitly - a reference to a register or variable R is now created via the expression "ref R". References are assigned like "(*Y) = X", with "(*ref R) = X" being equivalent to "R = X". Everything is always explicit now, which simplifies the logic in the typechecker. There's also now an invariant that every id directly in a LEXP is mutable, which is actually required for our rewriter steps to be sound. * More flexible syntax for L-expressions to better support wierd power-idioms, some syntax sugar means that: X.GET(a, b, c) ==> _mod_GET(X, a, b, c) X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c) for setters, this can be combined with the (still somewhat poorly named) LEXP_memory construct, such that: X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y) Currently I use the _mod_ prefix for these 'modifier' functions, but we could omit that a la rust. * The register bits typedef construct no longer exists in the typechecker. This construct never worked consistently between backends and inc/dec vectors, and it can be easily replaced by structs with fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e. type operator ... ('n : Int) ('m : Int) = slice('n, 'm) struct cr = { CR0 : 32 ... 35, /* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */ CR1 : 36 ... 39, /* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */ CR2 : 40 ... 43, CR3 : 44 ... 47, CR4 : 48 ... 51, CR5 : 52 ... 55, CR6 : 56 ... 59, CR7 : 60 ... 63, } This greatly simplifies a lot of the logic in the typechecker, as it means that E_field is no longer ambiguously overloaded between records and register bit typedefs. This also makes writing semantics for these constructs much simpler. --- editors/sail2-mode.el | 9 ++----- language/l2.ott | 2 ++ src/ast_util.ml | 2 ++ src/initial_check.ml | 1 + src/interpreter.ml | 67 ++++++++++++++++++++++++++++++++++++++++++----- src/isail.ml | 2 +- src/lexer2.mll | 8 +++--- src/parse_ast.ml | 1 + src/parser2.mly | 2 ++ src/pretty_print_sail2.ml | 2 ++ src/process_file.ml | 1 + src/process_file.mli | 1 + src/rewriter.ml | 11 +++++++- src/rewriter.mli | 2 ++ src/rewrites.ml | 8 ++++++ src/rewrites.mli | 3 +++ src/sail.ml | 2 +- src/type_check.ml | 19 ++++++++------ src/value.ml | 15 +++++++++-- 19 files changed, 127 insertions(+), 31 deletions(-) diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index 7a420f14..26301d0f 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -34,13 +34,8 @@ (modify-syntax-entry ?_ "w" st) (modify-syntax-entry ?' "w" st) (modify-syntax-entry ?* ". 23" st) - (condition-case nil - (progn - (modify-syntax-entry ?\( "()1n" st) - (modify-syntax-entry ?\) ")(4n" st)) - (error ; XEmacs signals an error instead of ignoring `n'. - (modify-syntax-entry ?\( "()1" st) - (modify-syntax-entry ?\) ")(4" st))) + (modify-syntax-entry ?/ ". 124b" st) + (modify-syntax-entry ?\n "> b" st) st) "Syntax table for Sail2 mode") diff --git a/language/l2.ott b/language/l2.ott index ea4a8a6a..d26073f5 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -826,6 +826,8 @@ exp :: 'E_' ::= lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id +% | ref id :: :: ref + | deref exp :: :: deref {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} diff --git a/src/ast_util.ml b/src/ast_util.ml index 4407b7f1..7e966bf2 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -413,6 +413,7 @@ and map_letbind_annot_aux f = function and map_lexp_annot f (LEXP_aux (lexp, annot)) = LEXP_aux (map_lexp_annot_aux f lexp, f annot) and map_lexp_annot_aux f = function | LEXP_id id -> LEXP_id id + | LEXP_deref exp -> LEXP_deref (map_exp_annot f exp) | LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps) | LEXP_cast (typ, id) -> LEXP_cast (typ, id) | LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps) @@ -660,6 +661,7 @@ and string_of_pat (P_aux (pat, l)) = and string_of_lexp (LEXP_aux (lexp, _)) = match lexp with | LEXP_id v -> string_of_id v + | LEXP_deref exp -> "*(" ^ string_of_exp exp ^ ")" | LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" diff --git a/src/initial_check.ml b/src/initial_check.ml index 0915bc38..d7b69c4f 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -528,6 +528,7 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l LEXP_aux( (match exp with | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) + | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp) | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) | Parse_ast.E_tuple(tups) -> diff --git a/src/interpreter.ml b/src/interpreter.ml index 4fd75094..7e84f5c7 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -53,20 +53,30 @@ open Ast_util open Value type gstate = - { registers : value Bindings.t } + { registers : value Bindings.t; + letbinds : (Type_check.tannot letbind) list + } type lstate = { locals : value Bindings.t } type state = lstate * gstate -let initial_gstate = - { registers = Bindings.empty } +let rec ast_letbinds (Defs defs) = + match defs with + | [] -> [] + | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs) + | _ :: defs -> ast_letbinds (Defs defs) + +let initial_gstate ast = + { registers = Bindings.empty; + letbinds = ast_letbinds ast + } let initial_lstate = { locals = Bindings.empty } -let initial_state = initial_lstate, initial_gstate +let initial_state ast = initial_lstate, initial_gstate ast let value_of_lit (L_aux (l_aux, _)) = match l_aux with @@ -77,6 +87,11 @@ let value_of_lit (L_aux (l_aux, _)) = | L_false -> V_bool false | L_string str -> V_string str | L_num n -> V_int n + | L_hex str -> + Util.string_to_list str + |> List.map (fun c -> List.map (fun b -> V_bit b) (Sail_lib.hex_char c)) + |> List.concat + |> (fun v -> V_vector v) | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function @@ -175,7 +190,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps) | E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2) | E_tuple exps -> E_tuple (List.map (subst id value) exps) - | E_assign (lexp, exp) -> E_assign (lexp, subst id value exp) (* Shadowing... *) + | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *) | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) -> (* TODO: Fix shadowing *) E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body) @@ -189,6 +204,16 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = in wrap e_aux +and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) = + let wrap lexp_aux = LEXP_aux (lexp_aux, annot) in + let lexp_aux = match lexp_aux with + | LEXP_deref exp -> LEXP_deref (subst id value exp) + | LEXP_id id' -> LEXP_id id' + | LEXP_memory (f, exps) -> LEXP_memory (f, List.map (subst id value) exps) + | _ -> failwith ("subst lexp") + in + wrap lexp_aux + (**************************************************************************) (* 2. Expression Evaluation *) @@ -199,6 +224,14 @@ let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown)) let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp) +let rec build_letchain lbs (E_aux (_, annot) as exp) = + print_endline ("LETCHAIN " ^ string_of_exp exp); + match lbs with + | [] -> exp + | lb :: lbs -> + let exp = E_aux (E_let (lb, exp), annot) in + build_letchain lbs exp + let rec step (E_aux (e_aux, annot) as orig_exp) = let wrap e_aux' = return (E_aux (e_aux', annot)) in match e_aux with @@ -246,6 +279,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else failwith "Match failure" + | E_vector_update (vec, n, x) -> + wrap (E_app (mk_id "vector_update", [vec; n; x])) + (* otherwise left-to-right evaluation order for function applications *) | E_app (id, exps) -> let evaluated, unevaluated = Util.take_drop is_value exps in @@ -298,6 +334,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_throw exp when is_value exp -> throw (value_of_exp exp) | E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp') + | E_ref id -> return (exp_of_value (V_ref (string_of_id id))) | E_id id -> begin let open Type_check in @@ -312,6 +349,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = in return exp | Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals)) + | Local (Immutable, _) -> + let chain = build_letchain gstate.letbinds orig_exp in + print_endline "CHAINED"; + return chain | _ -> failwith "id" end @@ -355,6 +396,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let ul = (Parse_ast.Unknown, None) in let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in wrap (E_assign (lexp, exp')) + | E_assign (LEXP_aux (LEXP_vector (vec, n), _), exp) -> + let open Type_check in + let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in + let ul = (Parse_ast.Unknown, None) in + let exp' = E_aux (E_vector_update (vec_exp, n, exp), ul) in + wrap (E_assign (vec, exp')) | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> begin let open Type_check in @@ -366,6 +413,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = puts ({ lstate with locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp | _ -> failwith "Assign" end + | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) -> + step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp)) + | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) -> + let id = Id_aux (Id (coerce_ref (value_of_exp reference)), Parse_ast.Unknown) in + gets >>= fun (lstate, gstate) -> + puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp | E_assign _ -> assert false | E_try (exp, pexps) when is_value exp -> return exp @@ -443,7 +496,7 @@ let rec get_fundef id (Defs defs) = let stack_cont (_, _, cont) = cont let stack_string (str, _, _) = str let stack_state (_, lstate, _) = lstate - + type frame = | Done of state * value | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list @@ -473,5 +526,5 @@ let rec eval_frame ast = function print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear); Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack') | Yield (Assertion_failed msg), _ -> - failwith msg + failwith msg | _ -> assert false diff --git a/src/isail.ml b/src/isail.ml index 88835b8a..3df9c8f1 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -127,7 +127,7 @@ let handle_input input = | _ -> print_endline ("Unrecognised command " ^ input) else if input <> "" then let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in - current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state, return exp, []))) + current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state !interactive_ast, return exp, []))) else () end | Evaluation frame -> diff --git a/src/lexer2.mll b/src/lexer2.mll index b293046f..312183fa 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -231,6 +231,8 @@ rule token = parse | "->" { MinusGt } | "=>" { EqGt(r "=>") } | "<=" { (LtEq(r"<=")) } + | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } + | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } | "infix" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; Fixity (Infix, Big_int.of_string (Char.escaped p), op) } @@ -243,8 +245,6 @@ rule token = parse | operator as op { try M.find op !operators with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } - | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } - | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } | tyvar_start startident ident* as i { TyVar(r i) } | "~" { Id(r"~") } | startident ident* as i { if M.mem i kw_table then @@ -269,8 +269,8 @@ rule token = parse and comment pos depth = parse - | "(*" { comment pos (depth+1) lexbuf } - | "*)" { if depth = 0 then () + | "/*" { comment pos (depth+1) lexbuf } + | "*/" { if depth = 0 then () else if depth > 0 then comment pos (depth-1) lexbuf else assert false } | "\n" { Lexing.new_line lexbuf; diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 83b116a2..e84e8a60 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -268,6 +268,7 @@ exp_aux = (* Expression *) | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) | E_id of id (* identifier *) | E_ref of id + | E_deref of exp | E_lit of lit (* literal constant *) | E_cast of atyp * exp (* cast *) | E_app of id * (exp) list (* function application *) diff --git a/src/parser2.mly b/src/parser2.mly index ebe829c2..34ab8732 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -714,6 +714,8 @@ exp: { mk_exp (E_let ($2, $4)) $startpos $endpos } | Var atomic_exp Eq exp In exp { mk_exp (E_var ($2, $4, $6)) $startpos $endpos } + | Star atomic_exp + { mk_exp (E_deref $2) $startpos $endpos } | Lcurly block Rcurly { mk_exp (E_block $2) $startpos $endpos } | Return exp diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 22b6e9ee..930da39c 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -357,6 +357,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) = separate space [doc_atomic_exp exp; colon; doc_typ typ] | E_lit lit -> doc_lit lit | E_id id -> doc_id id + | E_ref id -> string "ref" ^^ space ^^ doc_id id | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) @@ -395,6 +396,7 @@ and doc_lexp (LEXP_aux (l_aux, _) as lexp) = and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = match l_aux with | LEXP_id id -> doc_id id + | LEXP_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) diff --git a/src/process_file.ml b/src/process_file.ml index d57127a4..8c00d37b 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -236,5 +236,6 @@ let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml +let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check diff --git a/src/process_file.mli b/src/process_file.mli index f99bdf54..86e8fb05 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -56,6 +56,7 @@ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_sil : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/rewriter.ml b/src/rewriter.ml index fb82b80f..53a43e5b 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -107,7 +107,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with let effsum = match e with | E_block es -> union_eff_exps es | E_nondet es -> union_eff_exps es - | E_id _ + | E_id _ | E_ref _ | E_lit _ -> eff | E_cast (_,e) -> effect_of e | E_app (f,es) -> @@ -339,6 +339,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp + | LEXP_deref exp -> rewrap (LEXP_deref (rewriters.rewrite_exp rewriters exp)) | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters) tupls)) | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps)) | LEXP_vector (lexp,exp) -> @@ -472,6 +473,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, { e_block : 'exp list -> 'exp_aux ; e_nondet : 'exp list -> 'exp_aux ; e_id : id -> 'exp_aux + ; e_ref : id -> 'exp_aux ; e_lit : lit -> 'exp_aux ; e_cast : Ast.typ * 'exp -> 'exp_aux ; e_app : id * 'exp list -> 'exp_aux @@ -512,6 +514,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_internal_value : Value.value -> 'exp_aux ; e_aux : 'exp_aux * 'a annot -> 'exp ; lEXP_id : id -> 'lexp_aux + ; lEXP_deref : 'exp -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux ; lEXP_cast : Ast.typ * id -> 'lexp_aux ; lEXP_tup : 'lexp list -> 'lexp_aux @@ -538,6 +541,7 @@ let rec fold_exp_aux alg = function | E_block es -> alg.e_block (List.map (fold_exp alg) es) | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es) | E_id id -> alg.e_id id + | E_ref id -> alg.e_ref id | E_lit lit -> alg.e_lit lit | E_cast (typ,e) -> alg.e_cast (typ, fold_exp alg e) | E_app (id,es) -> alg.e_app (id, List.map (fold_exp alg) es) @@ -588,6 +592,7 @@ let rec fold_exp_aux alg = function and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot) and fold_lexp_aux alg = function | LEXP_id id -> alg.lEXP_id id + | LEXP_deref exp -> alg.lEXP_deref (fold_exp alg exp) | LEXP_memory (id,es) -> alg.lEXP_memory (id, List.map (fold_exp alg) es) | LEXP_tup les -> alg.lEXP_tup (List.map (fold_lexp alg) les) | LEXP_cast (typ,id) -> alg.lEXP_cast (typ,id) @@ -618,6 +623,7 @@ let id_exp_alg = { e_block = (fun es -> E_block es) ; e_nondet = (fun es -> E_nondet es) ; e_id = (fun id -> E_id id) + ; e_ref = (fun id -> E_ref id) ; e_lit = (fun lit -> (E_lit lit)) ; e_cast = (fun (typ,e) -> E_cast (typ,e)) ; e_app = (fun (id,es) -> E_app (id,es)) @@ -658,6 +664,7 @@ let id_exp_alg = ; e_internal_value = (fun v -> E_internal_value v) ; e_aux = (fun (e,annot) -> E_aux (e,annot)) ; lEXP_id = (fun id -> LEXP_id id) + ; lEXP_deref = (fun e -> LEXP_deref e) ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es)) ; lEXP_cast = (fun (typ,id) -> LEXP_cast (typ,id)) ; lEXP_tup = (fun tups -> LEXP_tup tups) @@ -712,6 +719,7 @@ let compute_exp_alg bot join = { e_block = split_join (fun es -> E_block es) ; e_nondet = split_join (fun es -> E_nondet es) ; e_id = (fun id -> (bot, E_id id)) + ; e_ref = (fun id -> (bot, E_ref id)) ; e_lit = (fun lit -> (bot, E_lit lit)) ; e_cast = (fun (typ,(v,e)) -> (v, E_cast (typ,e))) ; e_app = (fun (id,es) -> split_join (fun es -> E_app (id,es)) es) @@ -760,6 +768,7 @@ let compute_exp_alg bot join = ; e_internal_value = (fun v -> (bot, E_internal_value v)) ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot))) ; lEXP_id = (fun id -> (bot, LEXP_id id)) + ; lEXP_deref = (fun (v, e) -> (v, LEXP_deref e)) ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es) ; lEXP_cast = (fun (typ,id) -> (bot, LEXP_cast (typ,id))) ; lEXP_tup = (fun ls -> diff --git a/src/rewriter.mli b/src/rewriter.mli index faa6a81a..c3c384bf 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -108,6 +108,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, { e_block : 'exp list -> 'exp_aux ; e_nondet : 'exp list -> 'exp_aux ; e_id : id -> 'exp_aux + ; e_ref : id -> 'exp_aux ; e_lit : lit -> 'exp_aux ; e_cast : Ast.typ * 'exp -> 'exp_aux ; e_app : id * 'exp list -> 'exp_aux @@ -148,6 +149,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_internal_value : Value.value -> 'exp_aux ; e_aux : 'exp_aux * 'a annot -> 'exp ; lEXP_id : id -> 'lexp_aux + ; lEXP_deref : 'exp -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux ; lEXP_cast : Ast.typ * id -> 'lexp_aux ; lEXP_tup : 'lexp list -> 'lexp_aux diff --git a/src/rewrites.ml b/src/rewrites.ml index a28352f5..87baa746 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -328,6 +328,7 @@ let rewrite_sizeof (Defs defs) = { e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es')) ; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es')) ; e_id = (fun id -> (E_id id, E_id id)) + ; e_ref = (fun id -> (E_ref id, E_ref id)) ; e_lit = (fun lit -> (E_lit lit, E_lit lit)) ; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e'))) ; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es'))) @@ -368,6 +369,7 @@ let rewrite_sizeof (Defs defs) = ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v)) ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot))) ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id)) + ; lEXP_deref = (fun (e, e') -> (LEXP_deref e, LEXP_deref e')) ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es'))) ; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id))) ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) @@ -2955,6 +2957,12 @@ let rewrite_defs_ocaml = [ (* ("separate_numbs", rewrite_defs_separate_numbs) *) ] +let rewrite_defs_interpreter = [ + ("constraint", rewrite_constraint); + ("trivial_sizeof", rewrite_trivial_sizeof); + ("sizeof", rewrite_sizeof); + ] + let rewrite_defs_sil = [ ("top_sort_defs", top_sort_defs); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); diff --git a/src/rewrites.mli b/src/rewrites.mli index ce24a4c4..8fceadff 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -57,6 +57,9 @@ val rewrite_undefined : bool -> tannot defs -> tannot defs (* Perform rewrites to exclude AST nodes not supported for ocaml out*) val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list +(* Perform rewrites to exclude AST nodes not supported for interpreter *) +val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list + (* Perform rewrites to exclude AST nodes not supported for lem out*) val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list diff --git a/src/sail.ml b/src/sail.ml index 519ec916..d4e2526e 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -216,7 +216,7 @@ let main() = begin (if !(opt_interactive) then - (interactive_ast := ast; interactive_env := type_envs) + (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs) else ()); (if !(opt_sanity) then diff --git a/src/type_check.ml b/src/type_check.ml index 907c23a5..d3967e7d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2489,10 +2489,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in match lexp_aux with + | LEXP_deref exp -> + let inferred_exp = infer_exp env exp in + begin match typ_of inferred_exp with + | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "ref" -> + subtyp l env typ vtyp; annot_lexp (LEXP_deref inferred_exp) typ, env + | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" -> + subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env + end | LEXP_id v -> begin match Env.lookup_id v env with - | Local (Immutable, Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _)) when string_of_id r = "ref" -> - subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env | Local (Immutable, _) | Enum _ | Union _ -> typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v) | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env @@ -2599,9 +2605,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | _ -> assert false in match typ_of access with - | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" -> - subtyp l env typ deref_typ; - annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env | _ when not is_immutable && is_register -> subtyp l env typ (typ_of access); annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env @@ -2627,9 +2630,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | _ -> assert false in match typ_of access with - | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" -> - subtyp l env typ deref_typ; - annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env | _ when not is_immutable && is_register -> subtyp l env typ (typ_of access); annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env @@ -3230,6 +3230,9 @@ and propagate_lexp_effect (LEXP_aux (lexp, annot)) = add_effect_lexp (LEXP_aux (p_lexp, annot)) eff and propagate_lexp_effect_aux = function | LEXP_id id -> LEXP_id id, no_effect + | LEXP_deref exp -> + let p_exp = propagate_exp_effect exp in + LEXP_deref p_exp, effect_of p_exp | LEXP_memory (id, exps) -> let p_exps = List.map propagate_exp_effect exps in LEXP_memory (id, p_exps), collect_effects p_exps diff --git a/src/value.ml b/src/value.ml index 59dadafe..d9690899 100644 --- a/src/value.ml +++ b/src/value.ml @@ -61,6 +61,7 @@ type value = | V_tuple of value list | V_unit | V_string of string + | V_ref of string | V_ctor of string * value list | V_record of value StringMap.t @@ -127,6 +128,10 @@ let coerce_string = function | V_string str -> str | _ -> assert false +let coerce_ref = function + | V_ref str -> str + | _ -> assert false + let unit_value = V_unit let value_eq_int = function @@ -221,17 +226,23 @@ let value_replicate_bits = function | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2)) | _ -> failwith "value replicate_bits" +let is_bit = function + | V_bit _ -> true + | _ -> false + let rec string_of_value = function - | V_vector vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) + | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) + | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]" | V_bool true -> "true" | V_bool false -> "false" | V_bit B0 -> "bitzero" | V_bit B1 -> "bitone" | V_int n -> Big_int.to_string n | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" - | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]" + | V_list vals -> "[|" ^ Util.string_of_list ", " string_of_value vals ^ "|]" | V_unit -> "()" | V_string str -> "\"" ^ str ^ "\"" + | V_ref str -> "ref " ^ str | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" | V_record record -> "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" -- cgit v1.2.3