diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constraint.ml | 8 | ||||
| -rw-r--r-- | src/initial_check.ml | 4 | ||||
| -rw-r--r-- | src/initial_check.mli | 1 | ||||
| -rw-r--r-- | src/isail.ml | 51 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 60 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 1 |
7 files changed, 105 insertions, 21 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 7debc902..1bd6a437 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -278,11 +278,9 @@ let call_smt' l constraints : smt_result = let rec input_lines chan = function | 0 -> [] | n -> - begin - let l = input_line chan in - let ls = input_lines chan (n - 1) in - l :: ls - end + let l = input_line chan in + let ls = input_lines chan (n - 1) in + l :: ls in let digest = Digest.string smt_file in diff --git a/src/initial_check.ml b/src/initial_check.ml index b3d24820..691acd81 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1036,6 +1036,10 @@ let process_ast ?generate:(generate=true) defs = else ast +let ast_of_def_string_with f str = + let def = Parser.def_eof Lexer.token (Lexing.from_string str) in + process_ast (f (P.Defs [def])) + let ast_of_def_string str = let def = Parser.def_eof Lexer.token (Lexing.from_string str) in process_ast (P.Defs [def]) diff --git a/src/initial_check.mli b/src/initial_check.mli index b96a9efb..b41b1818 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -98,6 +98,7 @@ val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs val extern_of_string : id -> string -> unit def val val_spec_of_string : id -> string -> unit def val ast_of_def_string : string -> unit defs +val ast_of_def_string_with : (Parse_ast.defs -> Parse_ast.defs) -> string -> unit defs val exp_of_string : string -> unit exp val typ_of_string : string -> typ val constraint_of_string : string -> n_constraint diff --git a/src/isail.ml b/src/isail.ml index 8f71a809..4f63c732 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -181,6 +181,14 @@ let help = function "(:i | :infer) <expression> - Infer the type of an expression." | ":v" | ":verbose" -> "(:v | :verbose) - Increase the verbosity level, or reset to zero at max verbosity." + | ":b" | ":bind" -> + "(:b | :bind) <id> : <typ> - Declare a variable of a specific type" + | ":let" -> + ":let <id> = <exp> - Bind a variable to expression" + | ":def" -> + ":def <definition> - Evaluate a top-level definition" + | ":prove" -> + ":prove <constraint> - Try to prove a constraint in the top-level environment" | ":commands" -> ":commands - List all available commands." | ":help" -> @@ -311,9 +319,6 @@ let handle_input' input = let exp = Type_check.infer_exp !Interactive.env exp in pretty_sail stdout (doc_typ (Type_check.typ_of exp)); print_newline () - | ":canon" -> - let typ = Initial_check.typ_of_string arg in - print_endline (string_of_typ (Type_check.canonicalize !Interactive.env typ)) | ":prove" -> let nc = Initial_check.constraint_of_string arg in print_endline (string_of_bool (Type_check.prove __POS__ !Interactive.env nc)) @@ -328,8 +333,8 @@ let handle_input' input = else print_endline "Invalid argument for :clear, expected either :clear on or :clear off" | ":commands" -> let commands = - [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help :output :option"; - "Normal mode commands - :elf :(l)oad :(u)nload"; + [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :clear :commands :help :output :option"; + "Normal mode commands - :elf :(l)oad :(u)nload :let :(b)ind"; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; ":(c)ommand can be called as either :c or :command." ] @@ -350,16 +355,6 @@ let handle_input' input = interactive_state := initial_state !Interactive.ast Value.primops | ":pretty" -> print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast)) - | ":compile" -> - (* - let open PPrint in - let open C_backend in - let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in - let ast, env = Specialize.(specialize typ_ord_specialization ast !Interactive.env) in - let ctx = initial_ctx env in - interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast - *) - () | ":ir" -> print_endline arg; let open Jib in @@ -408,6 +403,32 @@ let handle_input' input = (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false; Process_file.clear_symbols () + | ":b" | ":bind" -> + let args = Str.split (Str.regexp " +") arg in + begin match args with + | v :: ":" :: args -> + let typ = Initial_check.typ_of_string (String.concat " " args) in + let _, env, _ = Type_check.bind_pat !Interactive.env (mk_pat (P_id (mk_id v))) typ in + Interactive.env := env + | _ -> print_endline "Invalid arguments for :bind" + end + | ":let" -> + let args = Str.split (Str.regexp " +") arg in + begin match args with + | v :: "=" :: args -> + let exp = Initial_check.exp_of_string (String.concat " " args) in + let ast, env = Type_check.check !Interactive.env (Defs [DEF_val (mk_letbind (mk_pat (P_id (mk_id v))) exp)]) in + Interactive.ast := append_ast !Interactive.ast ast; + Interactive.env := env; + interactive_state := initial_state !Interactive.ast Value.primops; + | _ -> print_endline "Invalid arguments for :let" + end + | ":def" -> + let ast = Initial_check.ast_of_def_string_with (Process_file.preprocess_ast options) arg in + let ast, env = Type_check.check !Interactive.env ast in + Interactive.ast := append_ast !Interactive.ast ast; + Interactive.env := env; + interactive_state := initial_state !Interactive.ast Value.primops; | _ -> unrecognised_command cmd end | Expression str -> diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index e90570e1..9ce3c3f0 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -358,6 +358,7 @@ let dominance_frontiers graph root idom children = type ssa_elem = | Phi of Ast.id * Ast.id list + | Pi of Jib.cval list let place_phi_functions graph df = let defsites = ref Bindings.empty in @@ -500,6 +501,7 @@ let rename_variables graph root children = counts := Bindings.add id i !counts; push_stack id i; Phi (append_id id ("_" ^ string_of_int i), args) + | Pi _ -> assert false (* Should not be introduced at this point *) in let fix_phi j = function @@ -510,6 +512,7 @@ let rename_variables graph root children = append_id a ("_" ^ string_of_int i) else a) ids) + | Pi _ -> assert false (* Should not be introduced at this point *) in let rec rename n = @@ -538,6 +541,53 @@ let rename_variables graph root children = in rename root +let place_pi_functions graph start idom children = + let get_guard = function + | CF_guard guard -> [guard] + | _ -> [] + in + let get_pi_contents ssanodes = + List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes) + in + + let rec go n = + begin match graph.nodes.(n) with + | Some ((ssa, cfnode), preds, succs) -> + let p = idom.(n) in + if p <> -1 then + begin match graph.nodes.(p) with + | Some ((dom_ssa, _), _, _) -> + let args = get_guard cfnode @ get_pi_contents dom_ssa in + graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs) + | None -> assert false + end + | None -> assert false + end; + IntSet.iter go children.(n) + in + go start + +(** Remove p nodes. Assumes the graph is acyclic. *) +let remove_nodes remove_cf graph = + for n = 0 to graph.next - 1 do + match graph.nodes.(n) with + | Some ((_, cfnode), preds, succs) when remove_cf cfnode -> + IntSet.iter (fun pred -> + match graph.nodes.(pred) with + | Some (content, preds', succs') -> + graph.nodes.(pred) <- Some (content, preds', IntSet.remove n (IntSet.union succs succs')) + | None -> assert false + ) preds; + IntSet.iter (fun succ -> + match graph.nodes.(succ) with + | Some (content, preds', succs') -> + graph.nodes.(succ) <- Some (content, IntSet.remove n (IntSet.union preds preds'), succs') + | None -> assert false + ) succs; + graph.nodes.(n) <- None + | _ -> () + done + let ssa instrs = let start, finish, cfg = control_flow_graph instrs in let idom = immediate_dominators cfg start in @@ -545,13 +595,21 @@ let ssa instrs = let df = dominance_frontiers cfg start idom children in place_phi_functions cfg df; rename_variables cfg start children; + place_pi_functions cfg start idom children; + (* remove_guard_nodes (function CF_guard _ -> true | CF_label _ -> true | _ -> false) cfg; *) cfg (* Debugging utilities for outputing Graphviz files. *) +let string_of_ssainstr = function + | Phi (id, args) -> + string_of_id id ^ " = φ(" ^ Util.string_of_list ", " string_of_id args ^ ")" + | Pi cvals -> + "π(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")" + let string_of_phis = function | [] -> "" - | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l" + | phis -> Util.string_of_list "\\l" string_of_ssainstr phis ^ "\\l" let string_of_node = function | (phis, CF_label label) -> string_of_phis phis ^ label diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli index 11df036c..75c130cf 100644 --- a/src/jib/jib_ssa.mli +++ b/src/jib/jib_ssa.mli @@ -80,6 +80,7 @@ val immediate_dominators : 'a array_graph -> int -> int array type ssa_elem = | Phi of Ast.id * Ast.id list + | Pi of Jib.cval list (** Convert a list of instructions into SSA form *) val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph diff --git a/src/type_check.ml b/src/type_check.ml index 12832ad5..31a9370f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1217,6 +1217,7 @@ end = struct { env with constraints = List.map (constraint_subst v (arg_kopt (mk_kopt s_k s_v))) env.constraints; typ_vars = KBindings.add v (l, k) (KBindings.add s_v (s_l, s_k) env.typ_vars); + locals = Bindings.map (fun (mut, typ) -> mut, typ_subst v (arg_kopt (mk_kopt s_k s_v)) typ) env.locals; shadow_vars = KBindings.add v (n + 1) env.shadow_vars }, Some s_v end |