Almost at a checkpoint with the control flow and its theory compiling

src/Makefile

@@ -20,7 +20,7 @@ MLDIR = ml
 EXTRACTDIR = ml/extracted
 
 COQINCLUDES=$(foreach d, $(COQDIR), -R $(d) Vellvm) -R $(EXTRACTDIR) Extract
-COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
+COQC="$(COQBIN)coqc" -time-file "./profiling" -q $(COQINCLUDES) $(COQCOPTS)
 COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
 COQEXEC="$(COQBIN)coqtop" -q -w none $(COQINCLUDES) -batch -load-vernac-source
 COQMAKEFILE="$(COQBIN)coq_makefile"

src/_CoqProject

@@ -12,68 +12,28 @@
 ./coq/Analysis/Iteration.v
 ./coq/Analysis/Kildall.v
 ./coq/Analysis/ssa.v
-./coq/Handlers/Concretization.v
-./coq/Handlers/Global.v
-./coq/Handlers/Handlers.v
-./coq/Handlers/Intrinsics.v
-./coq/Handlers/Local.v
-./coq/Handlers/MemPropT.v
-./coq/Handlers/MemoryInterpreters.v
-./coq/Handlers/MemoryModel.v
-./coq/Handlers/MemoryModelImplementation.v
-./coq/Handlers/MemoryModules/FiniteAddresses.v
-./coq/Handlers/MemoryModules/FiniteExecPrimitives.v
-./coq/Handlers/MemoryModules/FiniteIntptr.v
-./coq/Handlers/MemoryModules/FiniteSizeof.v
-./coq/Handlers/MemoryModules/FiniteSpecPrimitives.v
-./coq/Handlers/MemoryModules/InfiniteAddresses.v
-./coq/Handlers/MemoryModules/Within.v
-./coq/Handlers/OOM.v
-./coq/Handlers/Pick.v
-./coq/Handlers/SerializationTheory.v
-./coq/Handlers/Stack.v
-./coq/Handlers/UndefinedBehaviour.v
 ./coq/Numeric/Archi.v
 ./coq/Numeric/Coqlib.v
 ./coq/Numeric/Floats.v
 ./coq/Numeric/IEEE754_extra.v
 ./coq/Numeric/Integers.v
 ./coq/Numeric/Zbits.v
-./coq/QC/GenAST.v
-./coq/QC/GenAlive2.v
-./coq/QC/Generators.v
 ./coq/QC/ReprAST.v
 ./coq/QC/ShowAST.v
 ./coq/QC/Utils.v
 ./coq/QC/DList.v
 ./coq/Semantics.v
-./coq/Semantics/ConcretizationParams.v
 ./coq/Semantics/Denotation.v
 ./coq/Semantics/DynamicValues.v
 ./coq/Semantics/GepM.v
+./coq/Semantics/Memory/DvalueBytes.v
 ./coq/Semantics/StoreId.v
-./coq/Semantics/InfiniteToFinite/Conversions/BaseConversions.v
-./coq/Semantics/InfiniteToFinite/Conversions/DvalueConversions.v
-./coq/Semantics/InfiniteToFinite/Conversions/EventConversions.v
-./coq/Semantics/InfiniteToFinite/Conversions/TreeConversions.v
-./coq/Semantics/InfiniteToFinite/R2Injective.v
-./coq/Semantics/InterpretationStack.v
 ./coq/Semantics/IntrinsicsDefinitions.v
 ./coq/Semantics/ItreeRaiseMReturns.v
 ./coq/Semantics/LLVMEvents.v
 ./coq/Semantics/LLVMParams.v
-./coq/Semantics/Lang.v
-./coq/Semantics/Memory/ErrSID.v
-./coq/Semantics/Memory/FiniteProvenance.v
-./coq/Semantics/Memory/MemBytes.v
-./coq/Semantics/Memory/DvalueBytes.v
-./coq/Semantics/Memory/Overlaps.v
 ./coq/Semantics/Memory/Sizeof.v
-./coq/Semantics/Memory/StoreId.v
 ./coq/Semantics/MemoryAddress.v
-./coq/Semantics/MemoryParams.v
-./coq/Semantics/RuttProps.v
-./coq/Semantics/TopLevel.v
 ./coq/Semantics/VellvmIntegers.v
 ./coq/Syntax.v
 ./coq/Syntax/AstLib.v
@@ -88,23 +48,10 @@
 ./coq/Syntax/TypToDtyp.v
 ./coq/Syntax/TypeUtil.v
 ./coq/Theory.v
-./coq/Theory/ContainsUB.v
-./coq/Theory/ContainsUBExtra.v
-./coq/Theory/ContainsUBOriginal.v
 ./coq/Theory/DenotationTheory.v
-./coq/Theory/ExpLemmas.v
-./coq/Theory/InstrLemmas.v
-./coq/Theory/InterpreterCFG.v
-./coq/Theory/InterpreterMCFG.v
-./coq/Theory/LocalFrame.v
-./coq/Theory/OOMRefinementExamples.v
-./coq/Theory/Refinement.v
-./coq/Theory/StatePredicates.v
 ./coq/Theory/SymbolicInterpreter.v
-./coq/Theory/TopLevelRefinements.v
 ./coq/Transformations/BlockFusion.v
 ./coq/Transformations/DeadCodeElimination.v
-./coq/Transformations/EquivExpr.v
 ./coq/Transformations/Peephole.v
 ./coq/Transformations/Transform.v
 ./coq/Utilities.v

src/backfile

@@ -0,0 +1,55 @@
+./coq/QC/GenAST.v
+./coq/QC/GenAlive2.v
+./coq/QC/Generators.v
+./coq/Handlers/Concretization.v
+./coq/Handlers/Global.v
+./coq/Handlers/Handlers.v
+./coq/Handlers/Intrinsics.v
+./coq/Handlers/Local.v
+./coq/Handlers/MemPropT.v
+./coq/Handlers/MemoryInterpreters.v
+./coq/Handlers/MemoryModel.v
+./coq/Handlers/MemoryModelImplementation.v
+./coq/Handlers/MemoryModules/FiniteAddresses.v
+./coq/Handlers/MemoryModules/FiniteExecPrimitives.v
+./coq/Handlers/MemoryModules/FiniteIntptr.v
+./coq/Handlers/MemoryModules/FiniteSizeof.v
+./coq/Handlers/MemoryModules/FiniteSpecPrimitives.v
+./coq/Handlers/MemoryModules/InfiniteAddresses.v
+./coq/Handlers/MemoryModules/Within.v
+./coq/Handlers/OOM.v
+./coq/Handlers/Pick.v
+./coq/Handlers/SerializationTheory.v
+./coq/Handlers/Stack.v
+./coq/Handlers/UndefinedBehaviour.v
+./coq/Semantics/InfiniteToFinite/Conversions/BaseConversions.v
+./coq/Semantics/InfiniteToFinite/Conversions/DvalueConversions.v
+./coq/Semantics/InfiniteToFinite/Conversions/EventConversions.v
+./coq/Semantics/InfiniteToFinite/Conversions/TreeConversions.v
+./coq/Semantics/InfiniteToFinite/R2Injective.v
+./coq/Semantics/InterpretationStack.v
+./coq/Semantics/Memory/ErrSID.v
+./coq/Semantics/Memory/FiniteProvenance.v
+./coq/Semantics/Memory/Overlaps.v
+./coq/Semantics/Memory/StoreId.v
+./coq/Semantics/Memory/MemBytes.v
+./coq/Semantics/ConcretizationParams.v
+./coq/Semantics/MemoryParams.v
+../coq/Semantics/Lang.v
+./coq/Semantics/RuttProps.v
+./coq/Semantics/TopLevel.v
+./coq/Theory/ContainsUB.v
+./coq/Theory/ContainsUBExtra.v
+./coq/Theory/ContainsUBOriginal.v
+./coq/Theory/ExpLemmas.v
+./coq/Theory/InstrLemmas.v
+./coq/Theory/InterpreterCFG.v
+./coq/Theory/InterpreterMCFG.v
+./coq/Theory/LocalFrame.v
+./coq/Theory/OOMRefinementExamples.v
+./coq/Theory/Refinement.v
+./coq/Theory/StatePredicates.v
+./coq/Theory/TopLevelRefinements.v
+./coq/Transformations/EquivExpr.v
+
+

src/coq/Analysis/Dom.v

@@ -1,12 +1,11 @@
 (** Reasoning about dominators in a graph. *)
+Set Warnings "-intuition-auto-with-star".
 
 Require Import List Equalities Orders RelationClasses Lia.
 Require Import FSets.
 
 Import ListNotations.
 
-
-
 Module Type LATTICE.
   Include EqLe'.
 

src/coq/Analysis/ssa.v

@@ -6,52 +6,53 @@ From Vellvm Require Import
      Syntax.Scope
      Analysis.Dom.
 (* end hide *)
+From stdpp Require Import fin_maps.
 
-  Lemma instr_id_eq_dec : forall (x y : instr_id), {x = y} + {x <> y}.
-  Proof.
-    intros. destruct (Eqv.eqv_dec_p x y); auto.
-  Qed.
+Lemma instr_id_eq_dec : forall (x y : instr_id), {x = y} + {x <> y}.
+Proof.
+  intros. repeat decide equality.
+Qed.
 
-  Definition def_sites_phis (phis : list (local_id * phi dtyp)) : list instr_id :=
-    List.map (fun '(x,_) => IId x) phis.
+Definition def_sites_phis (phis : list (local_id * phi dtyp)) : list instr_id :=
+  List.map (fun '(x,_) => IId x) phis.
 
-  Definition pc : Type := block_id * option (nat * instr_id).
+Definition pc : Type := block_id * option (nat * instr_id).
 
-  Lemma pc_eq_dec : forall (x y : pc), {x = y} + {x <> y}.
-  Proof.
-    repeat decide equality.
-  Qed.
+Lemma pc_eq_dec : forall (x y : pc), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Qed.
 
-  Definition opt_succ (mn : option (nat * instr_id)) : nat :=
-    match mn with | Some (n,_) => S n | None => 0 end.
+Definition opt_succ (mn : option (nat * instr_id)) : nat :=
+  match mn with | Some (n,_) => S n | None => 0 end.
 
-  Definition succ_instr (c : cfg dtyp) (v v' : pc) : Prop :=
-    let '(bid,mx) := v in
-    match find_block c.(blks) bid with
-    | Some bk =>
+Definition succ_instr (c : cfg dtyp) (v v' : pc) : Prop :=
+  let '(bid,mx) := v in
+  match c.(blks) !! bid with
+  | Some bk =>
       match List.nth_error
               (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) (opt_succ mx) with
-      | None => exists bid', List.In bid' (successors bk) /\ v' = (bid',None)
+      | None => exists bid', bid' ∈ (successors bk) /\ v' = (bid',None)
       | Some iid => v' = (bid, Some (opt_succ mx, iid))
       end
-    | None => False
-    end.
+  | None => False
+  end.
 
-  Definition mem_instr (c : cfg dtyp) (p : pc) : Prop :=
-    let '(bid,mx) := p in
-    match find_block c.(blks) bid with
-    | Some bk =>
+Definition mem_instr (c : cfg dtyp) (p : pc) : Prop :=
+  let '(bid,mx) := p in
+  match c.(blks) !! bid with
+  | Some bk =>
       match mx with
       | None => True
       | Some (offset,x) =>
-        match List.nth_error
-                (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) offset with
-        | None => False
-        | Some iid => x = iid
-        end
+          match List.nth_error
+                  (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) offset with
+          | None => False
+          | Some iid => x = iid
+          end
       end
-    | None => False
-    end.
+  | None => False
+  end.
 
 (**  ------------------------------------------------------------------------- *)
 (** * GRAPH instance for dominance calculation *)

src/coq/Numeric/Floats.v

@@ -15,6 +15,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Set Warnings "-intuition-auto-with-star".
+
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
 Require Import Psatz.

src/coq/Numeric/IEEE754_extra.v

@@ -431,7 +431,7 @@ Proof.
     apply integer_representable_2p. auto.
     apply (Zpower_gt_0 radix2).
     lia.
-- assert (IZR x <> 0%R) by (apply (IZR_neq _ _ n)).
+- assert (IZR x <> 0%R) by (apply (eq_IZR_contrapositive _ _ n)).
   destruct (BofZ_finite x H) as (A & B & C).
   destruct (BofZ_representable (2^p)) as (D & E & F).
     apply integer_representable_2p. auto.
@@ -1036,7 +1036,7 @@ Proof with (try discriminate).
   rewrite <- ! bpow_plus.
   replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; lia).
   rewrite bpow_opp. unfold cond_Ropp; destruct s; auto.
-  rewrite Ropp_inv_permute. auto. apply Rgt_not_eq. apply bpow_gt_0.
+  rewrite Rinv_opp. auto.
   split. simpl. apply F2R_neq_0. destruct s; simpl in H; discriminate.
   auto.
 Qed.

src/coq/Numeric/Zbits.v

@@ -13,6 +13,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Set Warnings "-intuition-auto-with-star".
+
 (** Additional operations and proofs about binary integers,
     on top of the ZArith standard library. *)
 

src/coq/QC/GenAST.v

@@ -10,8 +10,6 @@
 
     See vellvm-quickchick-overview.org in the root of the project for
     more details. *)
-Require Import Ceres.Ceres.
-
 From Vellvm Require Import LLVMAst Utilities AstLib Syntax.CFG Syntax.TypeUtil Syntax.TypToDtyp DynamicTypes Semantics.TopLevel QC.Utils QC.Generators Handlers.Handlers DList.
 Require Import Integers.
 

src/coq/QC/ReprAST.v

@@ -7,7 +7,7 @@
     QuickChick. It may be worthwhile to serialize a counterexample
     into a format that it can be imported into Coq for debugging.
 *)
-
+From stdpp Require Import gmap.
 From Vellvm Require Import LLVMAst ShowAST Utilities DynamicTypes.
 
 
@@ -35,6 +35,18 @@ Section ReprInstances.
       repr l := ("[" ++ contents repr l ++ "]")%string
     }.
 
+  #[global]
+   Instance reprProd (A B : Type) `{Repr A, Repr B} : Repr (A * B) :=
+    {
+      repr '(a,b) := ("(" ++ repr a ++ "," ++ repr b ++ ")")%string
+    }.
+
+  #[global]
+   Instance reprGmap (K V : Type) `{EqDecision K, Countable K, Repr K, Repr V} : Repr (gmap K V) :=
+    {
+      repr m := repr (A := list (K * V)) (map_to_list m)
+    }.
+
   #[global]
    Instance reprInt : Repr LLVMAst.int :=
     {

src/coq/QC/ShowAST.v

@@ -18,7 +18,7 @@ Import DList.
 From Coq Require Import
      ZArith String Bool.Bool Numbers.HexadecimalString
      Strings.Ascii.
-From QuickChick Require Import Show.
+From QuickChick Require Export Show.
 (* Import QcDefaultNotation. Open Scope qc_scope. *)
 Set Warnings "-extraction-opaque-accessed,-extraction".
 
@@ -142,6 +142,9 @@ Section ShowInstances.
        | DTYPE_Vector sz t          => "Vector"
        end.
 
+  #[global] Instance showDtyp : Show dtyp :=
+    {| show := show_dtyp |}.
+
   Definition show_linkage (l : linkage) : string :=
     match l with
     | LINKAGE_Private => "private "
@@ -707,7 +710,7 @@ tes on cstring on LLVMAst.v *)
     := {| dshow p :=
          let '(Phi t phis) := p in
          DList_join [string_to_DString "phi " ; dshow t ; string_to_DString " "] @@
-           concat_DString (string_to_DString ", ") (map show_phi_block phis)
+           concat_DString (string_to_DString ", ") (map show_phi_block (fin_maps.map_to_list phis))
        |}.
 
   Definition show_opt_prefix {A} `{Show A} (prefix : string) (ma : option A) : string

src/coq/Semantics.v

@@ -8,9 +8,9 @@
  *)
 
 From Vellvm Require Export
-     Handlers.Handlers
+     (* Handlers.Handlers *)
      Semantics.Denotation
-     Semantics.TopLevel
+     (* Semantics.TopLevel *)
      Semantics.DynamicValues
-     Semantics.InterpretationStack
+     (* Semantics.InterpretationStack *)
      Semantics.LLVMEvents.

src/coq/Semantics/ConcretizationParams.v

@@ -1,8 +1,7 @@
 From Vellvm Require Import
      Semantics.LLVMParams
      Semantics.MemoryParams
-     Semantics.Memory.MemBytes
-     Handlers.Concretization.
+     Semantics.Memory.MemBytes.
 
 Module Type ConcretizationParams (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP.ADDR LP.IP LP.SIZEOF LP.Events MP.BYTE_IMPL).
   Module CONCBASE := Concretization.MakeBase LP MP Byte.