diff options
| -rw-r--r-- | compiler/Interpreter.ml | 36 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 26 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 5 | ||||
| -rw-r--r-- | compiler/Print.ml | 3 |
4 files changed, 54 insertions, 16 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 81d6ff72..b2e55841 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -362,6 +362,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) ctx) else ctx in + log#ldebug + (lazy + ("evaluate_function_symbolic_synthesize_backward_from_return: (after \ + putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n" + ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx)); (* We now need to end the proper *input* abstractions - pay attention * to the fact that we end the *input* abstractions, not the *return* @@ -418,7 +423,28 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) } ]} *) - (None, false) + (* If we are borrow-checking: end the synth input abstraction to + check there is no borrow-checking issue. + Otherwise, do nothing. + + We need this check because of the following: + {[ + fn loop_reborrow_mut1<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 { + let mut x = 0; + while x > 0 { + x += 1; + } + if x > 0 { + a + } else { + b // Failure + } + } + ]} + (remark: this is slightly ad-hoc, and we won't need to do that + once we make the handling of loops more general). + *) + if !Config.borrow_check then (Some fun_abs_id, true) else (None, false) | Some abs -> (Some abs.abs_id, false) in log#ldebug @@ -619,11 +645,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let ctx_resl, cc = eval_function_body config (Option.get fdef.body).body ctx in - if synthesize then - (* Finish synthesizing *) - let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in - Some (cc el) - else None + let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in + (* Finish synthesizing *) + if synthesize then Some (cc el) else None with CFailure (span, msg) -> if synthesize then Some (Error (span, msg)) else None in diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 735f3743..0d770e80 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -665,8 +665,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) in List.iter end_at_return (fst (eval_loop_body fp)); - (* Check that the sets of abstractions we need to end per region group are pairwise - * disjoint *) + (* Check that the sets of abstractions we need to end per region group are + pairwise disjoint *) let aids_union = ref AbstractionId.Set.empty in let _ = RegionGroupId.Map.iter @@ -680,8 +680,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) !fp_ended_aids in - (* We also check that all the regions need to end - this is not necessary per - se, but if it doesn't happen it is bizarre and worth investigating... *) + (* If we generate a translation, we check that all the regions need to end + - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... + We need this check for now for technical reasons to make the translation work. + *) sanity_check __FILE__ __LINE__ (AbstractionId.Set.equal !aids_union !fp_aids) span; @@ -779,9 +781,11 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) no region group, and we set them as endable just above). If [remove_rg_id] is [false], we simply set the abstractions as non-endable - to freeze them (we will use the fixed point as starting point for the - symbolic execution of the loop body, and we have to make sure the input - abstractions are frozen). + **when generating a pure translation** to freeze them (we will use the + fixed point as starting point for the symbolic execution of the loop body, + and we have to make sure the input abstractions are frozen). + If we are simply borrow-checking the program, we can set the abstraction + as endable. *) let update_loop_abstractions (remove_rg_id : bool) = object @@ -796,7 +800,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) if remove_rg_id then Loop (loop_id, None, LoopSynthInput) else abs.kind in - { abs with can_end = remove_rg_id; kind } + (* If we borrow check we can always set the abstraction as + endable. If we generate a pure translation we have a few + more constraints. *) + let can_end = + if !Config.borrow_check then true else remove_rg_id + in + { abs with can_end; kind } | _ -> abs end in diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 3f7c023e..a1c0841a 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span) | Loop (loop_id', rg_id, kind) -> sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span; sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span; - let can_end = false in + (* If we borrow-check: we can set the abstractions as endable. + If we synthesize we have to constrain the region abstractions + a bit. *) + let can_end = !Config.borrow_check in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in super#visit_abs env abs diff --git a/compiler/Print.ml b/compiler/Print.ml index 7495d6bf..8bd709d0 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -309,13 +309,14 @@ module Values = struct let kind = if verbose then "[kind:" ^ abs_kind_to_string abs.kind ^ "]" else "" in + let can_end = if abs.can_end then "{endable}" else "{frozen}" in indent ^ "abs@" ^ AbstractionId.to_string abs.abs_id ^ kind ^ "{parents=" ^ AbstractionId.Set.to_string None abs.parents ^ "}" ^ "{regions=" ^ RegionId.Set.to_string None abs.regions - ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" + ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) : string = |