summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-27 09:11:42 +0100
committerSon Ho2022-01-27 09:11:42 +0100
commitf1dc4c9636f7ee237880e938bc8089697c6013e3 (patch)
treeed7c8d1ab6e5e5c06e3f3992d54dd2849959aa98 /src
parentdfd41681049ad7f7be503f150fb9c5e62f3b9ef9 (diff)
Implement Translate.translate_function
Diffstat (limited to 'src')
-rw-r--r--src/Assumed.ml2
-rw-r--r--src/Identifiers.ml1
-rw-r--r--src/InterpreterStatements.ml3
-rw-r--r--src/SymbolicToPure.ml42
-rw-r--r--src/Translate.ml158
-rw-r--r--src/main.ml1
6 files changed, 178 insertions, 29 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index c40387ea..fd11f30b 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -61,7 +61,7 @@ let box_deref_mut_sig = box_deref_sig true
Rk.: following what is written above, we don't include `Box::free`.
*)
-let assumed_functions : (A.assumed_fun_id * A.fun_sig) list =
+let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list =
[
(BoxNew, box_new_sig);
(BoxDeref, box_deref_shared_sig);
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 3a900643..757c9df5 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -44,6 +44,7 @@ module type Id = sig
val of_int : int -> id
val nth : 'a list -> id -> 'a
+ (* TODO: change the signature (invert the index and the list *)
val nth_opt : 'a list -> id -> 'a option
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c7e67f0a..b0d4e5e0 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -561,6 +561,9 @@ let eval_non_local_function_call_concrete (config : C.config)
evaluating in symbolic mode of course.
Note: there are no region parameters, because they should be erased.
+
+ **Rk.:** this function is **stateful** and generates fresh abstraction ids
+ for the region groups.
*)
let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
A.inst_fun_sig =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index be8730a3..41df82f6 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -224,7 +224,7 @@ type fs_ctx = {
}
(** Function synthesis context
- TODO: merge with bs_ctx?
+ TODO: remove
*)
let fs_ctx_to_bs_ctx (fs_ctx : fs_ctx) : bs_ctx =
@@ -273,6 +273,12 @@ let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def
let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def =
FunDefId.Map.find id ctx.fun_context.cfim_fun_defs
+(* TODO: move *)
+let bs_ctx_lookup_local_function_sig (def_id : FunDefId.id)
+ (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
+ let id = (A.Local def_id, back_id) in
+ RegularFunIdMap.find id ctx.fun_context.fun_sigs
+
let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
(ctx : bs_ctx) : bs_ctx =
let calls = ctx.calls in
@@ -558,6 +564,19 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx)
: bs_ctx * var list =
List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl
+(** This generates a fresh variable **which is not to be linked to any symbolic value** *)
+let fresh_var (ty : ty) (ctx : bs_ctx) : bs_ctx * var =
+ (* Generate the fresh variable *)
+ let id, var_counter = VarId.fresh ctx.var_counter in
+ let var = { id; ty } in
+ (* Update the context *)
+ let ctx = { ctx with var_counter } in
+ (* Return *)
+ (ctx, var)
+
+let fresh_vars (tys : ty list) (ctx : bs_ctx) : bs_ctx * var list =
+ List.fold_left_map (fun ctx ty -> fresh_var ty ctx) ctx tys
+
let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
@@ -1175,21 +1194,14 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
let otherwise = translate_expression otherwise ctx in
Switch (scrutinee, SwitchInt (int_ty, branches, otherwise))
-(* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : FunDefId.id)
- (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
- let id = (A.Local def_id, back_id) in
- RegularFunIdMap.find id ctx.fun_context.fun_sigs
-
-let translate_fun_def (fs_ctx : fs_ctx) (body : S.expression) : fun_def =
- let def = fs_ctx.fun_def in
- let bid = fs_ctx.bid in
- let bs_ctx = fs_ctx_to_bs_ctx fs_ctx in
+let translate_fun_def (def : A.fun_def) (ctx : bs_ctx) (body : S.expression) :
+ fun_def =
+ let bid = ctx.bid in
(* Translate the function *)
let def_id = def.A.def_id in
let basename = def.name in
- let signature = bs_ctx_lookup_local_function_sig def_id bid bs_ctx in
- let body = translate_expression body bs_ctx in
+ let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in
+ let body = translate_expression body ctx in
(* Compute the list of (properly ordered) input variables *)
let backward_inputs : var list =
match bid with
@@ -1201,10 +1213,10 @@ let translate_fun_def (fs_ctx : fs_ctx) (body : S.expression) : fun_def =
let backward_ids = List.append parents_ids [ back_id ] in
List.concat
(List.map
- (fun id -> T.RegionGroupId.Map.find id bs_ctx.backward_inputs)
+ (fun id -> T.RegionGroupId.Map.find id ctx.backward_inputs)
backward_ids)
in
- let inputs = List.append bs_ctx.forward_inputs backward_inputs in
+ let inputs = List.append ctx.forward_inputs backward_inputs in
(* Sanity check *)
assert (
List.for_all
diff --git a/src/Translate.ml b/src/Translate.ml
index 69e09334..b3dcf522 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,18 +1,20 @@
+open Errors
+open Cps
+open InterpreterUtils
+open InterpreterStatements
+open Interpreter
module L = Logging
module T = Types
module A = CfimAst
module M = Modules
module SA = SymbolicAst
-open Errors
-open Cps
-open InterpreterUtils
-open InterpreterStatements
(** The local logger *)
let log = L.translate_log
(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
- for the forward function and the backward functions. *)
+ for the forward function and the backward functions.
+ *)
let translate_function_to_symbolics (config : C.partial_config)
(m : M.cfim_module) (fid : A.FunDefId.id) :
SA.expression * SA.expression list =
@@ -25,23 +27,153 @@ let translate_function_to_symbolics (config : C.partial_config)
("translate_function_to_symbolics: " ^ Print.name_to_string fdef.A.name));
(* Evaluate *)
+ let synthesize = true in
let evaluate = evaluate_function_symbolic config synthesize m fid in
(* Execute the forward function *)
- let forward = evaluate None in
+ let forward = Option.get (evaluate None) in
(* Execute the backward functions *)
let backwards =
T.RegionGroupId.mapi
- (fun gid _ -> evaluate (Some gid))
+ (fun gid _ -> Option.get (evaluate (Some gid)))
fdef.signature.regions_hierarchy
in
(* Return *)
(forward, backwards)
-(*let translate (config : C.partial_config) (m : M.cfim_module) : unit =
- (* Translate all the type definitions *)
- let type_defs = SymbolicToPure.translate_type_defs m.type_defs in
+(** Translate a function, by generating its forward and backward translations.
+
+ TODO: we shouldn't need to take m as parameter (we actually recompute the
+ type and function contexts in [translate_function_to_symbolics]...)
+ *)
+let translate_function (config : C.partial_config) (m : M.cfim_module)
+ (type_context : C.type_context) (fun_context : C.fun_context)
+ (fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t)
+ (fdef : A.fun_def) : Pure.fun_def * Pure.fun_def list =
+ let def_id = fdef.def_id in
+
+ (* Compute the symbolic ASTs *)
+ let symbolic_forward, symbolic_backwards =
+ translate_function_to_symbolics config m fdef.def_id
+ in
+
+ (* Convert the symbolic ASTs to pure ASTs: *)
+
+ (* Initialize the context *)
+ let sv_to_var = V.SymbolicValueId.Map.empty in
+ let var_counter = Pure.VarId.generator_zero in
+ let calls = V.FunCallId.Map.empty in
+ let abstractions = V.AbstractionId.Map.empty in
+ let type_context =
+ {
+ SymbolicToPure.types_infos = type_context.type_infos;
+ cfim_type_defs = type_context.type_defs;
+ }
+ in
+ let fun_context =
+ { SymbolicToPure.cfim_fun_defs = fun_context.fun_defs; fun_sigs }
+ in
+ let ctx =
+ {
+ SymbolicToPure.bid = None;
+ (* Dummy for now *)
+ sv_to_var;
+ var_counter;
+ type_context;
+ fun_context;
+ forward_inputs = [];
+ (* Empty for now *)
+ backward_inputs = T.RegionGroupId.Map.empty;
+ (* Empty for now *)
+ backward_outputs = T.RegionGroupId.Map.empty;
+ (* Empty for now *)
+ calls;
+ abstractions;
+ }
+ in
+
+ (* We need to initialize the input/output variables. First, the inputs
+ * for the forward function *)
+ let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in
+ let forward_sg = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in
+ let ctx, forward_inputs = SymbolicToPure.fresh_vars forward_sg.inputs ctx in
- (* Translate all the function signatures *)
- let fun_defs = SymbolicToPure.translate_fun_signatures types_infos
- raise Unimplemented*)
+ let ctx = { ctx with forward_inputs } in
+
+ (* Translate the forward function *)
+ let pure_forward =
+ SymbolicToPure.translate_fun_def fdef ctx symbolic_forward
+ in
+
+ (* Translate the backward functions *)
+ let translate_backward (rg : T.region_var_group) : Pure.fun_def =
+ (* For the backward inputs/outputs initialization: we use the fact that
+ * there are no nested borrows for now, and so that the region groups
+ * can't have parents *)
+ assert (rg.parents = []);
+ (* TODO: the computation of the backward inputs is a bit awckward... *)
+ let back_id = rg.id in
+ let backward_sg =
+ RegularFunIdMap.find (A.Local def_id, Some back_id) fun_sigs
+ in
+ let _, backward_inputs =
+ Collections.List.split_at backward_sg.inputs (List.length forward_inputs)
+ in
+ let ctx, backward_inputs = SymbolicToPure.fresh_vars backward_inputs ctx in
+ let backward_outputs = backward_sg.outputs in
+ let ctx, backward_outputs =
+ SymbolicToPure.fresh_vars backward_outputs ctx
+ in
+ let backward_inputs =
+ T.RegionGroupId.Map.singleton back_id backward_inputs
+ in
+ let backward_outputs =
+ T.RegionGroupId.Map.singleton back_id backward_outputs
+ in
+
+ (* Put everything in the context *)
+ let ctx =
+ { ctx with bid = Some back_id; backward_inputs; backward_outputs }
+ in
+
+ (* Translate *)
+ let symbolic = T.RegionGroupId.nth symbolic_backwards back_id in
+ SymbolicToPure.translate_fun_def fdef ctx symbolic
+ in
+ let pure_backwards =
+ List.map translate_backward fdef.signature.regions_hierarchy
+ in
+
+ (* Return *)
+ (pure_forward, pure_backwards)
+
+let translate_module (config : C.partial_config) (m : M.cfim_module) : unit =
+ (* Compute the type and function contexts *)
+ let type_context, fun_context = compute_type_fun_contexts m in
+
+ (* Translate all the type definitions *)
+ let type_defs = SymbolicToPure.translate_type_defs m.types in
+
+ (* Translate all the function *signatures* *)
+ let assumed_sigs =
+ List.map (fun (id, sg) -> (A.Assumed id, sg)) Assumed.assumed_sigs
+ in
+ let local_sigs =
+ List.map
+ (fun (fdef : A.fun_def) -> (A.Local fdef.def_id, fdef.signature))
+ m.functions
+ in
+ let sigs = List.append assumed_sigs local_sigs in
+ let fun_sigs =
+ SymbolicToPure.translate_fun_signatures type_context.type_infos sigs
+ in
+
+ (* Translate all the functions *)
+ let fun_defs =
+ List.map
+ (fun (fdef : A.fun_def) ->
+ ( fdef.def_id,
+ translate_function config m type_context fun_context fun_sigs ))
+ m.functions
+ in
+ raise Unimplemented
diff --git a/src/main.ml b/src/main.ml
index ea4ab23f..db57b5a7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -9,6 +9,7 @@ module TA = TypesAnalysis
module P = Pure
open PrintSymbolicAst
open SymbolicToPure
+open Translate
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.