diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Collections.ml | 14 | ||||
| -rw-r--r-- | src/Contexts.ml | 6 | ||||
| -rw-r--r-- | src/Cps.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 68 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 13 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 20 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 47 | ||||
| -rw-r--r-- | src/Synthesis.ml | 4 | ||||
| -rw-r--r-- | src/SynthesizeSymbolic.ml | 89 | ||||
| -rw-r--r-- | src/Values.ml | 28 |
10 files changed, 240 insertions, 52 deletions
diff --git a/src/Collections.ml b/src/Collections.ml index b73bc3b6..54d0acac 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -9,6 +9,8 @@ module List = struct `split_at ls i` splits `ls` into two lists where the first list has length `i`. + + Raise `Failure` if the list is too short. *) let rec split_at (ls : 'a list) (i : int) = if i < 0 then raise (Invalid_argument "split_at take positive integers") @@ -21,6 +23,18 @@ module List = struct | x :: ls' -> let ls1, ls2 = split_at ls' (i - 1) in (x :: ls1, ls2) + + (** Pop the last element of a list + + Raise `Failure` if the list is empty. + *) + let rec pop_last (ls : 'a list) : 'a list * 'a = + match ls with + | [] -> raise (Failure "The list is empty") + | [ x ] -> ([], x) + | x :: ls -> + let ls, last = pop_last ls in + (x :: ls, last) end module type OrderedType = sig diff --git a/src/Contexts.ml b/src/Contexts.ml index 39c6ab91..6f0c02c4 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -68,6 +68,9 @@ let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator () let abstraction_id_counter, fresh_abstraction_id = AbstractionId.fresh_stateful_generator () +let fun_call_id_counter, fresh_fun_call_id = + FunCallId.fresh_stateful_generator () + (** We shouldn't need to reset the global counters, but it might be good to do it from time to time, for instance every time we start evaluating/ synthesizing a function. @@ -83,7 +86,8 @@ let reset_global_counters () = symbolic_value_id_counter := SymbolicValueId.generator_zero; borrow_id_counter := BorrowId.generator_zero; region_id_counter := RegionId.generator_zero; - abstraction_id_counter := AbstractionId.generator_zero + abstraction_id_counter := AbstractionId.generator_zero; + fun_call_id_counter := FunCallId.generator_zero type binder = { index : VarId.id; (** Unique variable identifier *) @@ -4,6 +4,7 @@ module T = Types module V = Values module C = Contexts +module SA = SymbolicAst (** TODO: change the name *) type eval_error = EPanic @@ -19,7 +20,7 @@ type statement_eval_res = (** Synthesized expresssion - dummy for now *) type sexpr = SOne | SList of sexpr list -type eval_result = sexpr option +type eval_result = SA.expression option type m_fun = C.eval_ctx -> eval_result (** Continuation function *) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index b2d952b1..69e12545 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -11,7 +11,7 @@ module Subst = Substitute module L = Logging open TypesUtils module Inv = Invariants -module S = Synthesis +module S = SynthesizeSymbolic open Cps open ValuesUtils open InterpreterUtils @@ -52,7 +52,7 @@ type proj_kind = LoanProj | BorrowProj *) let apply_symbolic_expansion_to_target_avalues (config : C.config) (allow_reborrows : bool) (proj_kind : proj_kind) - (original_sv : V.symbolic_value) (expansion : symbolic_expansion) + (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = (* Symbolic values contained in the expansion might contain already ended regions *) let check_symbolic_no_ended = false in @@ -150,7 +150,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) *) let apply_symbolic_expansion_to_avalues (config : C.config) (allow_reborrows : bool) (original_sv : V.symbolic_value) - (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = + (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = let apply_expansion proj_kind ctx = apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind original_sv expansion ctx @@ -199,7 +199,7 @@ let replace_symbolic_values (at_most_once : bool) This function does update the synthesis. *) let apply_symbolic_expansion_non_borrow (config : C.config) - (original_sv : V.symbolic_value) (expansion : symbolic_expansion) + (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = (* Apply the expansion to non-abstraction values *) let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in @@ -221,7 +221,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config) let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (kind : V.sv_kind) (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list) (types : T.rty list) - (ctx : C.eval_ctx) : symbolic_expansion list = + (ctx : C.eval_ctx) : V.symbolic_expansion list = (* Lookup the definition and check if it is an enumeration with several * variants *) let def = C.ctx_lookup_type_def ctx def_id in @@ -236,31 +236,31 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (* Initialize the expanded value for a given variant *) let initialize ((variant_id, field_types) : T.VariantId.id option * T.rty list) : - symbolic_expansion = + V.symbolic_expansion = let field_values = List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types in - let see = SeAdt (variant_id, field_values) in + let see = V.SeAdt (variant_id, field_values) in see in (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types let compute_expanded_symbolic_tuple_value (kind : V.sv_kind) - (field_types : T.rty list) : symbolic_expansion = + (field_types : T.rty list) : V.symbolic_expansion = (* Generate the field values *) let field_values = List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types in let variant_id = None in - let see = SeAdt (variant_id, field_values) in + let see = V.SeAdt (variant_id, field_values) in see let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : - symbolic_expansion = + V.symbolic_expansion = (* Introduce a fresh symbolic value *) let boxed_value = mk_fresh_symbolic_value kind boxed_ty in - let see = SeAdt (None, [ boxed_value ]) in + let see = V.SeAdt (None, [ boxed_value ]) in see let expand_symbolic_value_shared_borrow (config : C.config) @@ -363,16 +363,16 @@ let expand_symbolic_value_shared_borrow (config : C.config) let bids = !borrows in assert (not (V.BorrowId.Set.is_empty bids)); let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in - let see = SeSharedRef (bids, shared_sv) in + let see = V.SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see ctx in + (* Call the continuation *) + let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Continue *) - cf ctx + S.synthesize_symbolic_expansion_no_branching original_sv see expr (** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : C.config) @@ -388,7 +388,7 @@ let expand_symbolic_value_borrow (config : C.config) * borrow id *) let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in let bid = C.fresh_borrow_id () in - let see = SeMutRef (bid, sv) in + let see = V.SeMutRef (bid, sv) in (* Expand the symbolic values - we simply perform a substitution (and * check that we perform exactly one substitution) *) let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in @@ -402,10 +402,10 @@ let expand_symbolic_value_borrow (config : C.config) apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see ctx in + (* Apply the continuation *) + let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Continue *) - cf ctx + S.synthesize_symbolic_expansion_no_branching original_sv see expr | T.Shared -> expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx @@ -419,7 +419,7 @@ let expand_symbolic_value_borrow (config : C.config) *) let apply_branching_symbolic_expansions_non_borrow (config : C.config) (sv : V.symbolic_value) - (see_cf_l : (symbolic_expansion option * m_fun) list) : m_fun = + (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun = fun ctx -> assert (see_cf_l <> []); (* Apply the symbolic expansion in in the context and call the continuation *) @@ -447,7 +447,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) | _ -> failwith "Unreachable" in (* Synthesize and return *) - S.synthesize_symbolic_expansion sv subterms + let seel = List.map fst see_cf_l in + S.synthesize_symbolic_expansion sv seel subterms (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). @@ -492,10 +493,10 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx in + (* Call the continuation *) + let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Continue *) - cf ctx + S.synthesize_symbolic_expansion_no_branching original_sv see expr (* Boxes *) | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in @@ -503,10 +504,10 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx in + (* Call the continuation *) + let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Continue *) - cf ctx + S.synthesize_symbolic_expansion_no_branching original_sv see expr (* Borrows *) | T.Ref (region, ref_ty, rkind) -> expand_symbolic_value_borrow config original_sv region ref_ty rkind cf @@ -514,13 +515,12 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Booleans *) | T.Bool -> assert allow_branching; - (* Synthesis *) - S.synthesize_symbolic_expansion_if_branching original_sv; (* Expand the symbolic value to true or false and continue execution *) - let see_true = SeConcrete (V.Bool true) in - let see_false = SeConcrete (V.Bool false) in + let see_true = V.SeConcrete (V.Bool true) in + let see_false = V.SeConcrete (V.Bool false) in let seel = [ see_true; see_false ] in let seel = List.map (fun see -> (Some see, cf)) seel in + (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) apply_branching_symbolic_expansions_non_borrow config original_sv seel ctx | _ -> failwith ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty) @@ -569,8 +569,6 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) (int_type : T.integer_type) (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun = - (* Synthesis *) - S.synthesize_symbolic_expansion_switch_int_branching sv; (* Sanity check *) assert (sv.V.sv_ty = T.Integer int_type); (* For all the branches of the switch, we expand the symbolic value @@ -583,10 +581,10 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) * (optional expansion, statement to execute) *) let tgts = - List.map (fun (v, cf) -> (Some (SeConcrete (V.Scalar v)), cf)) tgts + List.map (fun (v, cf) -> (Some (V.SeConcrete (V.Scalar v)), cf)) tgts in let tgts = List.append tgts [ (None, otherwise) ] in - (* Then expand and evaluate *) + (* Then expand and evaluate - this generates the proper symbolic AST *) apply_branching_symbolic_expansions_non_borrow config sv tgts (** See [expand_symbolic_value] *) diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 982d9460..946bacea 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -8,13 +8,6 @@ open TypesUtils open InterpreterUtils open InterpreterBorrowsCore -(** A symbolic expansion *) -type symbolic_expansion = - | SeConcrete of V.constant_value - | SeAdt of (T.VariantId.id option * V.symbolic_value list) - | SeMutRef of V.BorrowId.id * V.symbolic_value - | SeSharedRef of V.BorrowId.Set.t * V.symbolic_value - (** Auxiliary function. Apply a proj_borrows on a shared borrow. @@ -255,7 +248,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (** Convert a symbolic expansion *which is not a borrow* to a value *) let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) - (see : symbolic_expansion) : V.typed_value = + (see : V.symbolic_expansion) : V.typed_value = let ty = Subst.erase_regions sv.V.sv_ty in let value = match see with @@ -277,7 +270,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) during a symbolic expansion. *) let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) - (see : symbolic_expansion) : V.typed_value = + (see : V.symbolic_expansion) : V.typed_value = match see with | SeMutRef (bid, bv) -> let ty = Subst.erase_regions sv.V.sv_ty in @@ -293,7 +286,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) TODO: detailed comments. See [apply_proj_borrows] *) let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) - (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = + (see : V.symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should * contain regions which we will project *) assert (ty_has_regions_in_set regions original_sv_ty); diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index d76def43..17fe700f 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -668,9 +668,14 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind) let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref = ref V.AbstractionId.Map.empty in + (* We generate *one* fresh call identifier for all the introduced abstractions + * (it links them together) *) + let call_id = C.fresh_fun_call_id () in (* Auxiliary function to create one abstraction *) - let create_abs (rg : A.abs_region_group) : V.abs = + let create_abs (back_id : V.BackwardFunctionId.id) (rg : A.abs_region_group) : + V.abs = let abs_id = rg.T.id in + let back_id = Some back_id in let parents = List.fold_left (fun s pid -> V.AbstractionId.Set.add pid s) @@ -695,10 +700,19 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind) V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions !abs_to_ancestors_regions; (* Create the abstraction *) - { V.abs_id; kind; parents; regions; ancestors_regions; avalues = [] } + { + V.abs_id; + call_id; + back_id; + kind; + parents; + regions; + ancestors_regions; + avalues = []; + } in (* Apply *) - List.map create_abs rgl + V.BackwardFunctionId.mapi create_abs rgl (** Evaluate a statement *) let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml new file mode 100644 index 00000000..6b66ada7 --- /dev/null +++ b/src/SymbolicAst.ml @@ -0,0 +1,47 @@ +(** The "symbolic" AST is the AST directly generated by the symbolic execution. + It is very rough and meant to be extremely straightforward to build during + the symbolic execution: we later apply transformations to generate the + pure AST that we export. *) + +open Identifiers +module T = Types +module V = Values +module E = Expressions +module A = CfimAst + +type fun_id = + | Fun of A.fun_id + (** A "regular" function (i.e., a function which is not a primitive operation) *) + | Unop of E.unop + | Binop of E.binop + +type call = { + call_id : V.FunCallId.id; + func : A.fun_id; + type_params : T.ety list; + args : V.typed_value list; + dest : V.symbolic_value; +} + +type expression = + | Return + | Panic + | FunCall of call * expression + | EndAbstraction of V.abs * expression + | Expansion of V.symbolic_value * expansion + +and expansion = + | ExpandNoBranch of V.symbolic_expansion * expression + (** A symbolic expansion which doesn't generate a branching. + Includes: expansion of borrows, structures, enumerations with one + variants... *) + | ExpandEnum of + (T.VariantId.id option * V.symbolic_value list * expression) list + (** A symbolic expansion of an ADT value which leads to branching (i.e., + a match over an enumeration with strictly more than one variant *) + | ExpandBool of expression * expression + (** A boolean expansion (i.e, an `if ... then ... else ...`) *) + | ExpandInt of + T.integer_type * (V.scalar_value * expression) list * expression + (** An integer expansion (i.e, a switch over an integer). The last + expression is for the "otherwise" branch. *) diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 8a0dce93..acecd517 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -42,13 +42,13 @@ let synthesize_symbolic_expansion (_sv : V.symbolic_value) (i.e., applied on a value which is not an enumeration with several variants). *) let synthesize_symbolic_expansion_no_branching (_sv : V.symbolic_value) - (_see : symbolic_expansion) : unit = + (_see : V.symbolic_expansion) : unit = () (** Synthesize code for a symbolic enum expansion (which leads to branching) *) let synthesize_symbolic_expansion_enum_branching (_sv : V.symbolic_value) - (_seel : symbolic_expansion list) : unit = + (_seel : V.symbolic_expansion list) : unit = () let synthesize_symbolic_expansion_if_branching (_sv : V.symbolic_value) : unit = diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml new file mode 100644 index 00000000..b9bad7c9 --- /dev/null +++ b/src/SynthesizeSymbolic.ml @@ -0,0 +1,89 @@ +open Errors +open Identifiers +module C = Collections +module T = Types +module V = Values +module E = Expressions +module A = CfimAst +open SymbolicAst + +let synthesize_symbolic_expansion (sv : V.symbolic_value) + (seel : V.symbolic_expansion option list) (exprl : expression list option) : + expression option = + match exprl with + | None -> None + | Some exprl -> + let ls = List.combine seel exprl in + (* Match on the symbolic value type to know which can of expansion happened *) + let expansion = + match sv.V.sv_ty with + | T.Bool -> ( + (* Boolean expansion: there should be two branches *) + match ls with + | [ + (Some (V.SeConcrete (V.Bool true)), true_exp); + (Some (V.SeConcrete (V.Bool false)), false_exp); + ] -> + ExpandBool (true_exp, false_exp) + | _ -> failwith "Ill-formed boolean expansion") + | T.Integer int_ty -> + (* Switch over an integer: split between the "regular" branches + and the "otherwise" branch (which should be the last branch) *) + let branches, otherwise = C.List.pop_last ls in + (* For all the regular branches, the symbolic value should have + * been expanded to a constant *) + let get_scalar (see : V.symbolic_expansion option) : V.scalar_value + = + match see with + | Some (V.SeConcrete (V.Scalar cv)) -> + assert (cv.V.int_ty = int_ty); + cv + | _ -> failwith "Unreachable" + in + let branches = + List.map (fun (see, exp) -> (get_scalar see, exp)) branches + in + (* For the otherwise branch, the symbolic value should have been left + * unchanged *) + let otherwise_see, otherwise = otherwise in + assert (otherwise_see = None); + (* Return *) + ExpandInt (int_ty, branches, otherwise) + | T.Adt (adt_id, regions, types) -> ( + (* An ADT expansion can lead to branching: check if this is the case *) + match ls with + | [] -> failwith "Ill-formed ADT expansion" + | [ (see, exp) ] -> + (* No branching *) + ExpandNoBranch (Option.get see, exp) + | ls -> + (* Branching: it is necessarily an enumeration expansion *) + let get_variant (see : V.symbolic_expansion option) : + T.VariantId.id option * V.symbolic_value list = + match see with + | Some (V.SeAdt (vid, fields)) -> (vid, fields) + | _ -> failwith "Ill-formed branching ADT expansion" + in + let exp = + List.map + (fun (see, exp) -> + let vid, fields = get_variant see in + (vid, fields, exp)) + ls + in + ExpandEnum exp) + | T.Ref (r, ty, rkind) -> ( + (* Reference expansion: there should be one branch *) + match ls with + | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) + | _ -> failwith "Ill-formed borrow expansion") + | T.TypeVar _ | Char | Never | Str | Array _ | Slice _ -> + failwith "Ill-formed symbolic expansion" + in + Some (Expansion (sv, expansion)) + +let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) + (see : V.symbolic_expansion) (expr : expression option) : expression option + = + let exprl = match expr with None -> None | Some expr -> Some [ expr ] in + synthesize_symbolic_expansion sv [ Some see ] exprl diff --git a/src/Values.ml b/src/Values.ml index 4946b811..1812cd18 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -13,6 +13,10 @@ module SymbolicValueId = IdGen () module AbstractionId = IdGen () +module FunCallId = IdGen () + +module BackwardFunctionId = IdGen () + (** A variable *) type big_int = Z.t @@ -712,6 +716,17 @@ type abs_kind = type abs = { abs_id : (AbstractionId.id[@opaque]); + call_id : (FunCallId.id[@opaque]); + (** The identifier of the function call which introduced this + abstraction. This is not used by the symbolic execution: + this is only used for pretty-printing and debugging, in the + symbolic AST, generated by the symbolic execution. + *) + back_id : (BackwardFunctionId.id option[@opaque]); + (** The id of the backward function to which this abstraction is linked. + This is not used by the symbolic execution: it is a utility for + the symbolic AST, generated by the symbolic execution. + *) kind : (abs_kind[@opaque]); parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *) regions : (RegionId.Set.t[@opaque]); (** Regions owned by this abstraction *) @@ -744,3 +759,16 @@ type abs = { In order to model the relations between the borrows, we use "abstraction values", which are a special kind of value. *) + +(** A symbolic expansion + + A symbolic expansion doesn't represent a value, but rather an operation + that we apply to values. + + TODO: this should rather be name "expanded_symbolic" + *) +type symbolic_expansion = + | SeConcrete of constant_value + | SeAdt of (VariantId.id option * symbolic_value list) + | SeMutRef of BorrowId.id * symbolic_value + | SeSharedRef of BorrowId.Set.t * symbolic_value |