summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile2
-rw-r--r--TODO.md5
-rw-r--r--src/Pure.ml13
-rw-r--r--src/PureMicroPasses.ml25
-rw-r--r--src/SymbolicToPure.ml3
5 files changed, 43 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index 53382164..25a8b06f 100644
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,7 @@ test: build translate-no_nested_borrows translate-hashmap translate-paper
# Add specific options to some tests
translate-no_nested_borrows translate-paper: \
- TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses
+ TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-state -no-decreases-clauses
translate-no_nested_borrows translate-paper: SUBDIR:=misc
translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state
translate-hashmap: SUBDIR:=hashmap
diff --git a/TODO.md b/TODO.md
index 62eb95d5..3816cda8 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,8 +1,7 @@
# TODO
-0. borrows which are never ended? Drop locals in *symbolic* modes upon return
-
-0. improve variable names generation: "hash_map" -> "hm" (and not just "h")
+0. Improve treatments of error and state error monads. In particular, introduce
+ `return` and `fail`, and remove `Return` and `Fail`.
0. replace all the `failwith` with `raise (Failure ...)`: in CPS, it messes
up with provenance tracking
diff --git a/src/Pure.ml b/src/Pure.ml
index 96c7d211..bdcb35f8 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -34,6 +34,9 @@ type integer_type = T.integer_type [@@deriving show, ord]
*)
type assumed_ty = State | Result | Vec | Option [@@deriving show, ord]
+(* TODO: we should never directly manipulate `Return` and `Fail`, but rather
+ * the monadic functions `return` and `fail` (makes treatment of error and
+ * state-error monads more uniform) *)
let result_return_id = VariantId.of_int 0
let result_fail_id = VariantId.of_int 1
@@ -375,7 +378,15 @@ type unop = Not | Neg of integer_type [@@deriving show, ord]
type fun_id =
| Regular of A.fun_id * T.RegionGroupId.id option
(** Backward id: `Some` if the function is a backward function, `None`
- if it is a forward function *)
+ if it is a forward function.
+
+ TODO: we need to redefine A.fun_id here, to add `fail` and
+ `return` (important to get a unified treatment of the state-error
+ monad). For now, when using the state-error monad: extraction
+ works only if we unfold all the monadic let-bindings, and we
+ then replace the content of the occurrences of `Return` to also
+ return the state (which is really super ugly).
+ *)
| Unop of unop
| Binop of E.binop * integer_type
[@@deriving show, ord]
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 61d247ea..6c61b9dc 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1008,6 +1008,31 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
let switch_body = Match [ fail_branch; success_branch ] in
let e = Switch (re, switch_body) in
self#visit_expression state_var e
+
+ method! visit_Value state_var rv mp =
+ if config.use_state_monad then
+ match rv.ty with
+ | Adt (Assumed Result, _) -> (
+ match rv.value with
+ | RvAdt av ->
+ (* We only need to replace the content of `Return ...` *)
+ (* TODO: type checking is completely broken at this point... *)
+ let variant_id = Option.get av.variant_id in
+ if variant_id = result_return_id then
+ let res_v = Collections.List.to_cons_nil av.field_values in
+ let state_value = mk_typed_rvalue_from_var state_var in
+ let res = mk_simpl_tuple_rvalue [ state_value; res_v ] in
+ let res = mk_result_return_rvalue res in
+ (mk_value_expression res None).e
+ else super#visit_Value state_var rv mp
+ | _ -> raise (Failure "Unrechable"))
+ | _ -> super#visit_Value state_var rv mp
+ else super#visit_Value state_var rv mp
+ (** We also need to update values, in case this value is `Return ...`.
+
+ TODO: this is super ugly... We need to use the monadic functions
+ `fail` and `return` instead.
+ *)
end
in
(* Update the body *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index f2ed1053..5709ce23 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -972,6 +972,9 @@ and translate_return (_config : config) (opt_v : V.typed_value option)
(* Forward function *)
let v = Option.get opt_v in
let v = typed_value_to_rvalue ctx v in
+ (* TODO: we need to use a `return` function (otherwise we have problems
+ * with the state-error monad). We also need to update the type when using
+ * a state-error monad. *)
let v = mk_result_return_rvalue v in
let e = Value (v, None) in
let ty = v.ty in