Merge branch 'master' into _lazy_type_normalization

project-everest · Oct 31, 2018 · 305f66e · 305f66e
2 parents f935ee1 + b17f1ed
commit 305f66e
Show file tree

Hide file tree

Showing 25 changed files with 125 additions and 75 deletions.
diff --git a/SConstruct b/SConstruct
@@ -733,7 +733,7 @@ def translate_vaf_file(options, source_vaf):
   types_include = ''
   types_include = f'-include {target}.types.vaf'
   env.Command(targets, [source_vaf, vale_exe],
-    f'{mono} {vale_exe} -fstarText -quickMods -typecheck {types_include} {opt_vale_includes}' +
+    f'{mono} {vale_exe} -fstarText -typecheck {types_include} {opt_vale_includes}' +
     f' -in {source_vaf} -out {target_fst} -outi {target_fsti}' +
     f' {vale_scons_args} {" ".join(vale_user_args)}')
   return targets

diff --git a/fstar/code/arch/x64/X64.Vale.Decls.fsti b/fstar/code/arch/x64/X64.Vale.Decls.fsti
@@ -6,6 +6,7 @@ module X64.Vale.Decls
 // because they refer to Semantics_s.
 // Regs_i and State_i are ok, because they do not refer to Semantics_s.
 
+open Defs_s
 open Prop_s
 open X64.Machine_s
 open X64.Vale.State
@@ -56,13 +57,15 @@ unfold let va_cmp = operand
 unfold let va_register = reg
 unfold let va_operand_xmm = xmm
 
+[@va_qattr] unfold let va_expand_state (s:state) : state = s
+
 (* Abbreviations *)
 unfold let get_reg (o:va_reg_operand) : reg = OReg?.r o
 
 (* Constructors *)
 val va_fuel_default : unit -> va_fuel
 [@va_qattr] unfold let va_op_operand_reg (r:reg) : va_operand = OReg r
-[@va_qattr] unfold let va_op_xmm_xmm(x:xmm) : va_operand_xmm = x
+[@va_qattr] unfold let va_op_xmm_xmm (x:xmm) : va_operand_xmm = x
 [@va_qattr] unfold let va_op_opr_reg (r:reg) : va_operand = OReg r
 [@va_qattr] unfold let va_op_opr64_reg (r:reg) : va_operand = OReg r
 [@va_qattr] unfold let va_const_operand (n:int) = OConst n

diff --git a/fstar/code/arch/x64/X64.Vale.InsBasic.vaf b/fstar/code/arch/x64/X64.Vale.InsBasic.vaf
@@ -8,6 +8,7 @@ include{:fstar}{:open} "X64.Vale.QuickCode"
 module X64.Vale.InsBasic
 
 #verbatim{:interface}
+open Defs_s
 open Types_s
 open Arch.Types
 open X64.Machine_s
@@ -61,20 +62,20 @@ operand_type dst_opr64:nat64 @ operand := reg_opr64;
 operand_type opr64:nat64 := dst_opr64 | const;
 
 // add {:typecheck false} attr because Type0 is not defined. (TODO: get rid of this)
-procedure{:quick exportOnly}{:typecheck false} AssertQuickType(ghost p:Type0) returns(ghost u:squash(p))
+procedure{:public}{:quick exportOnly}{:typecheck false} AssertQuickType(ghost p:Type0) returns(ghost u:squash(p))
     requires
         p;
 {
     u := tuple();
 }
 
-procedure{:instruction Ins(S.Mov64(dst,src))}{:quick exportOnly} Mov64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Mov64(dst,src))}{:quick exportOnly} Mov64(inout dst:dst_opr64, src:opr64)
     ensures
         dst == old(src);
 {
 }
 
-procedure{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     requires
@@ -84,7 +85,7 @@ procedure{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64(inout dst
 {
 }
 
-procedure{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64Wrap(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64Wrap(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -93,15 +94,15 @@ procedure{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly} Add64Wrap(inout
 {
 }
 
-procedure{:instruction Ins(S.AddLea64(dst, src1, src2))}{:quick exportOnly} AddLea64(out dst:dst_opr64, src1:opr64, src2:opr64)
+procedure{:public}{:instruction Ins(S.AddLea64(dst, src1, src2))}{:quick exportOnly} AddLea64(out dst:dst_opr64, src1:opr64, src2:opr64)
     requires
         src1 + src2 < pow2_64;
     ensures
         dst == old(src1) + old(src2);
 {
 }
 
-procedure{:instruction Ins(S.AddCarry64(dst, src))}{:quick exportOnly} Adc64Wrap(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.AddCarry64(dst, src))}{:quick exportOnly} Adc64Wrap(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -110,7 +111,7 @@ procedure{:instruction Ins(S.AddCarry64(dst, src))}{:quick exportOnly} Adc64Wrap
 {
 }
 
-procedure{:instruction Ins(S.Adcx64(dst, src))}{:quick exportOnly} Adcx64Wrap(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Adcx64(dst, src))}{:quick exportOnly} Adcx64Wrap(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -119,7 +120,7 @@ procedure{:instruction Ins(S.Adcx64(dst, src))}{:quick exportOnly} Adcx64Wrap(in
 {
 }
 
-procedure{:instruction Ins(S.Adox64(dst, src))}{:quick exportOnly} Adox64Wrap(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Adox64(dst, src))}{:quick exportOnly} Adox64Wrap(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -128,7 +129,7 @@ procedure{:instruction Ins(S.Adox64(dst, src))}{:quick exportOnly} Adox64Wrap(in
 {
 }
 
-procedure{:instruction Ins(S.Sub64(dst, src))}{:quick exportOnly} Sub64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Sub64(dst, src))}{:quick exportOnly} Sub64(inout dst:dst_opr64, src:opr64)
     requires
         0 <= dst - src;
     modifies
@@ -138,7 +139,7 @@ procedure{:instruction Ins(S.Sub64(dst, src))}{:quick exportOnly} Sub64(inout ds
 {
 }
 
-procedure{:instruction Ins(S.Sub64(dst, src))}{:quick exportOnly} Sub64Wrap(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Sub64(dst, src))}{:quick exportOnly} Sub64Wrap(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -153,9 +154,9 @@ let lemma_fundamental_div_mod (a b:nat64) :
   ()
 #endverbatim
 
-ghost procedure lemma_fundamental_div_mod(ghost a:nat64, ghost b:nat64) extern;
+ghost procedure{:public} lemma_fundamental_div_mod(ghost a:nat64, ghost b:nat64) extern;
 
-procedure{:instruction Ins(S.Mul64(src))}{:quick exportOnly} Mul64Wrap(src:opr64)
+procedure{:public}{:instruction Ins(S.Mul64(src))}{:quick exportOnly} Mul64Wrap(src:opr64)
     modifies
         efl;
         rax;
@@ -166,7 +167,7 @@ procedure{:instruction Ins(S.Mul64(src))}{:quick exportOnly} Mul64Wrap(src:opr64
     lemma_fundamental_div_mod(old(rax), old(src));
 }
 
-procedure{:instruction Ins(S.Mulx64(dst_hi, dst_lo, src))}{:quick exportOnly} Mulx64(out dst_hi:dst_opr64, out dst_lo:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Mulx64(dst_hi, dst_lo, src))}{:quick exportOnly} Mulx64(out dst_hi:dst_opr64, out dst_lo:dst_opr64, src:opr64)
     requires @dst_hi != @dst_lo;
     reads
         rdx;
@@ -176,7 +177,7 @@ procedure{:instruction Ins(S.Mulx64(dst_hi, dst_lo, src))}{:quick exportOnly} Mu
     lemma_fundamental_div_mod(old(rdx), old(src));
 }
 
-procedure{:instruction Ins(S.IMul64(dst, src))}{:quick exportOnly} IMul64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.IMul64(dst, src))}{:quick exportOnly} IMul64(inout dst:dst_opr64, src:opr64)
     requires
         0 <= dst * src < pow2_64;
     modifies
@@ -186,7 +187,7 @@ procedure{:instruction Ins(S.IMul64(dst, src))}{:quick exportOnly} IMul64(inout
 {
 }
 
-procedure{:instruction Ins(S.Xor64(dst, src))}{:quick exportOnly} Xor64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.Xor64(dst, src))}{:quick exportOnly} Xor64(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
@@ -196,23 +197,23 @@ procedure{:instruction Ins(S.Xor64(dst, src))}{:quick exportOnly} Xor64(inout ds
 {
 }
 
-procedure{:instruction Ins(S.And64(dst, src))}{:quick exportOnly} And64(inout dst:dst_opr64, src:opr64)
+procedure{:public}{:instruction Ins(S.And64(dst, src))}{:quick exportOnly} And64(inout dst:dst_opr64, src:opr64)
     modifies
         efl;
     ensures
         dst == old(iand64(dst,src));
 {
 }
 
-procedure{:instruction Ins(S.Shl64(dst, amt))}{:quick exportOnly} Shl64(inout dst:dst_opr64, amt:shift_amt64)
+procedure{:public}{:instruction Ins(S.Shl64(dst, amt))}{:quick exportOnly} Shl64(inout dst:dst_opr64, amt:shift_amt64)
     modifies
         efl;
     ensures
         dst == old(ishl64(dst, amt));
 {
 }
 
-procedure{:instruction Ins(S.Shr64(dst, amt))}{:quick exportOnly} Shr64(inout dst:dst_opr64, amt:shift_amt64)
+procedure{:public}{:instruction Ins(S.Shr64(dst, amt))}{:quick exportOnly} Shr64(inout dst:dst_opr64, amt:shift_amt64)
     modifies
         efl;
     ensures

diff --git a/fstar/code/arch/x64/X64.Vale.InsMem.vaf b/fstar/code/arch/x64/X64.Vale.InsMem.vaf
@@ -7,6 +7,7 @@ include{:fstar}{:open} "X64.Vale.QuickCode"
 module X64.Vale.InsMem
 
 #verbatim{:interface}
+open Defs_s
 open X64.Machine_s
 open X64.Vale.State
 open X64.Vale.Decls
@@ -26,12 +27,12 @@ module P = X64.Print_s
 
 #reset-options "--initial_fuel 2 --max_fuel 2 --z3rlimit 20"
 
-procedure{:operand} Mem_in(base:opr, inline offset:int) returns(o:opr)
+procedure{:public}{:operand} Mem_in(base:opr, inline offset:int) returns(o:opr)
     reads
         mem;
     extern;
 
-procedure{:instruction Ins(S.Mov64(dst, OMem(MReg(get_reg(src), offset))))}{:quick exportOnly} Load64(
+procedure{:public}{:instruction Ins(S.Mov64(dst, OMem(MReg(get_reg(src), offset))))}{:quick exportOnly}{:public} Load64(
     out dst:dst_opr64,
         src:reg_opr64,
         inline offset:int)
@@ -44,7 +45,7 @@ procedure{:instruction Ins(S.Mov64(dst, OMem(MReg(get_reg(src), offset))))}{:qui
 {
 }
 
-procedure{:instruction Ins(S.Mov64(OMem(MReg(get_reg(dst), offset)), src))}{:quick exportOnly} Store64(
+procedure{:public}{:instruction Ins(S.Mov64(OMem(MReg(get_reg(dst), offset)), src))}{:quick exportOnly}{:public} Store64(
         dst:reg_opr64,
         src:opr64,
         inline offset:int)

diff --git a/fstar/code/arch/x64/X64.Vale.InsVector.vaf b/fstar/code/arch/x64/X64.Vale.InsVector.vaf
@@ -13,6 +13,7 @@ include{:fstar}{:open} "X64.Vale.QuickCode"
 module X64.Vale.InsVector
 
 #verbatim{:interface}
+open Defs_s
 open Words_s
 open Words.Two_s
 open Words.Four_s
@@ -71,7 +72,7 @@ operand_type xmm:quad32 :=
 | inout xmm12 | inout xmm13 | inout xmm14 | inout xmm15
 ;
 
-procedure{:instruction Ins(S.Paddd(dst, src))}{:quick exportOnly} Paddd(inout dst:xmm, src:xmm)
+procedure{:public}{:instruction Ins(S.Paddd(dst, src))}{:quick exportOnly} Paddd(inout dst:xmm, src:xmm)
     modifies efl;
     ensures
         dst == old(Mkfour(
@@ -82,29 +83,29 @@ procedure{:instruction Ins(S.Paddd(dst, src))}{:quick exportOnly} Paddd(inout ds
 {
 }
 
-procedure{:instruction Ins(S.Pxor(dst, src))}{:quick exportOnly} Pxor(inout dst:xmm, src:xmm)
+procedure{:public}{:instruction Ins(S.Pxor(dst, src))}{:quick exportOnly} Pxor(inout dst:xmm, src:xmm)
     ensures
         dst == old(quad32_xor(dst, src));
 {
 }
 
-procedure{:instruction Ins(S.Pslld(dst, amt))}{:quick exportOnly} Pslld(inout dst:xmm, inline amt:int)
+procedure{:public}{:instruction Ins(S.Pslld(dst, amt))}{:quick exportOnly} Pslld(inout dst:xmm, inline amt:int)
     requires
         0 <= amt < 32;
     ensures
         dst == four_map((lambda i:nat32 :: ishl32(i, amt)), old(dst));
 {
 }
 
-procedure{:instruction Ins(S.Psrld(dst, amt))}{:quick exportOnly} Psrld(inout dst:xmm, inline amt:int)
+procedure{:public}{:instruction Ins(S.Psrld(dst, amt))}{:quick exportOnly} Psrld(inout dst:xmm, inline amt:int)
     requires
         0 <= amt < 32;
     ensures
         dst == four_map((lambda i:nat32 :: ishr32(i, amt)), old(dst));
 {
 }
 
-procedure{:instruction Ins(S.Pshufd(dst, src, permutation))}{:quick exportOnly}
+procedure{:public}{:instruction Ins(S.Pshufd(dst, src, permutation))}{:quick exportOnly}
     Pshufd(inout dst:xmm, src:xmm, inline permutation:imm8)
     ensures
         dst == old(Mkfour(
@@ -115,7 +116,7 @@ procedure{:instruction Ins(S.Pshufd(dst, src, permutation))}{:quick exportOnly}
 {
 }
 
-procedure{:instruction Ins(S.Pcmpeqd(dst, src))}{:quick exportOnly}
+procedure{:public}{:instruction Ins(S.Pcmpeqd(dst, src))}{:quick exportOnly}
     Pcmpeqd(inout dst:xmm, src:xmm)
     ensures
         dst == old(Mkfour(
@@ -126,7 +127,7 @@ procedure{:instruction Ins(S.Pcmpeqd(dst, src))}{:quick exportOnly}
 {
 }
 
-procedure{:instruction Ins(S.Pextrq(dst, src, index))}{:quick exportOnly}
+procedure{:public}{:instruction Ins(S.Pextrq(dst, src, index))}{:quick exportOnly}
     Pextrq(out dst:dst_opr64, src:xmm, inline index:imm8)
     requires
         index < 2;
@@ -135,7 +136,7 @@ procedure{:instruction Ins(S.Pextrq(dst, src, index))}{:quick exportOnly}
 {
 }
 
-procedure{:instruction Ins(S.Pinsrd(dst, src, index))}{:quick exportOnly}
+procedure{:public}{:instruction Ins(S.Pinsrd(dst, src, index))}{:quick exportOnly}
     Pinsrd(inout dst:xmm, src:opr64, inline index:imm8)
     requires
         src < pow2_32;
@@ -145,7 +146,7 @@ procedure{:instruction Ins(S.Pinsrd(dst, src, index))}{:quick exportOnly}
 {
 }
 
-procedure{:quick exportOnly}
+procedure{:public}{:quick exportOnly}
     PinsrdImm(inout dst:xmm, inline immediate:nat32, inline index:imm8, out tmp:reg_opr64)
     requires
         index < 4;
@@ -156,7 +157,7 @@ procedure{:quick exportOnly}
     Pinsrd(dst, tmp, index);
 }
 
-procedure{:instruction Ins(S.Pinsrq(dst, src, index))}{:quick exportOnly}
+procedure{:public}{:instruction Ins(S.Pinsrq(dst, src, index))}{:quick exportOnly}
     Pinsrq(inout dst:xmm, src:opr64, inline index:imm8)
     requires
         index < 2;
@@ -165,7 +166,7 @@ procedure{:instruction Ins(S.Pinsrq(dst, src, index))}{:quick exportOnly}
 {
 }
 
-procedure{:quick exportOnly}
+procedure{:public}{:quick exportOnly}
     PinsrqImm(inout dst:xmm, inline immediate:nat64, inline index:imm8, out tmp:reg_opr64)
     requires
         index < 2;
@@ -176,7 +177,7 @@ procedure{:quick exportOnly}
     Pinsrq(dst, tmp, index);
 }
 
-procedure{:instruction Ins(S.VPSLLDQ(dst, src, 4))}{:quick exportOnly} VPSLLDQ4(inout dst:xmm, src:xmm)
+procedure{:public}{:instruction Ins(S.VPSLLDQ(dst, src, 4))}{:quick exportOnly} VPSLLDQ4(inout dst:xmm, src:xmm)
     ensures
         dst == old(Mkfour(0, src.lo0, src.lo1, src.hi2));
 {

diff --git a/fstar/code/arch/x64/X64.Vale.Lemmas.fsti b/fstar/code/arch/x64/X64.Vale.Lemmas.fsti
@@ -1,4 +1,5 @@
 module X64.Vale.Lemmas
+open Defs_s
 open Prop_s
 open X64.Machine_s
 open X64.Vale.State

diff --git a/fstar/code/arch/x64/X64.Vale.QuickCode.fst b/fstar/code/arch/x64/X64.Vale.QuickCode.fst
@@ -1,4 +1,5 @@
 module X64.Vale.QuickCode
+open Defs_s
 open X64.Machine_s
 open X64.Vale.State
 open X64.Vale.Decls

diff --git a/fstar/code/arch/x64/X64.Vale.QuickCodes.fsti b/fstar/code/arch/x64/X64.Vale.QuickCodes.fsti
@@ -1,6 +1,7 @@
 // Optimized weakest precondition generation for 'quick' procedures
 
 module X64.Vale.QuickCodes
+open Defs_s
 open X64.Machine_s
 open X64.Vale.State
 open X64.Vale.Decls

diff --git a/fstar/code/arch/x64/X64.Vale.Regs.fsti b/fstar/code/arch/x64/X64.Vale.Regs.fsti
@@ -1,6 +1,7 @@
 module X64.Vale.Regs
 // This interface should not refer to Semantics_s
 
+open Defs_s
 open Prop_s
 open X64.Machine_s
 

diff --git a/fstar/code/arch/x64/X64.Vale.State.fsti b/fstar/code/arch/x64/X64.Vale.State.fsti
@@ -1,6 +1,7 @@
 module X64.Vale.State
 // This interface should not refer to Semantics_s
 
+open Defs_s
 open Prop_s
 open X64.Machine_s
 

diff --git a/fstar/code/arch/x64/X64.Vale.Xmms.fsti b/fstar/code/arch/x64/X64.Vale.Xmms.fsti
@@ -1,6 +1,7 @@
 module X64.Vale.Xmms
 // This interface should not refer to Semantics_s
 
+open Defs_s
 open Prop_s
 open X64.Machine_s
 

diff --git a/fstar/code/test/Test.Memcpy.vaf b/fstar/code/test/Test.Memcpy.vaf
@@ -5,6 +5,7 @@ include "../arch/x64/X64.Vale.InsVector.vaf"
 module Test.Memcpy
 
 #verbatim{:interface}{:implementation}
+open Defs_s
 open X64.Machine_s
 open X64.Vale.State
 open X64.Vale.Decls

diff --git a/fstar/specs/defs/Defs_s.fst b/fstar/specs/defs/Defs_s.fst
@@ -0,0 +1,5 @@
+module Defs_s
+// Small number of definitions that are meant to be opened by everyone
+
+// Used to guide normalization in F*'s type system
+irreducible let va_qattr = ()