Merge pull request #227 from AeneasVerif/son/clean-synthesis

Remove the use of `Option` from the functions synthesizing the symbolic AST

1 files changed, 88 insertions, 100 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 94158979..fb3701f3 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -277,7 +277,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
 let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     (fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id)
     (loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool)
-    (ctx : eval_ctx) : SA.expression option =
+    (ctx : eval_ctx) : SA.expression =
   log#ldebug
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return:"
@@ -477,8 +477,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   (* Generate the Return node *)
   let return_expr =
     match loop_id with
-    | None -> Some (SA.Return (ctx, None))
-    | Some loop_id -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
+    | None -> SA.Return (ctx, None)
+    | Some loop_id -> SA.ReturnWithLoop (loop_id, inside_loop)
   in
   (* Apply *)
   cc return_expr
@@ -486,12 +486,12 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
 (** Evaluate a function with the symbolic interpreter.
 
     We return:
-    - the list of symbolic values introduced for the input values (this is useful
-      for the synthesis)
+    - the list of symbolic values introduced for the input values (this is
+      useful for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
-    (fdef : fun_decl) : symbolic_value list * SA.expression option =
+let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
+    symbolic_value list * SA.expression =
   (* Debug *)
   let name_to_string () =
     Print.Types.name_to_string
@@ -518,101 +518,92 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
     match res with
     | Return | LoopReturn _ ->
-        if synthesize then
-          (* We have to "play different endings":
-           * - one execution for the forward function
-           * - one execution per backward function
-           * We then group everything together.
-           *)
-          (* There are two cases:
-           * - if this is a forward translation, we retrieve the returned value.
-           * - if this is a backward translation, we introduce "return"
-           *   abstractions to consume the return value, then end all the
-           *   abstractions up to the one in which we are interested.
-           *)
-          (* Forward translation: retrieve the returned value *)
-          let fwd_e =
-            (* Pop the frame and retrieve the returned value at the same time *)
-            let pop_return_value = true in
-            let ret_value, ctx, cc_pop =
-              pop_frame config fdef.item_meta.span pop_return_value ctx
-            in
-            (* Generate the Return node *)
-            cc_pop (Some (SA.Return (ctx, ret_value)))
-          in
-          let fwd_e = Option.get fwd_e in
-          (* Backward translation: introduce "return"
-             abstractions to consume the return value, then end all the
-             abstractions up to the one in which we are interested.
-          *)
-          let loop_id =
-            match res with
-            | Return -> None
-            | LoopReturn loop_id -> Some loop_id
-            | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
-          in
-          let is_regular_return = true in
-          let inside_loop = Option.is_some loop_id in
-          let finish_back_eval back_id =
-            Option.get
-              (evaluate_function_symbolic_synthesize_backward_from_return config
-                 fdef inst_sg back_id loop_id is_regular_return inside_loop ctx)
-          in
-          let back_el =
-            RegionGroupId.mapi
-              (fun gid _ -> (gid, finish_back_eval gid))
-              regions_hierarchy
+        (* We have to "play different endings":
+         * - one execution for the forward function
+         * - one execution per backward function
+         * We then group everything together.
+         *)
+        (* There are two cases:
+         * - if this is a forward translation, we retrieve the returned value.
+         * - if this is a backward translation, we introduce "return"
+         *   abstractions to consume the return value, then end all the
+         *   abstractions up to the one in which we are interested.
+         *)
+        (* Forward translation: retrieve the returned value *)
+        let fwd_e =
+          (* Pop the frame and retrieve the returned value at the same time *)
+          let pop_return_value = true in
+          let ret_value, ctx, cc_pop =
+            pop_frame config fdef.item_meta.span pop_return_value ctx
           in
-          let back_el = RegionGroupId.Map.of_list back_el in
-          (* Put everything together *)
-          synthesize_forward_end ctx0 None fwd_e back_el
-        else None
+          (* Generate the Return node *)
+          cc_pop (SA.Return (ctx, ret_value))
+        in
+        (* Backward translation: introduce "return"
+           abstractions to consume the return value, then end all the
+           abstractions up to the one in which we are interested.
+        *)
+        let loop_id =
+          match res with
+          | Return -> None
+          | LoopReturn loop_id -> Some loop_id
+          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+        in
+        let is_regular_return = true in
+        let inside_loop = Option.is_some loop_id in
+        let finish_back_eval back_id =
+          evaluate_function_symbolic_synthesize_backward_from_return config fdef
+            inst_sg back_id loop_id is_regular_return inside_loop ctx
+        in
+        let back_el =
+          RegionGroupId.mapi
+            (fun gid _ -> (gid, finish_back_eval gid))
+            regions_hierarchy
+        in
+        let back_el = RegionGroupId.Map.of_list back_el in
+        (* Put everything together *)
+        synthesize_forward_end ctx0 None fwd_e back_el
     | EndEnterLoop (loop_id, loop_input_values)
     | EndContinue (loop_id, loop_input_values) ->
         (* Similar to [Return]: we have to play different endings *)
-        if synthesize then
-          let inside_loop =
-            match res with
-            | EndEnterLoop _ -> false
-            | EndContinue _ -> true
-            | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
-          in
-          (* Forward translation *)
-          let fwd_e =
-            (* Pop the frame - there is no returned value to pop: in the
-               translation we will simply call the loop function *)
-            let pop_return_value = false in
-            let _ret_value, _ctx, cc_pop =
-              pop_frame config fdef.item_meta.span pop_return_value ctx
-            in
-            (* Generate the Return node *)
-            cc_pop (Some (SA.ReturnWithLoop (loop_id, inside_loop)))
-          in
-          let fwd_e = Option.get fwd_e in
-          (* Backward translation: introduce "return"
-             abstractions to consume the return value, then end all the
-             abstractions up to the one in which we are interested.
-          *)
-          let is_regular_return = false in
-          let finish_back_eval back_id =
-            Option.get
-              (evaluate_function_symbolic_synthesize_backward_from_return config
-                 fdef inst_sg back_id (Some loop_id) is_regular_return
-                 inside_loop ctx)
-          in
-          let back_el =
-            RegionGroupId.mapi
-              (fun gid _ -> (gid, finish_back_eval gid))
-              regions_hierarchy
+        let inside_loop =
+          match res with
+          | EndEnterLoop _ -> false
+          | EndContinue _ -> true
+          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+        in
+        (* Forward translation *)
+        let fwd_e =
+          (* Pop the frame - there is no returned value to pop: in the
+             translation we will simply call the loop function *)
+          let pop_return_value = false in
+          let _ret_value, _ctx, cc_pop =
+            pop_frame config fdef.item_meta.span pop_return_value ctx
           in
-          let back_el = RegionGroupId.Map.of_list back_el in
-          (* Put everything together *)
-          synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
-        else None
+          (* Generate the Return node *)
+          cc_pop (SA.ReturnWithLoop (loop_id, inside_loop))
+        in
+        (* Backward translation: introduce "return"
+           abstractions to consume the return value, then end all the
+           abstractions up to the one in which we are interested.
+        *)
+        let is_regular_return = false in
+        let finish_back_eval back_id =
+          evaluate_function_symbolic_synthesize_backward_from_return config fdef
+            inst_sg back_id (Some loop_id) is_regular_return inside_loop ctx
+        in
+        let back_el =
+          RegionGroupId.mapi
+            (fun gid _ -> (gid, finish_back_eval gid))
+            regions_hierarchy
+        in
+        let back_el = RegionGroupId.Map.of_list back_el in
+        (* Put everything together *)
+        synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
     | Panic ->
         (* Note that as we explore all the execution branches, one of
          * the executions can lead to a panic *)
-        if synthesize then Some SA.Panic else None
+        SA.Panic
     | Unit | Break _ | Continue _ ->
         craise __FILE__ __LINE__ fdef.item_meta.span
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
@@ -624,12 +615,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
-      let el =
-        List.map Option.get
-          (List.map (fun (ctx, res) -> finish res ctx) ctx_resl)
-      in
-      cc (Some el)
-    with CFailure (span, msg) -> Some (Error (span, msg))
+      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+      cc el
+    with CFailure (span, msg) -> Error (span, msg)
   in
   (* Return *)
   (input_svs, symbolic)