From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/SynthesizeSymbolic.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 857fea97..cac56487 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) assert (otherwise_see = None); (* Return *) ExpandInt (int_ty, branches, otherwise) - | T.Adt (_, _, _, _) -> + | T.Adt (_, _) -> (* Branching: it is necessarily an enumeration expansion *) let get_variant (see : V.symbolic_expansion option) : T.VariantId.id option * V.symbolic_value list = @@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ | T.Literal Char | Never -> + | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) @@ -97,10 +97,10 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) synthesize_symbolic_expansion sv place [ Some see ] el let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) (args : V.typed_value list) - (args_places : mplace option list) (dest : V.symbolic_value) - (dest_place : mplace option) (e : expression option) : expression option = + (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (args : V.typed_value list) (args_places : mplace option list) + (dest : V.symbolic_value) (dest_place : mplace option) + (e : expression option) : expression option = Option.map (fun e -> let call = @@ -108,8 +108,7 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) call_id; ctx; abstractions; - type_params; - const_generic_params; + generics; args; dest; args_places; @@ -125,26 +124,27 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) let synthesize_regular_function_call (fun_id : A.fun_id) (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) (args : V.typed_value list) - (args_places : mplace option list) (dest : V.symbolic_value) - (dest_place : mplace option) (e : expression option) : expression option = + (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (args : V.typed_value list) (args_places : mplace option list) + (dest : V.symbolic_value) (dest_place : mplace option) + (e : expression option) : expression option = synthesize_function_call (Fun (fun_id, call_id)) - ctx abstractions type_params const_generic_params args args_places dest - dest_place e + ctx abstractions generics args args_places dest dest_place e let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop) (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - synthesize_function_call (Unop unop) ctx [] [] [] [ arg ] [ arg_place ] dest - dest_place e + let generics = TypesUtils.mk_empty_generic_args in + synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ] + dest dest_place e let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop) (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value) (arg1_place : mplace option) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - synthesize_function_call (Binop binop) ctx [] [] [] [ arg0; arg1 ] + let generics = TypesUtils.mk_empty_generic_args in + synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs) -- cgit v1.2.3 From 5921be8e2e8955db5101354d8bf29ae6a3693f48 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 11 Sep 2023 06:35:07 +0200 Subject: Make progress on correctly handling trait method calls in the symbolic execution --- compiler/SynthesizeSymbolic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index cac56487..aeb6899f 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -122,7 +122,7 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (e : expression option) : expression option = Option.map (fun e -> EvalGlobal (gid, dest, e)) e -let synthesize_regular_function_call (fun_id : A.fun_id) +let synthesize_regular_function_call (fun_id : A.fun_id_or_trait_method_ref) (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx) (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) (args : V.typed_value list) (args_places : mplace option list) -- cgit v1.2.3 From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 20 Oct 2023 15:05:00 +0200 Subject: Start updating to handle function pointers --- compiler/SynthesizeSymbolic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index aeb6899f..9084f2b3 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ -> + | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ | T.Arrow _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) -- cgit v1.2.3 From ece74df70f12790bab7ecfe0c590c2c637e89801 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 11:40:31 +0200 Subject: Update following the addition of raw pointers --- compiler/SynthesizeSymbolic.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 9084f2b3..9dd65c84 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -85,7 +85,9 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ | T.Arrow _ -> + | T.TypeVar _ + | T.Literal Char + | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) -- cgit v1.2.3 From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/SynthesizeSymbolic.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 9dd65c84..edd67749 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -32,16 +32,16 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) (* Match on the symbolic value type to know which can of expansion happened *) let expansion = match sv.V.sv_ty with - | T.Literal PV.Bool -> ( + | T.TLiteral PV.TBool -> ( (* Boolean expansion: there should be two branches *) match ls with | [ - (Some (V.SeLiteral (PV.Bool true)), true_exp); - (Some (V.SeLiteral (PV.Bool false)), false_exp); + (Some (V.SeLiteral (PV.VBool true)), true_exp); + (Some (V.SeLiteral (PV.VBool false)), false_exp); ] -> ExpandBool (true_exp, false_exp) | _ -> raise (Failure "Ill-formed boolean expansion")) - | T.Literal (PV.Integer int_ty) -> + | T.TLiteral (PV.TInteger 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 @@ -50,7 +50,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) let get_scalar (see : V.symbolic_expansion option) : V.scalar_value = match see with - | Some (V.SeLiteral (PV.Scalar cv)) -> + | Some (V.SeLiteral (PV.VScalar cv)) -> assert (cv.PV.int_ty = int_ty); cv | _ -> raise (Failure "Unreachable") @@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) assert (otherwise_see = None); (* Return *) ExpandInt (int_ty, branches, otherwise) - | T.Adt (_, _) -> + | T.TAdt (_, _) -> (* Branching: it is necessarily an enumeration expansion *) let get_variant (see : V.symbolic_expansion option) : T.VariantId.id option * V.symbolic_value list = @@ -86,7 +86,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) | T.TypeVar _ - | T.Literal Char + | T.TLiteral TChar | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ -> raise (Failure "Ill-formed symbolic expansion") in @@ -99,7 +99,7 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) synthesize_symbolic_expansion sv place [ Some see ] el let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (abstractions : V.AbstractionId.id list) (generics : T.generic_args) (args : V.typed_value list) (args_places : mplace option list) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = @@ -126,7 +126,7 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) let synthesize_regular_function_call (fun_id : A.fun_id_or_trait_method_ref) (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (abstractions : V.AbstractionId.id list) (generics : T.generic_args) (args : V.typed_value list) (args_places : mplace option list) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = @@ -171,7 +171,7 @@ let synthesize_loop (loop_id : V.LoopId.id) (input_svalues : V.symbolic_value list) (fresh_svalues : V.SymbolicValueId.Set.t) (rg_to_given_back_tys : - (T.RegionId.Set.t * T.rty list) T.RegionGroupId.Map.t) + (T.RegionId.Set.t * T.ty list) T.RegionGroupId.Map.t) (end_expr : expression option) (loop_expr : expression option) : expression option = match (end_expr, loop_expr) with -- cgit v1.2.3 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/SynthesizeSymbolic.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index edd67749..ddb9d681 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -80,14 +80,14 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) ls in ExpandAdt exp - | T.Ref (_, _, _) -> ( + | T.TRef (_, _, _) -> ( (* Reference expansion: there should be one branch *) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ + | T.TVar _ | T.TLiteral TChar - | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ -> + | TNever | T.TTraitType _ | T.TArrow _ | T.TRawPtr _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/SynthesizeSymbolic.ml | 122 +++++++++++++++++++---------------------- 1 file changed, 57 insertions(+), 65 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index ddb9d681..38efc53a 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -1,57 +1,52 @@ -module C = Collections -module T = Types -module PV = PrimitiveValues -module V = Values -module E = Expressions -module A = LlbcAst +open Types +open TypesUtils +open PrimitiveValues +open Expressions +open Values open SymbolicAst -let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace = +let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace = let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in { bv; projection = p.projection } -let mk_opt_mplace (p : E.place option) (ctx : Contexts.eval_ctx) : mplace option - = +let mk_opt_mplace (p : place option) (ctx : Contexts.eval_ctx) : mplace option = Option.map (fun p -> mk_mplace p ctx) p -let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) : +let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) : mplace option = - match op with - | E.Copy p | E.Move p -> Some (mk_mplace p ctx) - | E.Constant _ -> None + match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None let mk_meta (m : meta) (e : expression) : expression = Meta (m, e) -let synthesize_symbolic_expansion (sv : V.symbolic_value) - (place : mplace option) (seel : V.symbolic_expansion option list) - (el : expression list option) : expression option = +let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) + (seel : symbolic_expansion option list) (el : expression list option) : + expression option = match el with | None -> None | Some el -> let ls = List.combine seel el in (* Match on the symbolic value type to know which can of expansion happened *) let expansion = - match sv.V.sv_ty with - | T.TLiteral PV.TBool -> ( + match sv.sv_ty with + | TLiteral TBool -> ( (* Boolean expansion: there should be two branches *) match ls with | [ - (Some (V.SeLiteral (PV.VBool true)), true_exp); - (Some (V.SeLiteral (PV.VBool false)), false_exp); + (Some (SeLiteral (VBool true)), true_exp); + (Some (SeLiteral (VBool false)), false_exp); ] -> ExpandBool (true_exp, false_exp) | _ -> raise (Failure "Ill-formed boolean expansion")) - | T.TLiteral (PV.TInteger int_ty) -> + | TLiteral (TInteger 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 + let branches, otherwise = Collections.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 - = + let get_scalar (see : symbolic_expansion option) : scalar_value = match see with - | Some (V.SeLiteral (PV.VScalar cv)) -> - assert (cv.PV.int_ty = int_ty); + | Some (SeLiteral (VScalar cv)) -> + assert (cv.int_ty = int_ty); cv | _ -> raise (Failure "Unreachable") in @@ -64,12 +59,12 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) assert (otherwise_see = None); (* Return *) ExpandInt (int_ty, branches, otherwise) - | T.TAdt (_, _) -> + | TAdt (_, _) -> (* Branching: it is necessarily an enumeration expansion *) - let get_variant (see : V.symbolic_expansion option) : - T.VariantId.id option * V.symbolic_value list = + let get_variant (see : symbolic_expansion option) : + VariantId.id option * symbolic_value list = match see with - | Some (V.SeAdt (vid, fields)) -> (vid, fields) + | Some (SeAdt (vid, fields)) -> (vid, fields) | _ -> raise (Failure "Ill-formed branching ADT expansion") in let exp = @@ -80,29 +75,28 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) ls in ExpandAdt exp - | T.TRef (_, _, _) -> ( + | TRef (_, _, _) -> ( (* Reference expansion: there should be one branch *) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TVar _ - | T.TLiteral TChar - | TNever | T.TTraitType _ | T.TArrow _ | T.TRawPtr _ -> + | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ + -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) -let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) - (place : mplace option) (see : V.symbolic_expansion) (e : expression option) - : expression option = +let synthesize_symbolic_expansion_no_branching (sv : symbolic_value) + (place : mplace option) (see : symbolic_expansion) (e : expression option) : + expression option = let el = Option.map (fun e -> [ e ]) e in synthesize_symbolic_expansion sv place [ Some see ] el let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (generics : T.generic_args) - (args : V.typed_value list) (args_places : mplace option list) - (dest : V.symbolic_value) (dest_place : mplace option) - (e : expression option) : expression option = + (abstractions : AbstractionId.id list) (generics : generic_args) + (args : typed_value list) (args_places : mplace option list) + (dest : symbolic_value) (dest_place : mplace option) (e : expression option) + : expression option = Option.map (fun e -> let call = @@ -120,58 +114,56 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) FunCall (call, e)) e -let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) +let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value) (e : expression option) : expression option = Option.map (fun e -> EvalGlobal (gid, dest, e)) e -let synthesize_regular_function_call (fun_id : A.fun_id_or_trait_method_ref) - (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (generics : T.generic_args) - (args : V.typed_value list) (args_places : mplace option list) - (dest : V.symbolic_value) (dest_place : mplace option) - (e : expression option) : expression option = +let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref) + (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) + (abstractions : AbstractionId.id list) (generics : generic_args) + (args : typed_value list) (args_places : mplace option list) + (dest : symbolic_value) (dest_place : mplace option) (e : expression option) + : expression option = synthesize_function_call (Fun (fun_id, call_id)) ctx abstractions generics args args_places dest dest_place e -let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop) - (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value) +let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop) + (arg : typed_value) (arg_place : mplace option) (dest : symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - let generics = TypesUtils.mk_empty_generic_args in + let generics = empty_generic_args in synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ] dest dest_place e -let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop) - (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value) - (arg1_place : mplace option) (dest : V.symbolic_value) +let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : binop) + (arg0 : typed_value) (arg0_place : mplace option) (arg1 : typed_value) + (arg1_place : mplace option) (dest : symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - let generics = TypesUtils.mk_empty_generic_args in + let generics = empty_generic_args in synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e -let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs) +let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : abs) (e : expression option) : expression option = Option.map (fun e -> EndAbstraction (ctx, abs, e)) e let synthesize_assignment (ctx : Contexts.eval_ctx) (lplace : mplace) - (rvalue : V.typed_value) (rplace : mplace option) (e : expression option) : + (rvalue : typed_value) (rplace : mplace option) (e : expression option) : expression option = Option.map (fun e -> Meta (Assignment (ctx, lplace, rvalue, rplace), e)) e -let synthesize_assertion (ctx : Contexts.eval_ctx) (v : V.typed_value) +let synthesize_assertion (ctx : Contexts.eval_ctx) (v : typed_value) (e : expression option) = Option.map (fun e -> Assertion (ctx, v, e)) e let synthesize_forward_end (ctx : Contexts.eval_ctx) - (loop_input_values : V.typed_value V.SymbolicValueId.Map.t option) - (e : expression) (el : expression T.RegionGroupId.Map.t) = + (loop_input_values : typed_value SymbolicValueId.Map.t option) + (e : expression) (el : expression RegionGroupId.Map.t) = Some (ForwardEnd (ctx, loop_input_values, e, el)) -let synthesize_loop (loop_id : V.LoopId.id) - (input_svalues : V.symbolic_value list) - (fresh_svalues : V.SymbolicValueId.Set.t) - (rg_to_given_back_tys : - (T.RegionId.Set.t * T.ty list) T.RegionGroupId.Map.t) +let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) + (fresh_svalues : SymbolicValueId.Set.t) + (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t) (end_expr : expression option) (loop_expr : expression option) : expression option = match (end_expr, loop_expr) with -- cgit v1.2.3 From f852e1a1334b7506c0baf366b9e75cd01b9c843e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 12:15:37 +0100 Subject: Rename PrimitiveValues to Values --- compiler/SynthesizeSymbolic.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 38efc53a..9e14a4d6 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -1,6 +1,5 @@ open Types open TypesUtils -open PrimitiveValues open Expressions open Values open SymbolicAst -- cgit v1.2.3 From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:43:12 +0100 Subject: Add span information to the generated code --- compiler/SynthesizeSymbolic.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 9e14a4d6..efcf001a 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -15,7 +15,7 @@ let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) : mplace option = match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None -let mk_meta (m : meta) (e : expression) : expression = Meta (m, e) +let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e) let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) (seel : symbolic_expansion option list) (el : expression list option) : @@ -163,8 +163,8 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx) let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) (fresh_svalues : SymbolicValueId.Set.t) (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t) - (end_expr : expression option) (loop_expr : expression option) : - expression option = + (end_expr : expression option) (loop_expr : expression option) + (meta : Meta.meta) : expression option = match (end_expr, loop_expr) with | None, None -> None | Some end_expr, Some loop_expr -> @@ -177,5 +177,6 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) rg_to_given_back_tys; end_expr; loop_expr; + meta; }) | _ -> raise (Failure "Unreachable") -- cgit v1.2.3