Experiment: dunify proofs

compiler/Makefile

@@ -39,10 +39,10 @@ all:
 	for p in _build/install/default/bin/*; do ln -sf $$p $$(basename $$p); done
 
 CIL:
-	$(RM) -f src/CIL/*.ml src/CIL/*.mli ../proofs/extraction.vo
+	$(RM) -f src/CIL/*.ml src/CIL/*.mli
 	$(MAKE) -C ../proofs extraction
-	cp ../proofs/lang/ocaml/*.ml  src/CIL/
-	cp ../proofs/lang/ocaml/*.mli src/CIL/
+	cp ../proofs/_build/default/extraction/*.ml  src/CIL/
+	cp ../proofs/_build/default/extraction/*.mli src/CIL/
 
 check: all
 	$(CHECK) --report=report.log $(CHECKCATS)

compiler/entry/commonCLI.ml

@@ -91,8 +91,8 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
       let cp = Conv.cuprog_of_prog prog in
       (* We need to avoid catching compilation errors. *)
       match Compile.compile (module Arch) stop prog cp with
-      | Utils0.Ok _ -> assert false
-      | Utils0.Error e ->
+      | Result.Ok _ -> assert false
+      | Result.Error e ->
           let e = Conv.error_of_cerror (Printer.pp_err ~debug:false) e in
           raise (HiError e)
       | exception Found -> !res

compiler/src/compile.ml

@@ -63,8 +63,8 @@ let do_spill_unspill asmop ?(debug = false) cp =
       (fun k ii -> Conv.fresh_var_ident k ii (Uint63.of_int 0))
       p
   with
-  | Utils0.Error msg -> Error (Conv.error_of_cerror (Printer.pp_err ~debug) msg)
-  | Utils0.Ok p -> Ok (Conv.prog_of_cuprog p)
+  | Result.Error msg -> Error (Conv.error_of_cerror (Printer.pp_err ~debug) msg)
+  | Result.Ok p -> Ok (Conv.prog_of_cuprog p)
 
 let do_wint_int
    (type reg regx xreg rflag cond asm_op extra_op)
@@ -98,8 +98,8 @@ let do_wint_int
   let cp = Wint_int.wi2i_prog Arch.asmOp Arch.msf_size info cp in
   let cp =
     match cp with
-    | Utils0.Ok cp -> cp
-    | Utils0.Error e ->
+    | Result.Ok cp -> cp
+    | Result.Error e ->
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:false) e in
       raise (HiError e) in
   let (gd, fdso) = Conv.prog_of_cuprog cp in

compiler/src/conv.ml

@@ -292,7 +292,7 @@ let to_array ty p t =
   let ws, n = array_kind ty in
   let get i = 
     match Warray_.WArray.get p Aligned Warray_.AAscale ws t (cz_of_int i) with
-    | Utils0.Ok w -> z_of_word ws w
+    | Result.Ok w -> z_of_word ws w
     | _    -> assert false in
   ws, Array.init n get
 

compiler/src/evaluator.ml

@@ -1,5 +1,6 @@
 open BinNums
-open Utils0 
+open Utils0
+open Result
 open Type
 open Sem_type
 open Warray_
@@ -11,7 +12,7 @@ open Psem_defs
 open Values
 open Sem_params
 
-exception Eval_error of instr_info * Utils0.error 
+exception Eval_error of instr_info * error
 
 let pp_error fmt err =
   Format.fprintf fmt "%s" @@

compiler/src/evaluator.mli

@@ -1,4 +1,4 @@
-exception Eval_error of Expr.instr_info * Utils0.error
+exception Eval_error of Expr.instr_info * Result.error
 
 val exec :
   'syscall_state Sem_params.coq_EstateParams ->
@@ -33,4 +33,4 @@ val run :
   Low_memory.Memory.mem * Values.values
 
 val pp_val : Format.formatter -> Values.value -> unit
-val pp_error : Format.formatter -> Utils0.error -> unit
+val pp_error : Format.formatter -> Result.error -> unit

compiler/src/main_compiler.ml

@@ -212,8 +212,8 @@ let main () =
               (match
                  Evaluator.initial_memory Arch.reg_size (Z.of_string "1024") m
                with
-               | Utils0.Ok m -> m
-               | Utils0.Error err -> raise (Evaluator.Eval_error (ii, err)))
+               | Result.Ok m -> m
+               | Result.Error err -> raise (Evaluator.Eval_error (ii, err)))
               |> Evaluator.run
                    (module Arch)
                    (Expr.to_uprog Arch.asmOp cprog)
@@ -231,10 +231,10 @@ let main () =
       end;
 
     begin match Compile.compile (module Arch) visit_prog_after_pass prog cprog with
-    | Utils0.Error e ->
+    | Result.Error e ->
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:!debug) e in
       raise (HiError e)
-    | Utils0.Ok asm ->
+    | Result.Ok asm ->
       if !outfile <> "" then begin
         BatFile.with_file_out !outfile (fun out ->
           let fmt = BatFormat.formatter_of_out_channel out in

compiler/src/stackAlloc.ml

@@ -194,16 +194,16 @@ let memory_analysis pp_sr pp_err ~debug up =
         get_sao
         up
     with
-    | Utils0.Ok sp -> sp
-    | Utils0.Error e ->
+    | Result.Ok sp -> sp
+    | Result.Error e ->
       let e = Conv.error_of_cerror pp_err e in
       raise (HiError e)
   in
 
   let sp' =
     match Arch.aparams.ap_lap (Conv.fresh_var_ident (Reg (Normal, Direct)) IInfo.dummy (Uint63.of_int 0)) sp with
-    | Utils0.Ok sp -> sp
-    | Utils0.Error e ->
+    | Result.Ok sp -> sp
+    | Result.Error e ->
       let e = Conv.error_of_cerror pp_err e in
       raise (HiError e)
   in
@@ -235,8 +235,8 @@ let memory_analysis pp_sr pp_err ~debug up =
     let (fn, cfd) = Conv.cufdef_of_fdef fd in
     let fd = 
       match Dead_code.dead_code_fd Arch.asmOp Arch.aparams.ap_is_move_op false tokeep fn cfd with
-      | Utils0.Ok cfd -> Conv.fdef_of_cufdef (fn, cfd)
-      | Utils0.Error _ -> assert false in 
+      | Result.Ok cfd -> Conv.fdef_of_cufdef (fn, cfd)
+      | Result.Error _ -> assert false in 
     (extra,fd) in
   let fds = List.map deadcode fds in
   if debug then

compiler/src/x86_arch_full.ml

@@ -15,10 +15,13 @@ let atoI decl =
     V.mk s (Reg(k,Direct)) (Conv.ty_of_cty t) L._dummy [] in
 
   match Arch_extra.MkAToIdent.mk decl mk_var with
-  | Utils0.Error e ->
+  | Result.Error e ->
+      (* FIXME: in this experiment, Arch_extra.MkAToIdent.mk returns a string
+         in the error case, so it is not clear what to do here *)
+      assert false (*
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:true) e in
-      raise (Utils.HiError e)
-  | Utils0.Ok atoI -> atoI
+      raise (Utils.HiError e) *)
+  | Result.Ok atoI -> atoI
 
 module X86_core = struct
   type reg = register

compiler/tests/exec/execlib.ml

@@ -27,8 +27,8 @@ let load_file name =
 
 let init_memory ms =
   match Evaluator.initial_memory Arch.reg_size (Z.of_int 1024) ms with
-  | Utils0.Error _err -> assert false
-  | Utils0.Ok m -> m
+  | Result.Error _err -> assert false
+  | Result.Ok m -> m
 
 let exec (fs, prog) ms f args =
   let f = Hashtbl.find fs f in

proofs/Makefile

@@ -15,9 +15,7 @@ uninstall: Makefile.coq
 	$(MAKE) -f Makefile.coq uninstall
 
 extraction: Makefile.coq
-	$(RM) lang/ocaml/*.ml lang/ocaml/*.mli
-	$(RM) lang/extraction.vo
-	+$(COQMAKE) lang/extraction.vo
+	dune build extraction
 
 # --------------------------------------------------------------------
 this-clean::

proofs/_CoqProject

@@ -21,8 +21,6 @@
 -R ssrmisc Jasmin
 -R itrees Jasmin
 
-ssrmisc/oseq.v
-ssrmisc/seq_extra.v
 3rdparty/ssrring.v
 3rdparty/xseq.v
 arch/arch_decl.v
@@ -38,6 +36,7 @@ compiler/allocation.v
 compiler/allocation_proof.v
 compiler/arch_params.v
 compiler/arch_params_proof.v
+compiler/arm.v
 compiler/arm_decl.v
 compiler/arm_extra.v
 compiler/arm_facts.v
@@ -46,23 +45,22 @@ compiler/arm_instr_decl_lemmas.v
 compiler/arm_lowering.v
 compiler/arm_lowering_proof.v
 compiler/arm_params.v
-compiler/arm_params_proof.v
 compiler/arm_params_common.v
 compiler/arm_params_common_proof.v
 compiler/arm_params_core.v
 compiler/arm_params_core_proof.v
+compiler/arm_params_proof.v
 compiler/arm_stack_zeroization.v
 compiler/arm_stack_zeroization_proof.v
-compiler/arm.v
-compiler/array_expansion.v
-compiler/array_expansion_proof.v
 compiler/array_copy.v
 compiler/array_copy_proof.v
+compiler/array_expansion.v
+compiler/array_expansion_proof.v
 compiler/array_init.v
 compiler/array_init_proof.v
-compiler/compiler_util.v
 compiler/compiler.v
 compiler/compiler_proof.v
+compiler/compiler_util.v
 compiler/constant_prop.v
 compiler/constant_prop_proof.v
 compiler/dead_calls.v
@@ -80,34 +78,35 @@ compiler/linearization.v
 compiler/linearization_proof.v
 compiler/load_constants_in_cond.v
 compiler/load_constants_in_cond_proof.v
-compiler/lowering.v
 compiler/lower_spill.v
 compiler/lower_spill_proof.v
+compiler/lowering.v
+compiler/lowering_lemmas.v
 compiler/makeReferenceArguments.v
 compiler/makeReferenceArguments_proof.v
 compiler/merge_varmaps.v
 compiler/merge_varmaps_proof.v
 compiler/post_unrolling_check.v
 compiler/propagate_inline.v
 compiler/propagate_inline_proof.v
+compiler/remove_globals.v
+compiler/remove_globals_proof.v
 compiler/riscv.v
 compiler/riscv_decl.v
-compiler/riscv_instr_decl.v
 compiler/riscv_extra.v
+compiler/riscv_instr_decl.v
 compiler/riscv_lower_addressing.v
 compiler/riscv_lower_addressing_proof.v
 compiler/riscv_lowering.v
 compiler/riscv_lowering_proof.v
 compiler/riscv_params.v
-compiler/riscv_params_proof.v
-compiler/riscv_params_core.v
-compiler/riscv_params_core_proof.v
 compiler/riscv_params_common.v
 compiler/riscv_params_common_proof.v
+compiler/riscv_params_core.v
+compiler/riscv_params_core_proof.v
+compiler/riscv_params_proof.v
 compiler/riscv_stack_zeroization.v
 compiler/riscv_stack_zeroization_proof.v
-compiler/remove_globals.v
-compiler/remove_globals_proof.v
 compiler/slh_lowering.v
 compiler/slh_lowering_proof.v
 compiler/stack_alloc.v
@@ -127,6 +126,7 @@ compiler/wint_int.v
 compiler/wint_int_proof.v
 compiler/wint_word.v
 compiler/wint_word_proof.v
+compiler/x86.v
 compiler/x86_decl.v
 compiler/x86_extra.v
 compiler/x86_instr_decl.v
@@ -136,7 +136,6 @@ compiler/x86_params.v
 compiler/x86_params_proof.v
 compiler/x86_stack_zeroization.v
 compiler/x86_stack_zeroization_proof.v
-compiler/x86.v
 itrees/it_exec.v
 itrees/rutt_extras.v
 itrees/xrutt.v
@@ -159,26 +158,25 @@ lang/linear.v
 lang/linear_facts.v
 lang/linear_sem.v
 lang/low_memory.v
-lang/lowering_lemmas.v
 lang/memory_example.v
 lang/memory_model.v
 lang/one_varmap.v
 lang/psem.v
-lang/psem_defs.v
 lang/psem_core.v
+lang/psem_defs.v
+lang/psem_facts.v
 lang/psem_of_sem_proof.v
 lang/pseudo_operator.v
-lang/psem_facts.v
 lang/relational_logic.v
 lang/sem_one_varmap.v
-lang/sem_op_typed.v
 lang/sem_one_varmap_facts.v
+lang/sem_op_typed.v
 lang/sem_params.v
 lang/sem_type.v
 lang/sha256.v
 lang/shift_kind.v
-lang/sopn.v
 lang/slh_ops.v
+lang/sopn.v
 lang/stack_zero_strategy.v
 lang/strings.v
 lang/syscall.v
@@ -193,3 +191,5 @@ lang/waes.v
 lang/warray_.v
 lang/word.v
 lang/wsize.v
+ssrmisc/oseq.v
+ssrmisc/seq_extra.v

proofs/arch/_CoqProject

@@ -0,0 +1,23 @@
+-R ../_build/default/common common
+-R ../_build/default/itrees itrees
+-R ../_build/default/lang lang
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+
+-R ../_build/default/arch arch
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"

proofs/arch/arch_decl.v

@@ -7,23 +7,23 @@ From Coq Require Import
   Relation_Operators
   Utf8.
 
-Require Import
+From ssrmisc Require Import oseq.
+From lang Require Import
   global
   label
   memory_model
-  oseq
   sem_type
   strings
   syscall
   utils
   expr
   word.
 
-Require Import
+From lang Require Import
   sopn
   flag_combination
-  shift_kind
-  arm_expand_imm.
+  shift_kind.
+Require Import arm_expand_imm.
 
 (* -------------------------------------------------------------------- *)
 (* String representation of architecture components.