1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
open CfimOfJson
open Logging
open Print
module T = Types
module A = CfimAst
module I = Interpreter
module EL = Easy_logging.Logging
module TA = TypesAnalysis
module Micro = PureMicroPasses
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.
* JP: are you running with OCAMLRUNPARAM=b=1? *)
let () = Printexc.record_backtrace true
let usage =
Printf.sprintf
{|Aeneas: verification of Rust programs by translation to pure lambda calculus
Usage: %s [OPTIONS] FILE
|}
Sys.argv.(0)
let () =
(* Read the command line arguments *)
let dest_dir = ref "" in
let decompose_monads = ref false in
let unfold_monads = ref true in
let filter_unused_calls = ref true in
let spec =
[
("-dest", Arg.Set_string dest_dir, " Specify the output directory");
( "-decompose-monads",
Arg.Set decompose_monads,
" Decompose the monadic let-bindings.\n\n\
\ Introduces a temporary variable which is later decomposed,\n\
\ when the pattern on the left of the monadic let is not a \n\
\ variable.\n\
\ \n\
\ Example:\n\
\ `(x, y) <-- f (); ...` ~~>\n\
\ `tmp <-- f (); let (x, y) = tmp in ...`\n\
\ " );
( "-unfold-monads",
Arg.Set unfold_monads,
" Unfold the monadic let-bindings to matches" );
( "-filter-unused-calls",
Arg.Set filter_unused_calls,
" Filter the unused function calls, when possible" );
]
in
let spec = Arg.align spec in
let filenames = ref [] in
let add_filename f = filenames := f :: !filenames in
Arg.parse spec add_filename usage;
let fail () =
print_string usage;
exit 1
in
(* Retrieve and check the filename *)
let filename =
match !filenames with
| [ f ] ->
if not (Filename.check_suffix f ".cfim") then (
print_string "Unrecognized file extension";
fail ())
else if not (Sys.file_exists f) then (
print_string "File not found";
fail ())
else f
| _ ->
(* For now, we only process one file at a time *)
print_string usage;
exit 1
in
(* Check the destination directory *)
let dest_dir =
if !dest_dir = "" then Filename.dirname filename else !dest_dir
in
(* Set up the logging - for now we use default values - TODO: use the
* command-line arguments *)
Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
main_log#set_level EL.Debug;
interpreter_log#set_level EL.Debug;
statements_log#set_level EL.Debug;
paths_log#set_level EL.Warning;
expressions_log#set_level EL.Warning;
expansion_log#set_level EL.Warning;
borrows_log#set_level EL.Warning;
invariants_log#set_level EL.Warning;
symbolic_to_pure_log#set_level EL.Debug;
pure_micro_passes_log#set_level EL.Debug;
pure_to_extract_log#set_level EL.Debug;
translate_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file filename in
match cfim_module_of_json json with
| Error s ->
main_log#error "error: %s\n" s;
exit 1
| Ok m ->
(* Print the module *)
main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
(* Some options for the execution *)
let config =
{
C.check_invariants = true;
greedy_expand_symbolics_with_borrows = true;
}
in
(* Test the unit functions with the concrete interpreter *)
I.Test.test_unit_functions config m;
(* Evaluate the symbolic interpreter on the functions, ignoring the
* functions which contain loops - TODO: remove *)
let synthesize = true in
I.Test.test_functions_symbolic config synthesize m;
(* Translate the functions *)
let test_unit_functions = true in
let micro_passes_config =
{
Micro.decompose_monadic_let_bindings = !decompose_monads;
unfold_monadic_let_bindings = !unfold_monads;
filter_unused_monadic_calls = !filter_unused_calls;
}
in
Translate.translate_module filename dest_dir config micro_passes_config
test_unit_functions m
|
