Merge pull request #48 from AeneasVerif/son_closures

Prepare support for function pointers and closures

1 files changed, 40 insertions, 10 deletions

diff --git a/compiler/Main.ml b/compiler/Main.ml
index 7f98f581..835b9088 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -66,7 +66,7 @@ let () =
   (* Print the imported llbc *)
   let print_llbc = ref false in
 
-  let spec =
+  let spec_ls =
     [
       ( "-backend",
         Arg.Symbol (backend_names, set_backend),
@@ -123,7 +123,7 @@ let () =
     ]
   in
 
-  let spec = Arg.align spec in
+  let spec = Arg.align spec_ls in
   let filenames = ref [] in
   let add_filename f = filenames := f :: !filenames in
   Arg.parse spec add_filename usage;
@@ -132,20 +132,50 @@ let () =
     exit 1
   in
 
-  if !extract_template_decreases_clauses then extract_decreases_clauses := true;
+  (* Small helper to check the validity of the input arguments and print
+     an error if necessary *)
+  let check_arg_name name =
+    assert (List.exists (fun (n, _, _) -> n = name) spec_ls)
+  in
+  let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool)
+      (name1 : string) : unit =
+    check_arg_name name0;
+    check_arg_name name1;
+    if (not arg0) || arg1 then ()
+    else (
+      log#error "Invalid command-line arguments: the use of %s requires %s"
+        name0 name1;
+      fail ())
+  in
+
+  let check_arg_not (arg0 : bool) (name0 : string) (arg1 : bool)
+      (name1 : string) : unit =
+    check_arg_name name0;
+    check_arg_name name1;
+    if (not arg0) || not arg1 then ()
+    else (
+      log#error
+        "Invalid command-line arguments: the use of %s is incompatible with %s"
+        name0 name1;
+      fail ())
+  in
+
   if !print_llbc then main_log#set_level EL.Debug;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
-  assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
+  check_arg_implies
+    !extract_template_decreases_clauses
+    "-template-clauses" !extract_decreases_clauses "-decreases-clauses";
   (* Sanity check: -backward-no-state-update ==> -state *)
-  assert ((not !backward_no_state_update) || !use_state);
+  check_arg_implies !backward_no_state_update "-backward-no-state-update"
+    !use_state "-state";
   (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *)
-  assert (
-    (not !use_fuel)
-    || (not !extract_decreases_clauses)
-       && not !extract_template_decreases_clauses);
+  check_arg_not !use_fuel "-use-fuel" !extract_decreases_clauses
+    "-decreases-clauses";
   (* We have: not generate_lib_entry_point ==> split_files *)
-  assert (!split_files || !generate_lib_entry_point);
+  check_arg_implies
+    (not !generate_lib_entry_point)
+    "-no-gen-lib-entry" !split_files "-split-files";
   if !lean_gen_lakefile && not (!backend = Lean) then
     log#error
       "The -lean-default-lakefile option is valid only for the Lean backend";