diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Crates.ml | 2 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 7 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 3 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 3 | ||||
| -rw-r--r-- | compiler/Utils.ml | 2 | ||||
| -rw-r--r-- | compiler/dune | 63 |
7 files changed, 68 insertions, 22 deletions
diff --git a/compiler/Crates.ml b/compiler/Crates.ml index 844afb94..eb47a8e1 100644 --- a/compiler/Crates.ml +++ b/compiler/Crates.ml @@ -16,6 +16,7 @@ type declaration_group = | Global of GlobalDeclId.id [@@deriving show] +(** LLBC crate *) type llbc_crate = { name : string; declarations : declaration_group list; @@ -23,7 +24,6 @@ type llbc_crate = { functions : fun_decl list; globals : global_decl list; } -(** LLBC crate *) let compute_defs_maps (c : llbc_crate) : type_decl TypeDeclId.Map.t diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 248ad8b3..39f85581 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -11,6 +11,10 @@ open LlbcAst open Crates module EU = ExpressionsUtils +(** Various information about a function. + + Note that not all this information is used yet to adjust the extraction yet. + *) type fun_info = { can_fail : bool; (* Not used yet: all the extracted functions use an error monad *) @@ -18,13 +22,9 @@ type fun_info = { divergent : bool; (* Not used yet *) } [@@deriving show] -(** Various information about a function. - Note that not all this information is used yet to adjust the extraction yet. - *) - -type modules_funs_info = fun_info FunDeclId.Map.t (** Various information about a module's functions *) +type modules_funs_info = fun_info FunDeclId.Map.t let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t) (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index d74ee85f..0f6ed530 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -110,8 +110,8 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) ctx (** Convert an operand constant operand value to a typed value *) -let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) : V.typed_value - = +let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) : + V.typed_value = (* Check the type while converting - we actually need some information * contained in the type *) log#ldebug @@ -522,7 +522,8 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) | Error _ -> raise (Failure "Disciminant id out of range") (* Should really never happen *) | Ok sv -> - cf { V.value = V.Primitive (PV.Scalar sv); ty = Integer Isize })) + cf { V.value = V.Primitive (PV.Scalar sv); ty = Integer Isize }) + ) | _ -> raise (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v)) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 1d95c4b9..6dc8b402 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -136,7 +136,8 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) else let value : V.avalue = match (v.V.value, ty) with - | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.APrimitive cv + | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> + V.APrimitive cv | V.Adt adt, T.Adt (id, region_params, tys) -> (* Retrieve the types of the fields *) let field_types = diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index f5756046..30a89fee 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -42,7 +42,8 @@ let compute_primitive_value_ty (cv : primitive_value) : ty = | Char _ -> Char | String _ -> Str -let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern = +let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern + = let ty = compute_primitive_value_ty cv in { value = PatConstant cv; ty } diff --git a/compiler/Utils.ml b/compiler/Utils.ml index a285e869..9a79eb55 100644 --- a/compiler/Utils.ml +++ b/compiler/Utils.ml @@ -1,6 +1,6 @@ -exception Found (** Utility exception When looking for something while exploring a term, it can be easier to just throw an exception to signal we found what we were looking for. *) +exception Found diff --git a/compiler/dune b/compiler/dune index 08b0d30f..f0fd2102 100644 --- a/compiler/dune +++ b/compiler/dune @@ -15,16 +15,59 @@ (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) (libraries ppx_deriving yojson zarith easy_logging core_unix) - (modules Assumed Collections ConstStrings Contexts Cps Crates Errors - Expressions ExpressionsUtils ExtractToFStar FunsAnalysis Identifiers - InterpreterBorrowsCore InterpreterBorrows InterpreterExpansion - InterpreterExpressions Interpreter InterpreterPaths InterpreterProjectors - InterpreterStatements InterpreterUtils Invariants LlbcAst LlbcAstUtils - LlbcOfJson Logging Meta Names OfJsonBasic PrePasses Print PrintPure - PureMicroPasses Pure PureToExtract PureTypeCheck PureUtils Scalars - StringUtils Substitute SymbolicAst SymbolicToPure SynthesizeSymbolic - TranslateCore Translate TypesAnalysis Types TypesUtils Utils Values - ValuesUtils PrimitiveValues)) + (modules + Assumed + Collections + ConstStrings + Contexts + Cps + Crates + Errors + Expressions + ExpressionsUtils + ExtractToFStar + FunsAnalysis + Identifiers + InterpreterBorrowsCore + InterpreterBorrows + InterpreterExpansion + InterpreterExpressions + Interpreter + InterpreterPaths + InterpreterProjectors + InterpreterStatements + InterpreterUtils + Invariants + LlbcAst + LlbcAstUtils + LlbcOfJson + Logging + Meta + Names + OfJsonBasic + PrePasses + Print + PrintPure + PureMicroPasses + Pure + PureToExtract + PureTypeCheck + PureUtils + Scalars + StringUtils + Substitute + SymbolicAst + SymbolicToPure + SynthesizeSymbolic + TranslateCore + Translate + TypesAnalysis + Types + TypesUtils + Utils + Values + ValuesUtils + PrimitiveValues)) (documentation (package aeneas)) |