Merge pull request #79 from aqjune-aws/tablelookup-updatesplit

Add two ARM instructions and add print_log flags

arm/proofs/arm.ml

@@ -7,6 +7,8 @@
 (* Simplified model of aarch64 (64-bit ARM) semantics.                       *)
 (* ========================================================================= *)
 
+let arm_print_log = ref false;;
+
 (* ------------------------------------------------------------------------- *)
 (* Stating assumptions about instruction decoding. For ARM we                *)
 (* currently go all the way to the semantics in one jump, no asm.            *)
@@ -416,13 +418,25 @@ let DISCARD_STATE_TAC s =
 
 let DISCARD_OLDSTATE_TAC s =
   let v = mk_var(s,`:armstate`) in
-  let rec badread okvs tm =
+  let rec unbound_statevars_of_read bound_svars tm =
     match tm with
-      Comb(Comb(Const("read",_),cmp),s) -> not(mem s okvs)
-    | Comb(s,t) -> badread okvs s || badread okvs t
-    | Abs(v,t) -> badread (v::okvs) t
-    | _ -> false in
-  DISCARD_ASSUMPTIONS_TAC(badread [v] o concl);;
+      Comb(Comb(Const("read",_),cmp),s) ->
+        if mem s bound_svars then [] else [s]
+    | Comb(a,b) -> union (unbound_statevars_of_read bound_svars a)
+                         (unbound_statevars_of_read bound_svars b)
+    | Abs(v,t) -> unbound_statevars_of_read (v::bound_svars) t
+    | _ -> [] in
+  DISCARD_ASSUMPTIONS_TAC(
+    fun thm ->
+      let us = unbound_statevars_of_read [] (concl thm) in
+      if us = [] || us = [v] then false
+      else if not(mem v us) then true
+      else
+        if !arm_print_log then
+          (Printf.printf
+            "Info: assumption `%s` is erased, but it might have contained useful information\n"
+            (string_of_term (concl thm)); true)
+        else true);;
 
 (* ------------------------------------------------------------------------- *)
 (* More convenient stepping tactics, optionally with accumulation.           *)

arm/proofs/decode.ml

@@ -268,9 +268,9 @@ let decode = new_definition `!w:int32. decode w =
       (Immediate_Offset (iword (ival imm7 * &(if x then 8 else 4)))))
 
   // SIMD ld,st operations
-  | [0b00:2; 0b111101:6; 0b11:2; imm12:12; Rn:5; Rt:5] ->
-    // LDR (immediate, SIMD&FP), Unsigned offset. Q registers only
-    SOME (arm_ldst_q T Rt (XREG_SP Rn) (Immediate_Offset (word (val imm12 * 16))))
+  | [0b00:2; 0b111101:6; 0b1:1; is_ld; imm12:12; Rn:5; Rt:5] ->
+    // LDR/STR (immediate, SIMD&FP), Unsigned offset, no writeback. Q registers only
+    SOME (arm_ldst_q is_ld Rt (XREG_SP Rn) (Immediate_Offset (word (val imm12 * 16))))
 
   // SIMD operations
   | [0:1; q; 0b001110:6; size:2; 1:1; Rm:5; 0b100001:6; Rn:5; Rd:5] ->
@@ -287,6 +287,10 @@ let decode = new_definition `!w:int32. decode w =
     // AND
     SOME (arm_AND_VEC (QREG' Rd) (QREG' Rn) (QREG' Rm) (if q then 128 else 64))
 
+  | [0:1; q; 0b101110101:9; Rm:5; 0b000111:6; Rn:5; Rd:5] ->
+    // BIT
+    SOME (arm_BIT (QREG' Rd) (QREG' Rn) (QREG' Rm) (if q then 128 else 64))
+
   | [0:1; q; 0b001110000:9; imm5:5; 0b000011:6; Rn:5; Rd:5] ->
     // DUP (general)
     if q /\ word_subword imm5 (0,4) = (word 0b1000:4 word) then
@@ -1082,15 +1086,16 @@ let dest_cons4 =
   let assert_byte n = function
   | Comb(Const("word",_),a) -> dest_numeral a = Int n
   | _ -> false in
-  fun n -> function
+  fun n t -> match t with
   | Comb(Comb(Const("CONS",_),a1), Comb(Comb(Const("CONS",_),a2),
       Comb(Comb(Const("CONS",_),a3), Comb(Comb(Const("CONS",_),a4),tm)))) when
     0 <= n && n <= 0xffffffff &&
     assert_byte (n land 0xff) a1 &&
     assert_byte ((n lsr 8) land 0xff) a2 &&
     assert_byte ((n lsr 16) land 0xff) a3 &&
     assert_byte ((n lsr 24) land 0xff) a4 -> tm
-  | _ -> failwith "dest_cons4";;
+  | _ -> failwith ("dest_cons4: 4-byte inst code " ^ string_of_int n ^
+                   " != first 4 bytes of " ^ string_of_term t);;
 
 (* Asserts that the input term is the given list of words, and returns it. *)
 let assert_word_list tm ls =

arm/proofs/instruction.ml

@@ -831,6 +831,18 @@ let arm_BICS = define
          CF := F ,,
          VF := F) s`;;
 
+let arm_BIT = define
+ `arm_BIT Rd Rn Rm datasize =
+    \s. let m = read Rm s
+        and n = read Rn s
+        and d = read Rd s in
+        let out:(128)word = word_or (word_and d (word_not m)) (word_and n m) in
+        if datasize = 128 then
+          (Rd := out) s
+        else
+          let out':(64)word = word_subword out (0,64) in
+          (Rd := word_zx out':(128)word) s`;;
+
 (*** As with x86, we have relative and absolute versions of branch & link ***)
 (*** The absolute one gives a natural way of handling linker-insertions.  ***)
 
@@ -1977,7 +1989,7 @@ let ARM_OPERATION_CLAUSES =
     (*** Alphabetically sorted, new alphabet appears in the next line ***)
       [arm_ADC; arm_ADCS_ALT; arm_ADD; arm_ADD_VEC_ALT; arm_ADDS_ALT; arm_ADR;
        arm_AND; arm_AND_VEC; arm_ANDS; arm_ASR; arm_ASRV;
-       arm_B; arm_BIC; arm_BICS; arm_BL; arm_BL_ABSOLUTE; arm_Bcond;
+       arm_B; arm_BIC; arm_BICS; arm_BIT; arm_BL; arm_BL_ABSOLUTE; arm_Bcond;
        arm_CBNZ_ALT; arm_CBZ_ALT; arm_CCMN; arm_CCMP; arm_CLZ; arm_CSEL;
        arm_CSINC; arm_CSINV; arm_CSNEG;
        arm_DUP_GEN;

arm/proofs/simulator.ml

@@ -162,6 +162,9 @@ let iclasses =
   (*** AND ***)
   "0x001110001xxxxx000111xxxxxxxxxx";
 
+  (*** BIT ***)
+  "0x101110101xxxxx000111xxxxxxxxxx";
+
   (*** DUP ***)
   "01001110000x1000000011xxxxxxxxxx"; (* DUP Vd.2d, xn *)
 

common/components.ml

@@ -27,6 +27,8 @@
 needs "Library/words.ml";;
 needs "common/overlap.ml";;
 
+let components_print_log = ref false;;
+
 (* ------------------------------------------------------------------------- *)
 (* Storing useful per-case theorems not true of a general component.         *)
 (* ------------------------------------------------------------------------- *)
@@ -2561,7 +2563,7 @@ let (NONOVERLAPPING_TAC:tactic) =
         with Failure _ ->
         try TAC_PROOF (g, SIMPLE_ARITH_TAC)
         with Failure _ ->
-          failwith ("NONOVERLAPPING_TAC: cannot prove " ^ (string_of_term t))
+          failwith ("NONOVERLAPPING_TAC: cannot prove `" ^ (string_of_term t) ^ "`")
         in
       cache := th::!cache; th) in
 
@@ -2910,7 +2912,10 @@ let (NONOVERLAPPING_TAC:tactic) =
                     else fail()) asl in
                 ACCEPT_TAC th gl
            with Failure _ -> NONOVERLAPPING_TAC gl)
-    | _ -> failwith "NONOVERLAPPING_TAC: inapplicable goal" in
+        | Comb(Comb(Const("orthogonal_components", _), p1), p2) when p1 = p2 ->
+          failwith "NONOVERLAPPING_TAC: orthogonal_components with identical operands"
+        | _ -> failwith ("NONOVERLAPPING_TAC: inapplicable goal: " ^
+                         (string_of_term w)) in
 
   OVERRIDDEN_NONOVERLAPPING_TAC;;
 
@@ -3064,8 +3069,17 @@ let STATE_UPDATE_NEW_RULE th =
 
 let ASSUMPTION_STATE_UPDATE_TAC =
   DISCH_THEN(fun uth ->
-        MP_TAC uth THEN
-        ASSUM_LIST(MAP_EVERY (TRY o STATE_UPDATE_TAC uth)));;
+    MP_TAC uth THEN
+    ASSUM_LIST(MAP_EVERY (fun th g ->
+      try STATE_UPDATE_TAC uth th g
+      with Failure s ->
+        if !components_print_log then
+          if s = "NONOVERLAPPING_TAC: orthogonal_components with identical operands"
+          then ALL_TAC g (* Exactly overwrites, e.g., orthogonal_components PC PC *)
+          else (Printf.printf
+            "Info: assumption `%s` is erased.\n    - Reason: %s\n"
+            (string_of_term (concl th)) s; ALL_TAC g)
+        else ALL_TAC g)));;
 
 (* ------------------------------------------------------------------------- *)
 (* Rule for "non-selfmodification" when supplied with std exec theorem       *)

common/relational.ml

@@ -342,6 +342,13 @@ let ASSIGNS_BYTES64 = prove
   CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN
   CONV_TAC NUM_REDUCE_CONV);;
 
+let ASSIGNS_BYTES128 = prove
+ (`!a. ASSIGNS (bytes128 a) = ASSIGNS(bytes(a,16))`,
+  GEN_TAC THEN REWRITE_TAC[bytes128] THEN
+  MATCH_MP_TAC ASSIGNS_BYTES_ASWORD THEN
+  CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN
+  CONV_TAC NUM_REDUCE_CONV);;
+
 let SUBSUMED_ASSIGNS_BYTES = prove
  (`!a1 (a2:int64) k1 k2.
         contained_modulo (2 EXP 64) (val a1,k1) (val a2,k2)
@@ -594,7 +601,8 @@ let UNDEFINED_VALUES = define
 let ASSIGNS_CANON_CONV =
   let byteconv =
     GEN_REWRITE_CONV TRY_CONV
-     [ASSIGNS_BYTES8; ASSIGNS_BYTES16; ASSIGNS_BYTES32; ASSIGNS_BYTES64] in
+     [ASSIGNS_BYTES8; ASSIGNS_BYTES16; ASSIGNS_BYTES32; ASSIGNS_BYTES64;
+      ASSIGNS_BYTES128] in
   fun tm ->
     match tm with
       Comb(Const("ASSIGNS",_),c) ->
@@ -1772,7 +1780,8 @@ let SUBSUMED_ASSIGNS_TAC =
   REPEAT(MATCH_MP_TAC SUBSUMED_ASSIGNS_SUBCOMPONENTS) THEN
   TRY(MATCH_ACCEPT_TAC SUBSUMED_ASSIGNS_SUBCOMPONENT) THEN
   GEN_REWRITE_TAC (BINOP_CONV o TRY_CONV)
-   [ASSIGNS_BYTES8; ASSIGNS_BYTES16; ASSIGNS_BYTES32; ASSIGNS_BYTES64] THEN
+   [ASSIGNS_BYTES8; ASSIGNS_BYTES16; ASSIGNS_BYTES32; ASSIGNS_BYTES64;
+    ASSIGNS_BYTES128] THEN
   MATCH_MP_TAC SUBSUMED_ASSIGNS_BYTES THEN CONTAINED_TAC;;
 
 (* ------------------------------------------------------------------------- *)