summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean42
-rw-r--r--compiler/Driver.ml14
-rw-r--r--compiler/Extract.ml8
-rw-r--r--compiler/ExtractAssumed.ml49
-rw-r--r--compiler/ExtractBase.ml22
-rw-r--r--compiler/LlbcAstUtils.ml20
-rw-r--r--compiler/Translate.ml36
-rw-r--r--compiler/dune1
8 files changed, 154 insertions, 38 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index ffc969f3..fa5a63cd 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int :=
| .Usize => Scalar.max .U32
| _ => Scalar.max ty
+theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by
+ cases ty <;> simp [Scalar.min, Scalar.max]
+ . simp [Isize.min, Isize.max]
+ have h1 := Isize.refined_min.property
+ have h2 := Isize.refined_max.property
+ cases h1 <;> cases h2 <;> simp [*]
+ . simp [Usize.max]
+ have h := Usize.refined_max.property
+ cases h <;> simp [*]
+
+theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by
+ have := Scalar.min_lt_max ty
+ int_tac
+
theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by
cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
have h := Isize.refined_min.property
@@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
@[reducible] def U64 := Scalar .U64
@[reducible] def U128 := Scalar .U128
+-- TODO: reducible?
+@[reducible] def isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def i8_min : I8 := Scalar.ofInt I8.min
+@[reducible] def i8_max : I8 := Scalar.ofInt I8.max
+@[reducible] def i16_min : I16 := Scalar.ofInt I16.min
+@[reducible] def i16_max : I16 := Scalar.ofInt I16.max
+@[reducible] def i32_min : I32 := Scalar.ofInt I32.min
+@[reducible] def i32_max : I32 := Scalar.ofInt I32.max
+@[reducible] def i64_min : I64 := Scalar.ofInt I64.min
+@[reducible] def i64_max : I64 := Scalar.ofInt I64.max
+@[reducible] def i128_min : I128 := Scalar.ofInt I128.min
+@[reducible] def i128_max : I128 := Scalar.ofInt I128.max
+
+-- TODO: reducible?
+@[reducible] def usize_min : Usize := Scalar.ofInt Usize.min
+@[reducible] def usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
+@[reducible] def u8_min : U8 := Scalar.ofInt U8.min
+@[reducible] def u8_max : U8 := Scalar.ofInt U8.max
+@[reducible] def u16_min : U16 := Scalar.ofInt U16.min
+@[reducible] def u16_max : U16 := Scalar.ofInt U16.max
+@[reducible] def u32_min : U32 := Scalar.ofInt U32.min
+@[reducible] def u32_max : U32 := Scalar.ofInt U32.max
+@[reducible] def u64_min : U64 := Scalar.ofInt U64.min
+@[reducible] def u64_max : U64 := Scalar.ofInt U64.max
+@[reducible] def u128_min : U128 := Scalar.ofInt U128.min
+@[reducible] def u128_max : U128 := Scalar.ofInt U128.max
+
-- TODO: below: not sure this is the best way.
-- Should we rather overload operations like +, -, etc.?
-- Also, it is possible to automate the generation of those definitions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index d88962db..0fde1d74 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -222,20 +222,6 @@ let () =
in
if has_loops then log#lwarning (lazy "Support for loops is experimental");
- (* If we target Lean, we request the crates to be split into several files
- whenever there are opaque functions *)
- if
- !backend = Lean
- && A.FunDeclId.Map.exists
- (fun _ (d : A.fun_decl) -> d.body = None)
- m.functions
- && not !split_files
- then (
- log#error
- "For Lean, we request the -split-file option whenever using opaque \
- functions";
- fail ());
-
(* We don't support mutually recursive definitions with decreases clauses in Lean *)
if
!backend = Lean && !extract_decreases_clauses
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index de6c2fc8..74540787 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -8,6 +8,7 @@ open Pure
open PureUtils
open TranslateCore
open ExtractBase
+open ExtractAssumed
open StringUtils
open Config
module F = Format
@@ -3852,8 +3853,13 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the type *)
F.pp_open_hovbox fmt 0;
extract_ty ctx fmt TypeDeclId.Set.empty false ty;
+ (* Close the definition *)
+ F.pp_print_string fmt ")";
+ F.pp_close_box fmt ();
+ (* Close the definition box *)
F.pp_close_box fmt ();
- (* Close the definition boxe *) F.pp_close_box fmt ()
+ (* Add a line *)
+ F.pp_print_space fmt ()
(** Extract a global declaration.
diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml
new file mode 100644
index 00000000..bbcedb2b
--- /dev/null
+++ b/compiler/ExtractAssumed.ml
@@ -0,0 +1,49 @@
+(** This file declares external identifiers that we catch to map them to
+ definitions coming from the standard libraries in our backends. *)
+
+open Utils
+open StringUtils
+open Names
+
+type simple_name = string list [@@deriving show, ord]
+
+let name_to_simple_name (s : name) : simple_name =
+ (* We simply ignore the disambiguators *)
+ List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
+
+(** Small helper which cuts a string at the occurrences of "::" *)
+let string_to_simple_name (s : string) : simple_name =
+ (* No function to split by using string separator?? *)
+ let name = String.split_on_char ':' s in
+ List.filter (fun s -> s <> "") name
+
+module SimpleNameOrd = struct
+ type t = simple_name
+
+ let compare = compare_simple_name
+ let to_string = show_simple_name
+ let pp_t = pp_simple_name
+ let show_t = show_simple_name
+end
+
+module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+
+let assumed_globals : (string * string) list =
+ [
+ ("core::num::usize::MAX", "usize_max");
+ ("core::num::u8::MAX", "u8_max");
+ ("core::num::u16::MAX", "u16_max");
+ ("core::num::u32::MAX", "u32_max");
+ ("core::num::u64::MAX", "u64_max");
+ ("core::num::u128::MAX", "u128_max");
+ ("core::num::isize::MAX", "isize_max");
+ ("core::num::i8::MAX", "i8_max");
+ ("core::num::i16::MAX", "i16_max");
+ ("core::num::i32::MAX", "i32_max");
+ ("core::num::i64::MAX", "i64_max");
+ ("core::num::i128::MAX", "i128_max");
+ ]
+
+let assumed_globals_map : string SimpleNameMap.t =
+ SimpleNameMap.of_list
+ (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 435aa10c..9c9e08a5 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -5,6 +5,7 @@ open TranslateCore
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
+open ExtractAssumed
(** The local logger *)
let log = L.pure_to_extract_log
@@ -1198,12 +1199,23 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
extraction_ctx =
(* TODO: update once the body id can be an option *)
let is_opaque = false in
- let name = ctx.fmt.global_name def.name in
let decl = GlobalId def.def_id in
- let body = FunId (FromLlbc (Regular def.body_id, None, None)) in
- let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in
- let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
- ctx
+
+ (* Check if the global corresponds to an assumed global that we should map
+ to a custom definition in our standard library (for instance, happens
+ with "core::num::usize::MAX") *)
+ let sname = name_to_simple_name def.name in
+ match SimpleNameMap.find_opt sname assumed_globals_map with
+ | Some name ->
+ (* Yes: register the custom binding *)
+ ctx_add is_opaque decl name ctx
+ | None ->
+ (* Not the case: "standard" registration *)
+ let name = ctx.fmt.global_name def.name in
+ let body = FunId (FromLlbc (Regular def.body_id, None, None)) in
+ let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in
+ let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
+ ctx
let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
(ctx : extraction_ctx) : string =
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 1111c297..8c8bbabe 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -12,3 +12,23 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).name
| Assumed aid -> Assumed.get_assumed_name aid
+
+(** Return the opaque declarations found in the crate.
+
+ Remark: the list of functions also contains the list of opaque global bodies.
+ *)
+let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list =
+ let open ExtractAssumed in
+ let is_opaque_fun (d : fun_decl) : bool =
+ let sname = name_to_simple_name d.name in
+ d.body = None && not (SimpleNameMap.mem sname assumed_globals_map)
+ in
+ let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
+ (* Note that by checking the function bodies we also the globals *)
+ ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types),
+ List.filter is_opaque_fun (FunDeclId.Map.values k.functions) )
+
+(** Return true if the crate contains opaque declarations, ignoring the assumed
+ definitions. *)
+let crate_has_opaque_decls (k : crate) : bool =
+ crate_get_opaque_decls k <> ([], [])
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index a4041751..90066163 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -430,19 +430,9 @@ type gen_config = {
}
(** Returns the pair: (has opaque type decls, has opaque fun decls) *)
-let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
- let has_opaque_types =
- Pure.TypeDeclId.Map.exists
- (fun _ (d : Pure.type_decl) ->
- match d.kind with Opaque -> true | _ -> false)
- ctx.trans_types
- in
- let has_opaque_funs =
- A.FunDeclId.Map.exists
- (fun _ (trans : pure_fun_translation) -> Option.is_none trans.fwd.f.body)
- ctx.trans_funs
- in
- (has_opaque_types, has_opaque_funs)
+let crate_has_opaque_decls (ctx : gen_ctx) : bool * bool =
+ let types, funs = LlbcAstUtils.crate_get_opaque_decls ctx.crate in
+ (types <> [], funs <> [])
(** Export a type declaration.
@@ -557,11 +547,20 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let body = trans.fwd.f in
let is_opaque = Option.is_none body.Pure.body in
- if
+ (* Check if we extract the global *)
+ let extract =
config.extract_globals
&& (((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque))
- then
+ in
+ (* Check if it is an assumed global - if yes, we ignore it because we
+ map the definition to one in the standard library *)
+ let open ExtractAssumed in
+ let sname = name_to_simple_name global.name in
+ let extract =
+ extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+ in
+ if extract then
(* We don't wrap global declaration groups between calls to functions
[{start, end}_global_decl_group] (which don't exist): global declaration
groups are always singletons, so the [extract_global_decl] function
@@ -828,7 +827,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
config.extract_opaque && config.extract_fun_decls
&& !Config.wrap_opaque_in_sig
&&
- let _, opaque_funs = module_has_opaque_decls ctx in
+ let _, opaque_funs = crate_has_opaque_decls ctx in
opaque_funs
in
if wrap_in_sig then (
@@ -1233,7 +1232,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(* Check if there are opaque types and functions - in which case we need
* to split *)
- let has_opaque_types, has_opaque_funs = module_has_opaque_decls ctx in
+ let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx in
let has_opaque_types = has_opaque_types || !Config.use_state in
(* Extract the types *)
@@ -1302,7 +1301,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
in
extract_file template_clauses_config ctx file_info);
- (* Extract the opaque functions, if needed *)
+ (* Extract the opaque declarations, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
(* In the case of Lean we generate a template file *)
@@ -1330,6 +1329,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
{
base_gen_config with
extract_fun_decls = true;
+ extract_globals = true;
extract_transparent = false;
extract_opaque = true;
interface = true;
diff --git a/compiler/dune b/compiler/dune
index db099c3c..2f5a0a44 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -22,6 +22,7 @@
Expressions
ExpressionsUtils
Extract
+ ExtractAssumed
ExtractBase
FunsAnalysis
Identifiers
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:19:54 +0000