summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-10-27 18:17:41 +0200
committerSon HO2022-10-28 17:41:04 +0200
commitcdaa37670587dadda92ddab076170eb6d8e237cd (patch)
tree4b19c44471774279bacdd55d4cc69665241351fd
parente286c339cf40c6fa4fee2b910af47ffcc34613fe (diff)
Take care of some TODOs
Diffstat (limited to '')
-rw-r--r--compiler/Errors.ml1
-rw-r--r--compiler/ExtractToFStar.ml2
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/InterpreterBorrows.ml2
-rw-r--r--compiler/InterpreterExpansion.ml2
-rw-r--r--compiler/InterpreterExpressions.ml2
-rw-r--r--compiler/InterpreterStatements.ml2
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/SymbolicToPure.ml6
-rw-r--r--compiler/dune1
10 files changed, 10 insertions, 12 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
deleted file mode 100644
index 58dd3a0b..00000000
--- a/compiler/Errors.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.Errors
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index b44b8f25..7267101c 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1,6 +1,6 @@
(** Extract to F* *)
-open Errors
+open Utils
open Pure
open PureUtils
open TranslateCore
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 7f51c5b9..f93a0ae1 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -137,7 +137,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
* will end - this will allow us to, first, mark the other return
* regions as non-endable, and, second, end those parent regions in
* proper order. *)
- let parent_rgs = list_parent_region_groups sg back_id in
+ let parent_rgs = list_ancestor_region_groups sg back_id in
let parent_input_abs_ids =
T.RegionGroupId.mapi
(fun rg_id rg ->
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 16f68d9e..e2d2bb0a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -442,7 +442,7 @@ let give_back_symbolic_value (_config : C.config)
(* Substitution function, to replace the borrow projectors over symbolic values *)
let subst (_abs : V.abs) local_given_back =
(* See the below comments: there is something wrong here *)
- let _ = raise Errors.Unimplemented in
+ let _ = raise Utils.Unimplemented in
(* Compute the projection over the given back value *)
let child_proj =
match nsv.sv_kind with
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 9a944428..cd6df2b0 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -712,7 +712,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
| T.Adt (Assumed (Vec | Option), _, _) ->
(* We can't expand those *)
raise (Failure "Attempted to greedily expand a Vec or an Option ")
- | T.Array _ -> raise Errors.Unimplemented
+ | T.Array _ -> raise Utils.Unimplemented
| T.Slice _ -> raise (Failure "Can't expand symbolic slices")
| T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
raise (Failure "Unreachable")
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 83cdfc9b..5a6947b0 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -4,7 +4,7 @@ module V = Values
module LA = LlbcAst
open Scalars
module E = Expressions
-open Errors
+open Utils
module C = Contexts
module Subst = Substitute
module L = Logging
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 308f561c..56ab05f3 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -10,7 +10,7 @@ open TypesUtils
open ValuesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
-open Errors
+open Utils
open Cps
open InterpreterUtils
open InterpreterProjectors
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 81879883..9899cfcf 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -707,7 +707,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
in
(* Compute the set of ancestors of the function in call1 *)
let call1_ancestors =
- LlbcAstUtils.list_parent_region_groups sg rg_id1
+ LlbcAstUtils.list_ancestor_region_groups sg rg_id1
in
(* Check if the function used in call0 is inside *)
T.RegionGroupId.Set.mem rg_id0 call1_ancestors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index f393b059..1341bccc 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1,4 +1,4 @@
-open Errors
+open Utils
open LlbcAstUtils
open Pure
open PureUtils
@@ -525,7 +525,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
match bid with
| None -> (None, T.RegionGroupId.Set.empty)
| Some bid ->
- let parents = list_parent_region_groups sg bid in
+ let parents = list_ancestor_region_groups sg bid in
(Some bid, parents)
in
(* List the inputs for:
@@ -1721,7 +1721,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
| None -> []
| Some back_id ->
let parents_ids =
- list_ordered_parent_region_groups def.signature back_id
+ list_ordered_ancestor_region_groups def.signature back_id
in
let backward_ids = List.append parents_ids [ back_id ] in
List.concat
diff --git a/compiler/dune b/compiler/dune
index d3f5eaec..af4cdb08 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -18,7 +18,6 @@
Contexts
Cps
Crates
- Errors
Expressions
ExpressionsUtils
ExtractToFStar