diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | aeneas.opam | 29 | ||||
| -rw-r--r-- | dune-project | 23 | ||||
| -rw-r--r-- | src/PrintSymbolicAst.ml | 59 | ||||
| -rw-r--r-- | src/driver.ml (renamed from src/main.ml) | 19 | ||||
| -rw-r--r-- | src/dune | 27 |
6 files changed, 101 insertions, 73 deletions
@@ -14,6 +14,8 @@ CHARON_TESTS_DIR = CHARON_OPTIONS = CHARON_TESTS_SRC = +AENEAS_DRIVER = src/driver.exe + # The user can specify additional translation options for Aeneas: OPTIONS ?= @@ -29,8 +31,15 @@ build-tests-verify: build tests verify # Build the project .PHONY: build -build: - dune build src/main.exe +build: build-driver build-lib + +.PHONY: build-driver +build-driver: + dune build $(AENEAS_DRIVER) + +.PHONY: build-lib +build-lib: + dune build src/aeneas.cmxs # Test the project by translating test files to F* .PHONY: tests @@ -91,10 +100,10 @@ trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc trans-polonius-%: gen-llbc-polonius-% - dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) trans-%: gen-llbc-% - dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc doc: diff --git a/aeneas.opam b/aeneas.opam new file mode 100644 index 00000000..4048f9a0 --- /dev/null +++ b/aeneas.opam @@ -0,0 +1,29 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.1" +synopsis: "" +description: "" +maintainer: ["son.ho@inria.fr"] +authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"] +license: "Apache-2.0" +homepage: "https://github.com/AeneasVerif/aeneas" +bug-reports: "https://github.com/AeneasVerif/aeneas/issues" +depends: [ + "dune" {>= "2.8"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/AeneasVerif/aeneas.git" diff --git a/dune-project b/dune-project index c2e46604..f8b418f2 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,24 @@ (lang dune 2.8) + +(name aeneas) + +(version 0.1) + +(generate_opam_files true) + +(formatting) + +(source + (uri git+https://github.com/AeneasVerif/aeneas.git)) + +(homepage "https://github.com/AeneasVerif/aeneas") + +(bug_reports "https://github.com/AeneasVerif/aeneas/issues") + +(authors + "Son Ho" + "Jonathan Protzenko" + "Aymeric Fromherz" + "Sidney Congard") + +(license Apache-2.0)
\ No newline at end of file diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml deleted file mode 100644 index 37b7555e..00000000 --- a/src/PrintSymbolicAst.ml +++ /dev/null @@ -1,59 +0,0 @@ -(** Printing utilities for symbolic AST. - - We don't put this in [Print] because: - - [Print] is getting quite big - - if we do so we have a dependency cycle... - *) - -open Errors -open Identifiers -open FunIdentifier -module T = Types -module TU = TypesUtils -module V = Values -module E = Expressions -module A = LlbcAst -module C = Contexts -open SymbolicAst -module P = Print -module PT = Print.Types - -type formatting_ctx = { - type_context : C.type_context; - fun_context : A.fun_decl FunDeclId.Map.t; - type_vars : T.type_var list; -} - -type formatter = P.Values.value_formatter - -let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter = - (* We shouldn't use [rvar_to_string] *) - let rvar_to_string _ = failwith "Unexpected use of rvar_to_string" in - let r_to_string r = PT.region_id_to_string r in - - let type_var_id_to_string vid = - let v = T.TypeVarId.nth ctx.type_vars vid in - v.name - in - let type_decl_id_to_string def_id = - let def = T.TypeDeclId.Map.find def_id ctx.type_context.type_decls in - P.name_to_string def.name - in - let adt_variant_to_string = - P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls - in - (* We shouldn't use [var_id_to_string] *) - let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in - - let adt_field_names = - P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls - in - { - rvar_to_string; - r_to_string; - type_var_id_to_string; - type_decl_id_to_string; - adt_variant_to_string; - var_id_to_string; - adt_field_names; - } diff --git a/src/main.ml b/src/driver.ml index 05e96af9..ae9d238a 100644 --- a/src/main.ml +++ b/src/driver.ml @@ -1,12 +1,15 @@ -open LlbcOfJson -open Logging -open Print -module T = Types -module A = LlbcAst -module I = Interpreter +open Aeneas.LlbcOfJson +open Aeneas.Logging +open Aeneas.Print +module T = Aeneas.Types +module A = Aeneas.LlbcAst +module I = Aeneas.Interpreter module EL = Easy_logging.Logging -module TA = TypesAnalysis -module Micro = PureMicroPasses +module TA = Aeneas.TypesAnalysis +module Micro = Aeneas.PureMicroPasses +module Print = Aeneas.Print +module PrePasses = Aeneas.PrePasses +module Translate = Aeneas.Translate (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. @@ -1,10 +1,33 @@ ;; core: for Core.Unix.mkdir_p (executable - (name main) + (name driver) + (public_name aeneas_driver) + (package aeneas) (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) - (libraries ppx_deriving yojson zarith easy_logging core_unix)) + (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas) + (modules driver)) + +(library + (name aeneas) ;; The name as used in the project + (public_name aeneas) ;; The name as revealed to the projects importing this library + (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)) + +(documentation + (package aeneas)) (env (dev |