From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 12 Mar 2024 17:19:14 +0100 Subject: WIP: does not compile yet because we need to propagate the meta variable. --- compiler/SynthesizeSymbolic.ml | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index ad34c48e..787bfb4f 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -4,21 +4,22 @@ open Expressions open Values open LlbcAst open SymbolicAst +open Errors -let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace = - let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in +let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace = + let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in { bv; projection = p.projection } -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_mplace (meta : Meta.meta) (p : place option) (ctx : Contexts.eval_ctx) : mplace option = + Option.map (fun p -> mk_mplace meta p ctx) p -let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) : +let mk_opt_place_from_op (meta : Meta.meta) (op : operand) (ctx : Contexts.eval_ctx) : mplace option = - match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None + match op with Copy p | Move p -> Some (mk_mplace meta p ctx) | Constant _ -> None let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e) -let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) +let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (place : mplace option) (seel : symbolic_expansion option list) (el : expression list option) : expression option = match el with @@ -36,7 +37,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) (Some (SeLiteral (VBool false)), false_exp); ] -> ExpandBool (true_exp, false_exp) - | _ -> raise (Failure "Ill-formed boolean expansion")) + | _ -> craise meta "Ill-formed boolean expansion") | TLiteral (TInteger int_ty) -> (* Switch over an integer: split between the "regular" branches and the "otherwise" branch (which should be the last branch) *) @@ -46,9 +47,9 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) let get_scalar (see : symbolic_expansion option) : scalar_value = match see with | Some (SeLiteral (VScalar cv)) -> - assert (cv.int_ty = int_ty); + cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message"; cv - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let branches = List.map (fun (see, exp) -> (get_scalar see, exp)) branches @@ -56,7 +57,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) (* For the otherwise branch, the symbolic value should have been left * unchanged *) let otherwise_see, otherwise = otherwise in - assert (otherwise_see = None); + cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged"; (* Return *) ExpandInt (int_ty, branches, otherwise) | TAdt (_, _) -> @@ -65,7 +66,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) VariantId.id option * symbolic_value list = match see with | Some (SeAdt (vid, fields)) -> (vid, fields) - | _ -> raise (Failure "Ill-formed branching ADT expansion") + | _ -> craise meta "Ill-formed branching ADT expansion" in let exp = List.map @@ -79,18 +80,18 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option) (* Reference expansion: there should be one branch *) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) - | _ -> raise (Failure "Ill-formed borrow expansion")) + | _ -> craise meta "Ill-formed borrow expansion") | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> - raise (Failure "Ill-formed symbolic expansion") + craise meta "Ill-formed symbolic expansion" in Some (Expansion (place, sv, expansion)) -let synthesize_symbolic_expansion_no_branching (sv : symbolic_value) +let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) (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 + synthesize_symbolic_expansion meta sv place [ Some see ] el let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) (sg : fun_sig option) (regions_hierarchy : region_var_groups) @@ -188,7 +189,7 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) loop_expr; meta; }) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) : expression option = -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/SynthesizeSymbolic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 787bfb4f..bdd27d0f 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -47,7 +47,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac let get_scalar (see : symbolic_expansion option) : scalar_value = match see with | Some (SeLiteral (VScalar cv)) -> - cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message"; + sanity_check (cv.int_ty = int_ty) meta; cv | _ -> craise meta "Unreachable" in @@ -57,7 +57,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac (* For the otherwise branch, the symbolic value should have been left * unchanged *) let otherwise_see, otherwise = otherwise in - cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged"; + sanity_check (otherwise_see = None) meta; (* Return *) ExpandInt (int_ty, branches, otherwise) | TAdt (_, _) -> -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/SynthesizeSymbolic.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index bdd27d0f..f7437f7e 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -6,22 +6,26 @@ open LlbcAst open SymbolicAst open Errors -let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace = +let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace + = let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in { bv; projection = p.projection } -let mk_opt_mplace (meta : Meta.meta) (p : place option) (ctx : Contexts.eval_ctx) : mplace option = +let mk_opt_mplace (meta : Meta.meta) (p : place option) + (ctx : Contexts.eval_ctx) : mplace option = Option.map (fun p -> mk_mplace meta p ctx) p -let mk_opt_place_from_op (meta : Meta.meta) (op : operand) (ctx : Contexts.eval_ctx) : - mplace option = - match op with Copy p | Move p -> Some (mk_mplace meta p ctx) | Constant _ -> None +let mk_opt_place_from_op (meta : Meta.meta) (op : operand) + (ctx : Contexts.eval_ctx) : mplace option = + match op with + | Copy p | Move p -> Some (mk_mplace meta p ctx) + | Constant _ -> None let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e) -let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (place : mplace option) - (seel : symbolic_expansion option list) (el : expression list option) : - expression option = +let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) + (place : mplace option) (seel : symbolic_expansion option list) + (el : expression list option) : expression option = match el with | None -> None | Some el -> @@ -87,9 +91,9 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac in Some (Expansion (place, sv, expansion)) -let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) (sv : symbolic_value) - (place : mplace option) (see : symbolic_expansion) (e : expression option) : - expression option = +let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) + (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 meta sv place [ Some see ] el -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/SynthesizeSymbolic.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'compiler/SynthesizeSymbolic.ml') diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index f7437f7e..74b333f3 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -41,7 +41,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (Some (SeLiteral (VBool false)), false_exp); ] -> ExpandBool (true_exp, false_exp) - | _ -> craise meta "Ill-formed boolean expansion") + | _ -> craise __FILE__ __LINE__ meta "Ill-formed boolean expansion") | TLiteral (TInteger int_ty) -> (* Switch over an integer: split between the "regular" branches and the "otherwise" branch (which should be the last branch) *) @@ -51,9 +51,9 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) let get_scalar (see : symbolic_expansion option) : scalar_value = match see with | Some (SeLiteral (VScalar cv)) -> - sanity_check (cv.int_ty = int_ty) meta; + sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) meta; cv - | _ -> craise meta "Unreachable" + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in let branches = List.map (fun (see, exp) -> (get_scalar see, exp)) branches @@ -61,7 +61,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (* For the otherwise branch, the symbolic value should have been left * unchanged *) let otherwise_see, otherwise = otherwise in - sanity_check (otherwise_see = None) meta; + sanity_check __FILE__ __LINE__ (otherwise_see = None) meta; (* Return *) ExpandInt (int_ty, branches, otherwise) | TAdt (_, _) -> @@ -70,7 +70,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) VariantId.id option * symbolic_value list = match see with | Some (SeAdt (vid, fields)) -> (vid, fields) - | _ -> craise meta "Ill-formed branching ADT expansion" + | _ -> craise __FILE__ __LINE__ meta "Ill-formed branching ADT expansion" in let exp = List.map @@ -84,10 +84,10 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (* Reference expansion: there should be one branch *) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) - | _ -> craise meta "Ill-formed borrow expansion") + | _ -> craise __FILE__ __LINE__ meta "Ill-formed borrow expansion") | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> - craise meta "Ill-formed symbolic expansion" + craise __FILE__ __LINE__ meta "Ill-formed symbolic expansion" in Some (Expansion (place, sv, expansion)) @@ -193,7 +193,7 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) loop_expr; meta; }) - | _ -> craise meta "Unreachable" + | _ -> craise __FILE__ __LINE__ meta "Unreachable" let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) : expression option = -- cgit v1.2.3 From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 14:07:36 +0100 Subject: formatting and changed save_error condition for failing from b to not b --- 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 74b333f3..576b2809 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -70,7 +70,9 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) VariantId.id option * symbolic_value list = match see with | Some (SeAdt (vid, fields)) -> (vid, fields) - | _ -> craise __FILE__ __LINE__ meta "Ill-formed branching ADT expansion" + | _ -> + craise __FILE__ __LINE__ meta + "Ill-formed branching ADT expansion" in let exp = List.map -- cgit v1.2.3