Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2582 r2588  
    666666qed.
    667667
     668lemma zero_ext_same_size : ∀n,v. zero_ext n n v = v.
     669#n #v whd in match (zero_ext ???); >nat_compare_eq @refl
     670qed.
     671
    668672axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
    669673
    670674axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
     675
     676(* notice that we restrict source and target sizes to be ≠ 0 *)
     677axiom zero_ext_one : ∀sz1,sz2. zero_ext (bitsize_of_intsize sz1) (bitsize_of_intsize sz2) (repr sz1 1) = (repr sz2 1).
    671678
    672679axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
     
    24352442qed.
    24362443
     2444(* --------------------------------------------------------------------------- *)
     2445(* Inversion principles for binary operations *)
     2446(* --------------------------------------------------------------------------- *)
     2447
     2448lemma sem_add_ip_inversion :
     2449  ∀sz,sg,ty',optlen.
     2450  ∀v1,v2,res.
     2451  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
     2452  ∃sz',i. v1 = Vint sz' i ∧
     2453      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2454       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2455#tsz #tsg #ty' * [ | #n ]
     2456*
     2457[ | #sz' #i' | | #p'
     2458| | #sz' #i' | | #p' ]
     2459#v2 #res
     2460whd in ⊢ ((??%?) → ?);
     2461#H destruct
     2462cases v2 in H;
     2463[ | #sz2' #i2' | | #p2'
     2464| | #sz2' #i2' | | #p2' ] normalize nodelta
     2465#H destruct
     2466[ 1,3:
     2467  lapply H -H
     2468  @(eq_bv_elim … i' (zero ?)) normalize nodelta
     2469  #Hi #Heq destruct (Heq)
     2470  %{sz'} %{(zero ?)} @conj destruct try @refl
     2471  %2 @conj try @conj try @refl
     2472| *: %{sz'} %{i'} @conj try @refl
     2473  %1 %{p2'} @conj try @refl
     2474] qed.
     2475
     2476(* symmetric of the upper one *)
     2477lemma sem_add_pi_inversion :
     2478  ∀sz,sg,ty',optlen.
     2479  ∀v1,v2,res.
     2480  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
     2481  ∃sz',i. v2 = Vint sz' i ∧
     2482      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2483       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2484#tsz #tsg #ty' * [ | #n ]
     2485*
     2486[ | #sz' #i' | | #p'
     2487| | #sz' #i' | | #p' ]
     2488#v2 #res
     2489whd in ⊢ ((??%?) → ?);
     2490#H destruct
     2491cases v2 in H; normalize nodelta
     2492[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
     2493#H destruct
     2494[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
     2495  %{p'} @conj try @refl
     2496| *: lapply H -H
     2497  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
     2498  #Hi #Heq destruct (Heq)
     2499  %{sz2'} %{(zero ?)} @conj destruct try @refl
     2500  %2 @conj try @conj try @refl
     2501] qed.
     2502
     2503(* Know that addition on integers gives an integer. Notice that there is no correlation
     2504   between the size in the types and the size of the integer values. *)
     2505lemma sem_add_ii_inversion :
     2506  ∀sz,sg.
     2507  ∀v1,v2,res.
     2508  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2509  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2510              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
     2511#sz #sg
     2512*
     2513[ | #sz' #i' | | #p' ]
     2514#v2 #res
     2515whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
     2516cases sz cases sg normalize nodelta
     2517#H destruct
     2518cases v2 in H; normalize nodelta
     2519#H1 destruct
     2520#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2521cases sz' in i'; #i' 
     2522whd in match (intsize_eq_elim ???????);
     2523cases H1 in H2; #j' normalize nodelta
     2524#Heq destruct (Heq)
     2525%{i'} %{j'} @conj try @conj try @conj try @refl
     2526qed.
     2527
     2528lemma sem_sub_pp_inversion :
     2529  ∀ty1,ty2,n1,n2,target.
     2530  ∀v1,v2,res.
     2531  sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) target = Some ? res →
     2532  ∃sz,sg.
     2533    target = Tint sz sg ∧
     2534    ((∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
     2535             division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
     2536             res = Vint sz (zero_ext ?? i)) ∨
     2537     (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint sz (zero ?))).
     2538#ty1 #ty2 #n1 #n2 #target
     2539cut (classify_sub (ptr_type ty1 n1) (ptr_type ty2 n2) =
     2540     sub_case_pp n1 n2 ty1 ty2)
     2541[ cases n1 cases n2     
     2542  [ | #n1 | #n2 | #n2 #n1 ] try @refl ]
     2543#Hclassify
     2544*
     2545[ | #sz #i | | #p ]
     2546#v2 #res
     2547whd in ⊢ ((??%?) → ?); normalize nodelta
     2548#H1 destruct
     2549lapply H1 -H1
     2550>Hclassify normalize nodelta
     2551[ 1,2: #H destruct ]
     2552cases v2 normalize nodelta
     2553[ | #sz' #i' | | #p'
     2554| | #sz' #i' | | #p' ]
     2555#H2 destruct
     2556cases target in H2;
     2557[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
     2558| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     2559normalize nodelta
     2560#H destruct
     2561[ 2,4,5,6,7,8,9:
     2562  cases (eq_block (pblock p) (pblock p')) in H;
     2563  normalize nodelta #H destruct
     2564  cases (eqb (sizeof ty1) O) in H;
     2565  normalize nodelta #H destruct ]
     2566%{sz} %{sg} @conj try @refl
     2567try /4 by or_introl, or_intror, conj, refl/
     2568cases (if_opt_inversion ???? H)
     2569#Hblocks_eq -H
     2570@(eqb_elim … (sizeof ty1) 0) normalize nodelta
     2571[ #Heq_sizeof #Habsurd destruct ]
     2572#_ #Hdiv
     2573%1 %{p} %{p'}
     2574cases (division_u ???) in Hdiv; normalize nodelta
     2575[ #Habsurd destruct ] #i #Heq destruct
     2576%{i} try @conj try @conj try @conj try @conj try @refl
     2577try @(eq_block_to_refl … Hblocks_eq)
     2578qed.
     2579
     2580lemma sem_sub_pi_inversion :
     2581  ∀sz,sg,ty',optlen,target.
     2582  ∀v1,v2,res.
     2583  sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) target = Some ? res →
     2584  ∃sz',i. v2 = Vint sz' i ∧
     2585      ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
     2586       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     2587#tsz #tsg #ty' * [ | #n ] #target
     2588*
     2589[ | #sz' #i' | | #p'
     2590| | #sz' #i' | | #p' ]
     2591#v2 #res
     2592whd in ⊢ ((??%?) → ?);
     2593#H destruct
     2594cases v2 in H; normalize nodelta
     2595[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
     2596#H destruct
     2597[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
     2598  %{p'} @conj try @refl
     2599| *: lapply H -H
     2600  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
     2601  #Hi #Heq destruct (Heq)
     2602  %{sz2'} %{(zero ?)} @conj destruct try @refl
     2603  %2 @conj try @conj try @refl
     2604] qed.
     2605
     2606lemma sem_sub_ii_inversion :
     2607  ∀sz,sg,ty.
     2608  ∀v1,v2,res.
     2609  sem_sub v1 (Tint sz sg) v2 (Tint sz sg) ty = Some ? res →
     2610  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2611              res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
     2612#sz #sg #ty *             
     2613[ | #sz' #i' | | #p' ]
     2614#v2 #res
     2615whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
     2616cases sz cases sg normalize nodelta
     2617#H destruct
     2618cases v2 in H; normalize nodelta
     2619#H1 destruct
     2620#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2621cases sz' in i'; #i' 
     2622whd in match (intsize_eq_elim ???????);
     2623cases H1 in H2; #j' normalize nodelta
     2624#Heq destruct (Heq)
     2625%{i'} %{j'} @conj try @conj try @conj try @refl
     2626qed.
     2627
     2628
     2629lemma sem_mul_inversion :
     2630  ∀sz,sg.
     2631  ∀v1,v2,res.
     2632  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2633  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2634              res = Vint sz' (short_multiplication ? i1 i2).
     2635#sz #sg *
     2636[ | #sz' #i' | | #p' ]
     2637#v2 #res
     2638whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2639cases sz cases sg normalize nodelta
     2640#H destruct
     2641cases v2 in H; normalize nodelta
     2642#H1 destruct
     2643#H2 destruct #Heq %{sz'} lapply Heq -Heq
     2644cases sz' in i'; #i' 
     2645whd in match (intsize_eq_elim ???????);
     2646cases H1 in H2; #j' normalize nodelta
     2647#Heq destruct (Heq)
     2648%{i'} %{j'} @conj try @conj try @conj try @refl
     2649qed.
     2650
     2651
     2652lemma sem_div_inversion_s :
     2653  ∀sz.
     2654  ∀v1,v2,res.
     2655  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     2656  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2657              match division_s ? i1 i2 with
     2658              [ Some q ⇒  res =  (Vint sz' q)
     2659              | None ⇒ False ].
     2660#sz *
     2661[ | #sz' #i' | | #p' ]
     2662#v2 #res
     2663whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2664>type_eq_dec_true normalize nodelta
     2665#H destruct
     2666cases v2 in H; normalize nodelta
     2667[ | #sz2' #i2' | | #p2' ]
     2668#Heq destruct
     2669%{sz'}
     2670lapply Heq -Heq
     2671cases sz' in i'; #i' 
     2672whd in match (intsize_eq_elim ???????);
     2673cases sz2' in i2'; #i2' normalize nodelta
     2674whd in match (option_map ????); #Hdiv destruct
     2675%{i'} %{i2'} @conj try @conj try @conj try @refl
     2676cases (division_s ???) in Hdiv;
     2677[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2678qed.
     2679
     2680lemma sem_div_inversion_u :
     2681  ∀sz.
     2682  ∀v1,v2,res.
     2683  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     2684  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2685              match division_u ? i1 i2 with
     2686              [ Some q ⇒  res =  (Vint sz' q)
     2687              | None ⇒ False ].
     2688#sz *
     2689[ | #sz' #i' | | #p' ]
     2690#v2 #res
     2691whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2692>type_eq_dec_true normalize nodelta
     2693#H destruct
     2694cases v2 in H; normalize nodelta
     2695[ | #sz2' #i2' | | #p2' ]
     2696#Heq destruct
     2697%{sz'}
     2698lapply Heq -Heq
     2699cases sz' in i'; #i' 
     2700whd in match (intsize_eq_elim ???????);
     2701cases sz2' in i2'; #i2' normalize nodelta
     2702whd in match (option_map ????); #Hdiv destruct
     2703%{i'} %{i2'} @conj try @conj try @conj try @refl
     2704cases (division_u ???) in Hdiv;
     2705[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2706qed.
     2707
     2708lemma sem_mod_inversion_s :
     2709  ∀sz.
     2710  ∀v1,v2,res.
     2711  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     2712  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2713              match modulus_s ? i1 i2 with
     2714              [ Some q ⇒  res =  (Vint sz' q)
     2715              | None ⇒ False ].
     2716#sz *
     2717[ | #sz' #i' | | #p' ]
     2718#v2 #res
     2719whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2720>type_eq_dec_true normalize nodelta
     2721#H destruct
     2722cases v2 in H; normalize nodelta
     2723[ | #sz2' #i2' | | #p2' ]
     2724#Heq destruct
     2725%{sz'}
     2726lapply Heq -Heq
     2727cases sz' in i'; #i' 
     2728whd in match (intsize_eq_elim ???????);
     2729cases sz2' in i2'; #i2' normalize nodelta
     2730whd in match (option_map ????); #Hdiv destruct
     2731%{i'} %{i2'} @conj try @conj try @conj try @refl
     2732cases (modulus_s ???) in Hdiv;
     2733[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2734qed.
     2735
     2736lemma sem_mod_inversion_u :
     2737  ∀sz.
     2738  ∀v1,v2,res.
     2739  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     2740  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2741              match modulus_u ? i1 i2 with
     2742              [ Some q ⇒  res =  (Vint sz' q)
     2743              | None ⇒ False ].
     2744#sz *
     2745[ | #sz' #i' | | #p' ]
     2746#v2 #res
     2747whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     2748>type_eq_dec_true normalize nodelta
     2749#H destruct
     2750cases v2 in H; normalize nodelta
     2751[ | #sz2' #i2' | | #p2' ]
     2752#Heq destruct
     2753%{sz'}
     2754lapply Heq -Heq
     2755cases sz' in i'; #i' 
     2756whd in match (intsize_eq_elim ???????);
     2757cases sz2' in i2'; #i2' normalize nodelta
     2758whd in match (option_map ????); #Hdiv destruct
     2759%{i'} %{i2'} @conj try @conj try @conj try @refl
     2760cases (modulus_u ???) in Hdiv;
     2761[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     2762qed.
     2763
     2764lemma sem_and_inversion :
     2765  ∀v1,v2,res.
     2766  sem_and v1 v2 = Some ? res →
     2767  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2768              res = Vint sz' (conjunction_bv ? i1 i2).
     2769*
     2770[ | #sz' #i' | | #p' ]
     2771#v2 #res
     2772whd in ⊢ ((??%?) → ?);
     2773#H destruct
     2774cases v2 in H; normalize nodelta
     2775[ | #sz2' #i2' | | #p2' ]
     2776#Heq destruct
     2777%{sz'}
     2778lapply Heq -Heq
     2779cases sz' in i'; #i' 
     2780whd in match (intsize_eq_elim ???????);
     2781cases sz2' in i2'; #i2' normalize nodelta
     2782#H destruct
     2783%{i'} %{i2'} @conj try @conj try @conj try @refl
     2784qed.
     2785
     2786lemma sem_or_inversion :
     2787  ∀v1,v2,res.
     2788  sem_or v1 v2 = Some ? res →
     2789  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2790              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
     2791*
     2792[ | #sz' #i' | | #p' ]
     2793#v2 #res
     2794whd in ⊢ ((??%?) → ?);
     2795#H destruct
     2796cases v2 in H; normalize nodelta
     2797[ | #sz2' #i2' | | #p2' ]
     2798#Heq destruct
     2799%{sz'}
     2800lapply Heq -Heq
     2801cases sz' in i'; #i' 
     2802whd in match (intsize_eq_elim ???????);
     2803cases sz2' in i2'; #i2' normalize nodelta
     2804#H destruct
     2805%{i'} %{i2'} @conj try @conj try @conj try @refl
     2806qed.
     2807
     2808lemma sem_xor_inversion :
     2809  ∀v1,v2,res.
     2810  sem_xor v1 v2 = Some ? res →
     2811  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     2812              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
     2813*
     2814[ | #sz' #i' | | #p' ]
     2815#v2 #res
     2816whd in ⊢ ((??%?) → ?);
     2817#H destruct
     2818cases v2 in H; normalize nodelta
     2819[ | #sz2' #i2' | | #p2' ]
     2820#Heq destruct
     2821%{sz'}
     2822lapply Heq -Heq
     2823cases sz' in i'; #i' 
     2824whd in match (intsize_eq_elim ???????);
     2825cases sz2' in i2'; #i2' normalize nodelta
     2826#H destruct
     2827%{i'} %{i2'} @conj try @conj try @conj try @refl
     2828qed.
     2829
     2830lemma sem_shl_inversion :
     2831  ∀v1,v2,res.
     2832  sem_shl v1 v2 = Some ? res →
     2833  ∃sz1,sz2,i1,i2.
     2834              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     2835              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
     2836                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
     2837              lt_u (bitsize_of_intsize sz2) i2
     2838                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
     2839*
     2840[ | #sz' #i' | | #p' ]
     2841#v2 #res
     2842whd in ⊢ ((??%?) → ?);
     2843#H destruct
     2844cases v2 in H; normalize nodelta
     2845[ | #sz2' #i2' | | #p2' ]
     2846#Heq destruct
     2847%{sz'} %{sz2'}
     2848lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     2849%{i'} %{i2'}
     2850>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     2851qed.
     2852
     2853lemma sem_shr_inversion :
     2854  ∀v1,v2,sz,sg,res.
     2855  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     2856  ∃sz1,sz2,i1,i2.
     2857              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
     2858              lt_u (bitsize_of_intsize sz2) i2
     2859                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
     2860              match sg with
     2861              [ Signed ⇒
     2862                 res =
     2863                   (Vint sz1
     2864                    (shift_right bool (7+pred_size_intsize sz1*8)
     2865                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
     2866                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
     2867              | Unsigned ⇒
     2868                 res =
     2869                   (Vint sz1
     2870                    (shift_right bool (7+pred_size_intsize sz1*8)
     2871                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
     2872              ].
     2873*
     2874[ | #sz' #i' | | #p' ]
     2875#v2 #sz * #res
     2876whd in ⊢ ((??%?) → ?);
     2877whd in match (classify_aop ??);
     2878>type_eq_dec_true normalize nodelta
     2879#H destruct
     2880cases v2 in H; normalize nodelta
     2881[ | #sz2' #i2' | | #p2'
     2882| | #sz2' #i2' | | #p2' ]
     2883#Heq destruct
     2884%{sz'} %{sz2'}
     2885lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
     2886%{i'} %{i2'}
     2887>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
     2888qed.
     2889
     2890
     2891
     2892lemma sem_cmp_int_inversion :
     2893  ∀v1,v2,sz,sg,op,m,res.
     2894   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
     2895   ∃sz,i1,i2. v1 = Vint sz i1 ∧
     2896              v2 = Vint sz i2 ∧
     2897    match sg with
     2898    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
     2899    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
     2900    ].
     2901#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
     2902whd in ⊢ ((??%?) → ?);
     2903whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
     2904cases v1
     2905[ | #sz #i | | #p ] normalize nodelta
     2906#H destruct
     2907cases v2 in H;
     2908[ | #sz' #i' | | #p' ] normalize nodelta
     2909#H destruct lapply H -H
     2910cases sz in i; #i
     2911cases sz' in i'; #i' cases sg normalize nodelta
     2912whd in match (intsize_eq_elim ???????); #H destruct
     2913[ 1,2: %{I8}
     2914| 3,4: %{I16}
     2915| 5,6: %{I32} ] 
     2916%{i} %{i'} @conj try @conj try @refl
     2917qed.
     2918
     2919
     2920lemma sem_cmp_ptr_inversion :
     2921  ∀v1,v2,ty',n,op,m,res.
     2922   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
     2923   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
     2924                 valid_pointer m p1 = true ∧
     2925                 valid_pointer m p2 = true ∧
     2926                 (if eq_block (pblock p1) (pblock p2)
     2927                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
     2928                  else sem_cmp_mismatch op) = Some ? res) ∨
     2929   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
     2930   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
     2931   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
     2932* [ | #sz #i | | #p ] normalize nodelta
     2933#v2 #ty' #n #op
     2934* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
     2935whd in match (classify_cmp ??); cases n normalize nodelta
     2936[ 2,4,6,8: #array_len ]
     2937whd in match (ptr_type ty' ?);
     2938whd in match (if_type_eq ?????);
     2939>type_eq_dec_true normalize nodelta
     2940#H destruct
     2941cases v2 in H; normalize nodelta
     2942[ | #sz' #i' | | #p'
     2943| | #sz' #i' | | #p'
     2944| | #sz' #i' | | #p'
     2945| | #sz' #i' | | #p' ]
     2946#H destruct
     2947try /6 by or_introl, or_intror, ex_intro, conj/
     2948[ 1: %1 %1 %2 %{p} @conj try @conj //
     2949| 3: %1 %1 %2 %{p} @conj try @conj //
     2950| *: %1 %1 %1 %{p} %{p'}
     2951     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
     2952     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
     2953     try @conj try @conj try @conj try @conj try @conj try @refl try @H
     2954     destruct
     2955] qed.
Note: See TracChangeset for help on using the changeset viewer.