Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalis

5 files changed, 57 insertions, 15 deletions

diff --git a/src/SoftwarePipelining/LICENSE b/src/SoftwarePipelining/LICENSE
new file mode 100644
index 0000000..e275fa0
--- /dev/null
+++ b/src/SoftwarePipelining/LICENSE
@@ -0,0 +1,19 @@
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index e9e058d..805dbda 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -220,6 +220,8 @@ Ltac liapp :=
 
 Ltac plia := solve [ unfold Ple in *; lia ].
 
+Ltac xomega := unfold Plt, Ple in *; zify; lia.
+
 Ltac crush := simplify; try discriminate; try congruence; try plia; liapp;
               try assumption; try (solve [auto]).
 
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 2403f40..13a4345 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -646,8 +646,8 @@ Section CORRECTNESS.
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
   Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
 
-  Lemma function_ptr_translated:
-    forall (b: Values.block) (f: RTL.fundef),
+  Lemma function_ptr_translated :
+    forall (b : Values.block) (f: RTL.fundef),
       Genv.find_funct_ptr ge b = Some f ->
       exists tf,
         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef prog f = Errors.OK tf.
@@ -2115,7 +2115,7 @@ Section CORRECTNESS.
            | [ _ : context[if ?x then _ else _] |- _ ] =>
              let EQ := fresh "EQ" in
              destruct x eqn:EQ; simpl in *
-           | [ H : ret _ _ = _  |- _ ] => invert H
+           | [ H : ret _ = _  |- _ ] => invert H
            | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
            end.
 
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index a2700a1..a5fa554 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -75,7 +75,7 @@ let pprint_binop l r =
 
 let unop = function
   | Vneg -> " - "
-  | Vnot -> " ! "
+  | Vnot -> " ~ "
 
 let register a =
   match PMap.find_opt a !name_map with
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 5e123a3..3fab464 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -183,23 +183,44 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
      | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
      | Pand p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (p1' ++ p2') _)
       | _, _ => None
       end
      | Por p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (mult p1' p2') _)
       | _, _ => None
       end
      | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
-     | _ => None
+     | Pnot (Pnot p') =>
+       match trans_pred n p' with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
+     | Pnot (Pand p1 p2) =>
+       match trans_pred n (Por (Pnot p1) (Pnot p2)) with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
+     | Pnot (Por p1 p2) =>
+       match trans_pred n (Pand (Pnot p1) (Pnot p2)) with
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
+       | None => None
+       end
      end
    end); split; intros; simpl in *; auto.
   - inv H. inv H0; auto.
-  - admit.
-  - admit.
+  - split; auto. destruct (a p') eqn:?; crush.
+  - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto.
+    crush.
+  - rewrite negb_involutive in H. apply i in H. auto.
+  - rewrite negb_involutive. apply i; auto.
+  - rewrite negb_andb in H. apply i. auto.
+  - rewrite negb_andb. apply i. auto.
+  - rewrite negb_orb in H. apply i. auto.
+  - rewrite negb_orb. apply i. auto.
   - apply satFormula_concat.
     apply andb_prop in H. inv H. apply i in H0. auto.
     apply andb_prop in H. inv H. apply i0 in H1. auto.
@@ -211,16 +232,16 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
   - apply orb_true_intro.
     apply satFormula_mult2 in H. inv H. apply i in H0. auto.
     apply i0 in H0. auto.
-Abort.
+Qed.
 
-(*Definition sat_pred (bound: nat) (p: pred_op) :
+Definition sat_pred (bound: nat) (p: pred_op) :
   option ({al : alist | sat_predicate p (interp_alist al) = true}
           + {forall a : asgn, sat_predicate p a = false}).
   refine
   ( match trans_pred bound p with
-    | Some (exist fm _) =>
+    | Some (exist _ fm _) =>
       match boundedSat bound fm with
-      | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
+      | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _))
       | Some (inright _) => Some (inright _)
       | None => None
       end
@@ -234,7 +255,7 @@ Qed.
 
 Definition sat_pred_simple (bound: nat) (p: pred_op) :=
   match sat_pred bound p with
-  | Some (inleft (exist al _)) => Some (Some al)
+  | Some (inleft (exist _ al _)) => Some (Some al)
   | Some (inright _) => Some None
   | None => None
   end.
@@ -243,7 +264,7 @@ Definition sat_pred_temp (bound: nat) (p: pred_op) :=
   match trans_pred_temp bound p with
   | Some fm => boundedSatSimple bound fm
   | None => None
-  end.*)
+  end.
 
 Inductive instr : Type :=
 | RBnop : instr