From f73b41a28d462345bf0a63c0bff7037f3668853e Mon Sep 17 00:00:00 2001 From: Qunyan Mangus Date: Thu, 4 Oct 2018 09:15:26 -0700 Subject: [PATCH 1/7] Only emit a procedure into an .fsti file if it has the attribute {:public} --- fstar/code/arch/x64/X64.Vale.InsBasic.vaf | 8 ++++---- fstar/code/arch/x64/X64.Vale.InsMem.vaf | 4 ++-- tools/Vale/src/emit_common_base.fs | 6 +++++- tools/Vale/src/emit_common_lemmas.fs | 4 ++-- tools/Vale/src/emit_common_quick_export.fs | 10 +++++----- tools/Vale/src/emit_fstar_text.fs | 2 ++ tools/Vale/src/transform.fs | 3 ++- 7 files changed, 22 insertions(+), 15 deletions(-) diff --git a/fstar/code/arch/x64/X64.Vale.InsBasic.vaf b/fstar/code/arch/x64/X64.Vale.InsBasic.vaf index 10d9e6cd..d713d065 100644 --- a/fstar/code/arch/x64/X64.Vale.InsBasic.vaf +++ b/fstar/code/arch/x64/X64.Vale.InsBasic.vaf @@ -61,20 +61,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{:quick exportOnly}{:typecheck false}{:public} 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{:instruction Ins(S.Mov64(dst,src))}{:quick exportOnly}{:public} 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{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly}{:public} Add64(inout dst:dst_opr64, src:opr64) modifies efl; requires @@ -84,7 +84,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{:instruction Ins(S.Add64(dst,src))}{:quick exportOnly}{:public} Add64Wrap(inout dst:dst_opr64, src:opr64) modifies efl; ensures diff --git a/fstar/code/arch/x64/X64.Vale.InsMem.vaf b/fstar/code/arch/x64/X64.Vale.InsMem.vaf index 061e0f10..b0ecdd9b 100644 --- a/fstar/code/arch/x64/X64.Vale.InsMem.vaf +++ b/fstar/code/arch/x64/X64.Vale.InsMem.vaf @@ -31,7 +31,7 @@ procedure{:operand} Mem_in(base:opr, inline offset:int) returns(o:opr) mem; extern; -procedure{:instruction Ins(S.Mov64(dst, OMem(MReg(get_reg(src), offset))))}{:quick exportOnly} Load64( +procedure{: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 +44,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{: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/tools/Vale/src/emit_common_base.fs b/tools/Vale/src/emit_common_base.fs index 5ab00bdf..8eaedea6 100644 --- a/tools/Vale/src/emit_common_base.fs +++ b/tools/Vale/src/emit_common_base.fs @@ -57,7 +57,7 @@ let filter_fun_attr (x, es) = let filter_proc_attr (x, es) = match x with - | Id ("timeLimit" | "timeLimitMultiplier" | "tactic" | "quick" | "recursive" | "decrease") -> true + | Id ("timeLimit" | "timeLimitMultiplier" | "tactic" | "quick" | "recursive" | "decrease" | "public") -> true | _ -> false in @@ -66,6 +66,10 @@ let attr_no_verify (s:string) (a:attrs):attrs = if !disable_verify && not verify then [(Id s, [])] else [] +let attr_public (a:attrs) : attrs = + let isPublic = attrs_get_bool (Id "public") false a in + if isPublic then [(Id "public", [])] else [] + // convert imperative updates to functional let assignments let rec let_updates_stmts (scope:Map) (ss:stmt list):(Set * stmt list)= let (_, updates, ss_rev) = List.fold let_update_stmt_rev (scope, Set.empty, []) ss in diff --git a/tools/Vale/src/emit_common_lemmas.fs b/tools/Vale/src/emit_common_lemmas.fs index 6bf32147..65c2a672 100644 --- a/tools/Vale/src/emit_common_lemmas.fs +++ b/tools/Vale/src/emit_common_lemmas.fs @@ -593,7 +593,7 @@ let build_lemma (env:env) (benv:build_env) (b1:id) (stmts:stmt list) (bstmts:stm fret = tProp; fspecs = []; fbody = Some eReq; - fattrs = [(Id "public", [])]; + fattrs = attr_public p.pattrs; } in let fEns = @@ -606,7 +606,7 @@ let build_lemma (env:env) (benv:build_env) (b1:id) (stmts:stmt list) (bstmts:stm fret_name = None; fspecs = []; fbody = Some eEns; - fattrs = [(Id "public", [])]; + fattrs = attr_public p.pattrs; } in [(loc, DFun fReq); (loc, DFun fEns)] diff --git a/tools/Vale/src/emit_common_quick_export.fs b/tools/Vale/src/emit_common_quick_export.fs index ab00332e..83d6183e 100644 --- a/tools/Vale/src/emit_common_quick_export.fs +++ b/tools/Vale/src/emit_common_quick_export.fs @@ -166,7 +166,7 @@ let build_proc (env:env) (loc:loc) (p:proc_decl):decls = fret = tType0; fspecs = []; fbody = Some (hide_ifs wpBody); - fattrs = [(Id "public", []); (Id "qattr", [])] @ attr_no_verify "lax" p.pattrs; + fattrs = [(Id "qattr", [])] @ attr_public p.pattrs @ attr_no_verify "lax" p.pattrs; } in @@ -195,7 +195,7 @@ let build_proc (env:env) (loc:loc) (p:proc_decl):decls = prets = []; pspecs = [(loc, specReq); (loc, specEns)]; pbody = Some []; - pattrs = attr_no_verify "admit" p.pattrs; + pattrs = attr_public p.pattrs @ attr_no_verify "admit" p.pattrs; } in @@ -219,7 +219,7 @@ let build_proc (env:env) (loc:loc) (p:proc_decl):decls = prets = [rSM; rF0; rG]; pspecs = [(loc, specReq); (loc, specEns)]; pbody = Some [sCallLemma; sAssignG]; - pattrs = [(Id "reducible", [])] @ attr_no_verify "admit" p.pattrs; + pattrs = [(Id "reducible", [])] @ attr_public p.pattrs @ attr_no_verify "admit" p.pattrs; } in @@ -242,7 +242,7 @@ let build_proc (env:env) (loc:loc) (p:proc_decl):decls = prets = []; pspecs = [(loc, specReq); (loc, specEns)]; pbody = Some [sCallLemma; sLemmaUpd; sAssertEq]; - pattrs = attr_no_verify "admit" p.pattrs; + pattrs = attr_public p.pattrs @ attr_no_verify "admit" p.pattrs; } in @@ -261,7 +261,7 @@ let build_proc (env:env) (loc:loc) (p:proc_decl):decls = fret = tRetQuick; fspecs = []; fbody = Some eQuick; - fattrs = [(Id "public", []); (Id "opaque_to_smt", []); (Id "qattr", [])] @ attr_no_verify "lax" p.pattrs; + fattrs = [(Id "opaque_to_smt", []); (Id "qattr", [])] @ attr_public p.pattrs @ attr_no_verify "lax" p.pattrs; } in [(loc, DFun fWp); (loc, DProc pMonotone); (loc, DProc pCompute); (loc, DProc pProof); (loc, DFun fQuick)] diff --git a/tools/Vale/src/emit_fstar_text.fs b/tools/Vale/src/emit_fstar_text.fs index 76a1c3f7..0db30d90 100644 --- a/tools/Vale/src/emit_fstar_text.fs +++ b/tools/Vale/src/emit_fstar_text.fs @@ -434,6 +434,7 @@ let emit_proc (ps:print_state) (loc:loc) (p:proc_decl):unit = (match ps.print_interface with None -> () | Some psi -> psi.PrintLine ("")); let psi = match ps.print_interface with None -> ps | Some psi -> psi in let tactic = match p.pbody with None -> None | Some _ -> attrs_get_exp_opt (Id "tactic") p.pattrs in + let isPublic = attrs_get_bool (Id "public") false p.pattrs in let isRecursive = attrs_get_bool (Id "recursive") false p.pattrs in let decreaseExps = attrs_get_exps_opt (Id "decrease") p.pattrs in let isAdmit = attrs_get_bool (Id "admit") false p.pattrs in @@ -459,6 +460,7 @@ let emit_proc (ps:print_state) (loc:loc) (p:proc_decl):unit = ( match (tactic, ps.print_interface) with | (Some _, None) -> () | (_, _) -> + let psi = if isPublic then psi else ps psi.PrintLine ("val " + (sid p.pname) + " : " + (val_string_of_formals args)); printPType psi "-> " decreases0 ); diff --git a/tools/Vale/src/transform.fs b/tools/Vale/src/transform.fs index 938ab89c..a8a535ff 100644 --- a/tools/Vale/src/transform.fs +++ b/tools/Vale/src/transform.fs @@ -1137,7 +1137,8 @@ let hoist_while_loops (env:env) (loc:loc) (p:proc_decl):decl list = prets = p_outs; pspecs = specs @ [spec_enter_body; spec_precedes]; pbody = Some (sInits @ b); - pattrs = (Id "already_has_mod_ok", [])::p.pattrs; + // always non-public, even if they are generated from the body of a public procedure + pattrs = [(Id "pubic", [EBool false]); (Id "already_has_mod_ok", [])] @ p.pattrs; } in let p_while = From 2cbb19dd41bfabb8e6753ef51c138f2431d78f9b Mon Sep 17 00:00:00 2001 From: Qunyan Mangus Date: Thu, 4 Oct 2018 11:38:18 -0700 Subject: [PATCH 2/7] Only emit 'val' of {:opaque} and {:public_decl} procedures to *.fsti if they are {:public} --- tools/Vale/src/emit_fstar_text.fs | 10 ++++++++-- tools/Vale/src/transform.fs | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/tools/Vale/src/emit_fstar_text.fs b/tools/Vale/src/emit_fstar_text.fs index 0db30d90..984e416c 100644 --- a/tools/Vale/src/emit_fstar_text.fs +++ b/tools/Vale/src/emit_fstar_text.fs @@ -404,7 +404,10 @@ let emit_fun (ps:print_state) (loc:loc) (f:fun_decl):unit = let decreases1 = if isRecursive then string_of_decrease dArgs 1 else "" in if isOpaque then ps.PrintLine (sVal (sid (transparent_id f.fname)) decreases0); - psi.PrintLine (sVal (sid f.fname) decreases1); + if isPublic then + psi.PrintLine (sVal (sid f.fname) decreases1); + else + ps.PrintLine (sVal (sid f.fname) decreases1); ( match f.fbody with | None -> () | Some e -> printBody header true (sid (transparent_id f.fname)) e @@ -414,7 +417,10 @@ let emit_fun (ps:print_state) (loc:loc) (f:fun_decl):unit = let header = if isRecursive then "and " else "let " in printBody header true (sid f.fname) eOpaque else if isPublicDecl then - psi.PrintLine (sVal (sid f.fname) decreases1); + if isPublic then + psi.PrintLine (sVal (sid f.fname) decreases1); + else + ps.PrintLine (sVal (sid f.fname) decreases1); ( match f.fbody with | None -> () | Some e -> printBody header true (sid f.fname) e diff --git a/tools/Vale/src/transform.fs b/tools/Vale/src/transform.fs index a8a535ff..ee108cbe 100644 --- a/tools/Vale/src/transform.fs +++ b/tools/Vale/src/transform.fs @@ -1138,7 +1138,7 @@ let hoist_while_loops (env:env) (loc:loc) (p:proc_decl):decl list = pspecs = specs @ [spec_enter_body; spec_precedes]; pbody = Some (sInits @ b); // always non-public, even if they are generated from the body of a public procedure - pattrs = [(Id "pubic", [EBool false]); (Id "already_has_mod_ok", [])] @ p.pattrs; + pattrs = [(Id "public", [EBool false]); (Id "already_has_mod_ok", [])] @ p.pattrs; } in let p_while = From 09ade5dd7f36ed3b1113578e389570c07b9252b7 Mon Sep 17 00:00:00 2001 From: Qunyan Mangus Date: Thu, 4 Oct 2018 15:29:52 -0700 Subject: [PATCH 3/7] For {:opaque} and {:publicDecl}, only "val" is written to *.fsti if it is public, enverything else is written goes into *.fst regardless if it is public or not. --- tools/Vale/src/emit_common_base.fs | 2 +- tools/Vale/src/emit_fstar_text.fs | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/tools/Vale/src/emit_common_base.fs b/tools/Vale/src/emit_common_base.fs index 8eaedea6..2858ad50 100644 --- a/tools/Vale/src/emit_common_base.fs +++ b/tools/Vale/src/emit_common_base.fs @@ -51,7 +51,7 @@ let varLhsOfId (x:id):lhs = (x, Some (None, NotGhost)) let filter_fun_attr (x, es) = match x with | Id "recursive" -> !fstar - | Id ("tactic" | "quick" | "decrease") -> true + | Id ("tactic" | "quick" | "decrease" | "public") -> true | _ -> false in diff --git a/tools/Vale/src/emit_fstar_text.fs b/tools/Vale/src/emit_fstar_text.fs index 984e416c..a9182bd1 100644 --- a/tools/Vale/src/emit_fstar_text.fs +++ b/tools/Vale/src/emit_fstar_text.fs @@ -384,7 +384,11 @@ let emit_fun (ps:print_state) (loc:loc) (f:fun_decl):unit = let isOpaque = isOpaque && not isAdmit in let isRecursive = attrs_get_bool (Id "recursive") false f.fattrs in (match ps.print_interface with None -> () | Some psi -> psi.PrintLine ("")); - let ps = match (isPublic, ps.print_interface) with (true, Some psi) -> psi | _ -> ps in + // write everything to *.fsti if it is public and not opaque or publicDecl. + // For opaque and publicDecl, only "val" is written into *.fsti if it is public, + // everything else goes into *.fst regardless if it is public or not. + let writeToPsi = isPublic && not (isOpaque || isPublicDecl) + let ps = match (writeToPsi, ps.print_interface) with (true, Some psi) -> psi | _ -> ps in let psi = match ps.print_interface with None -> ps | Some psi -> psi in emit_laxness ps f.fattrs; let sg = match f.fghost with Ghost -> "GTot" | NotGhost -> "Tot" in From e3571c5858f75edbd90b74ce04b26fe57cf9cbf5 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Thu, 4 Oct 2018 16:37:57 -0700 Subject: [PATCH 4/7] Enable quickMods by default --- SConstruct | 2 +- tools/Vale/src/emit_common_base.fs | 2 +- tools/Vale/src/main.fs | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/SConstruct b/SConstruct index 62a34826..b5dcde78 100644 --- 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/tools/Vale/src/emit_common_base.fs b/tools/Vale/src/emit_common_base.fs index 04db9c2a..8bf474ff 100644 --- a/tools/Vale/src/emit_common_base.fs +++ b/tools/Vale/src/emit_common_base.fs @@ -10,7 +10,7 @@ open Microsoft.FSharp.Math open System.Numerics let concise_lemmas = ref true; -let quick_mods = ref false; +let quick_mods = ref true; let precise_opaque = ref false; let reprint_decls_rev = ref ([]:decls) let disable_verify = ref false diff --git a/tools/Vale/src/main.fs b/tools/Vale/src/main.fs index 51e49088..27f57b67 100644 --- a/tools/Vale/src/main.fs +++ b/tools/Vale/src/main.fs @@ -143,6 +143,7 @@ let main (argv) = | "-reprintBlankLines=false" :: l -> reprint_blank_lines := false; match_args l | "-conciseLemmas=false" :: l -> concise_lemmas := false; match_args l | "-quickMods" :: l -> quick_mods := true; match_args l + | "-quickMods=false" :: l -> quick_mods := false; match_args l | "-disableVerify" :: l -> disable_verify := true; match_args l | "-omitUnverified" :: l -> omit_unverified := true; match_args l | "-noLemmas" :: l -> no_lemmas := true ; match_args l From f267e69137f2bed43f83cd7bd7a8ddbf2bbcadc5 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Thu, 4 Oct 2018 20:03:09 -0700 Subject: [PATCH 5/7] More ImportFStarTypes parsing --- tools/ImportFStarTypes/src/main.fs | 18 +++++++++++------- tools/ImportFStarTypes/src/parse.fsy | 3 ++- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/tools/ImportFStarTypes/src/main.fs b/tools/ImportFStarTypes/src/main.fs index a9d93828..109fa584 100644 --- a/tools/ImportFStarTypes/src/main.fs +++ b/tools/ImportFStarTypes/src/main.fs @@ -246,13 +246,17 @@ let rec parse_exp (e:raw_exp):f_exp = | RList [RLtGt _; e; RList us] -> EAppUnivs (parse_exp e, parse_univs us) | RList [RArrow _; RList ((RMatch _)::_); _] -> EUnsupported "MATCH" | RList [RArrow _; e1; e2] -> - let (a, e1) = get_aqual e1 in - let (x, e1) = - match e1 with - | RList [RColon _; RId (_, x); e1] -> (parse_id x, e1) - | _ -> err ("parse_exp: RArrow: " + string_of_raw_exp e) - in - EArrow (a, x, parse_exp e1, parse_exp e2) + try + ( + let (a, e1) = get_aqual e1 in + let (x, e1) = + match e1 with + | RList [RColon _; RId (_, x); e1] -> (parse_id x, e1) + | _ -> err ("parse_exp: RArrow: " + string_of_raw_exp e) + in + EArrow (a, x, parse_exp e1, parse_exp e2) + ) + with Err s -> EUnsupported s | RList [RColon _; e1; RId (_, ("Tm_type" | "Tm_delayed-resolved"))] -> parse_exp e1 | RList [RColon _; e1; RList [RColon _; RId (_, ("Tm_name" | "Tm_fvar")); _]] -> parse_exp e1 | RList [RColon _; e1; e2] -> ETyped (parse_exp e1, parse_exp e2) diff --git a/tools/ImportFStarTypes/src/parse.fsy b/tools/ImportFStarTypes/src/parse.fsy index b6afff0d..1d149ada 100644 --- a/tools/ImportFStarTypes/src/parse.fsy +++ b/tools/ImportFStarTypes/src/parse.fsy @@ -95,7 +95,7 @@ exp | exp1 PLUS exp1 { RList [RPlus $2; $1; $3] } | exp1 LBRACE exp RBRACE { RList [RRefine $2; $1; $3] } | exp1 ASCRIBED exp1s { RList [RAscribed $2; $1; rlist_opt $3] } - | exp1 ASCRIBED LBRACKET exp RBRACKET exp1s { RList [RAscribed $2; $1; $4; rlist_opt $6] } +/* | exp1 ASCRIBED LBRACKET exp RBRACKET exp1s { RList [RAscribed $2; $1; $4; rlist_opt $6] } */ | DECREASES exp1 { RList [RDecreases $1; $2] } exp1 @@ -118,6 +118,7 @@ exp1 exp2 : LPAREN exp RPAREN { match $2 with RList [] -> RUnitValue $1 | e -> e } + | LBRACKET exp RBRACKET { RList [] } | LPAREN ATTRIBUTES exp1s RPAREN { RList [RAttributes $2; RList $3] } | SCOLON { RSColon $1 } /* used in match and let */ | MATCH { RMatch $1 } /* used in match */ From d5264403a3161f04be05f2634f53e091dcaa5cea Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Mon, 8 Oct 2018 07:26:16 -0700 Subject: [PATCH 6/7] Fix parentheses in emit_fstar_text --- tools/Vale/src/emit_fstar_text.fs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/tools/Vale/src/emit_fstar_text.fs b/tools/Vale/src/emit_fstar_text.fs index a9182bd1..a6d7f2df 100644 --- a/tools/Vale/src/emit_fstar_text.fs +++ b/tools/Vale/src/emit_fstar_text.fs @@ -102,7 +102,7 @@ let rec string_of_exp_prec prec e = | EString s -> ("\"" + s.Replace("\\", "\\\\") + "\"", 99) | EOp (Uop (UCall CallGhost), [e]) -> (r prec e, prec) | EOp (Uop UReveal, [EApply (x, _, es)]) -> (r prec (vaApp "reveal_opaque" [eapply (transparent_id x) es]), prec) - | EOp (Uop UReveal, [EVar x]) -> ("(reveal_opaque " + (sid x) + ")", prec) + | EOp (Uop UReveal, [EVar x]) -> ("reveal_opaque " + (sid x), 90) | EOp (Uop (UNot BpBool), [e]) -> ("not " + (r 99 e), 90) | EOp (Uop (UNot BpProp), [e]) -> ("~" + (r 99 e), 90) | EOp (Uop UNeg, [e]) -> ("-" + (r 99 e), 0) @@ -132,10 +132,10 @@ let rec string_of_exp_prec prec e = | EOp (Subscript, [e1; e2]) -> (r prec (vaApp "subscript" [e1; e2]), prec) | EOp (Update, [e1; e2; e3]) -> (r prec (vaApp "update" [e1; e2; e3]), prec) | EOp (Cond, [e1; e2; e3]) -> ("if " + (r 90 e1) + " then " + (r 90 e2) + " else " + (r 90 e3), 0) - | EOp (FieldOp x, [e]) -> ((r 90 e) + "." + (sid x), 90) + | EOp (FieldOp x, [e]) -> ((r 95 e) + "." + (sid x), 95) | EOp (FieldUpdate x, [e1; e2]) -> ("({" + (r 90 e1) + " with " + (sid x) + " = " + (r 90 e2) + "})", 90) | EOp ((Subscript | Update | Cond | FieldOp _ | FieldUpdate _ | CodeLemmaOp | RefineOp | StateOp _ | OperandArg _), _) -> internalErr (sprintf "EOp: %A" e) - | EApply (x, _, es) -> ("(" + (sid x) + " " + (string_of_args es) + ")", 90) + | EApply (x, _, es) -> ((sid x) + " " + (string_of_args es), 90) | EBind ((Forall | Exists | Lambda), [], [], _, e) -> (r prec e, prec) | EBind (Forall, [], xs, ts, e) -> qbind "forall" " . " xs ts e | EBind (Exists, [], xs, ts, e) -> qbind "exists" " . " xs ts e @@ -160,9 +160,9 @@ and string_of_triggers (ts:exp list list):string = | [] -> "" | [t] -> "{:pattern" + string_of_trigger t + "}" | _::_::_ -> "{:pattern " + String.concat "\/ " (List.map string_of_trigger ts) + "}" -and string_of_exp (e:exp):string = string_of_exp_prec 90 e +and string_of_exp (e:exp):string = string_of_exp_prec 99 e +and string_of_exp90 (e:exp):string = string_of_exp_prec 90 e and string_of_exps (es:exp list):string = String.concat " " (List.map string_of_exp es) -and string_of_exps_tail (es:exp list):string = String.concat "" (List.map (fun e -> " " + string_of_exp e) es) and string_of_args (es:exp list):string = match es with [] -> "()" | _ -> string_of_exps es let name_of_formal (x:id, t:typ option) = sid x @@ -212,14 +212,14 @@ let rec emit_stmt (ps:print_state) (outs:(bool * formal list) option) (s:stmt):u | SVar (x, tOpt, _, g, a, None) -> () // used to forward-declare variables for SLetUpdates | SVar (x, tOpt, _, g, a, Some e) -> let sf = string_of_formal (x, tOpt) in - let rhs = " = " + (string_of_exp e) in + let rhs = " = " + (string_of_exp90 e) in ps.PrintLine ((string_of_var_storage g) + "let " + sf + rhs + " in") | SAlias _ -> internalErr "SAlias" - | SAssign ([], e) -> ps.PrintLine ((string_of_exp e) + ";") + | SAssign ([], e) -> ps.PrintLine ((string_of_exp90 e) + ";") | SAssign ([lhs], e) -> - ps.PrintLine ("let " + (string_of_lhs_formal lhs) + " = " + (string_of_exp e) + " in") + ps.PrintLine ("let " + (string_of_lhs_formal lhs) + " = " + (string_of_exp90 e) + " in") | SAssign ((_::_::_) as lhss, e) -> - ps.PrintLine ("let (" + (String.concat ", " (List.map string_of_lhs_formal lhss)) + ") = " + (string_of_exp e) + " in") + ps.PrintLine ("let (" + (String.concat ", " (List.map string_of_lhs_formal lhss)) + ") = " + (string_of_exp90 e) + " in") | SLetUpdates (outs, s) -> ps.PrintLine ("let (" + (String.concat ", " (List.map string_of_formal outs)) + ") ="); ps.PrintLine "("; @@ -230,7 +230,7 @@ let rec emit_stmt (ps:print_state) (outs:(bool * formal list) option) (s:stmt):u | SBlock ss -> notImplemented "block" | SQuickBlock _ -> internalErr "quick_block" | SIfElse (_, e, ss1, ss2) -> - ps.PrintLine ("if " + (string_of_exp e) + " then"); + ps.PrintLine ("if " + (string_of_exp90 e) + " then"); emit_block ps "" outs ss1; ps.PrintLine ("else"); emit_block ps (match outs with None -> ";" | Some _ -> "") outs ss2 @@ -250,7 +250,7 @@ let rec emit_stmt (ps:print_state) (outs:(bool * formal list) option) (s:stmt):u | ([], _) -> () in ps.PrintLine "="; - ps.PrintLine ("if " + (string_of_exp e) + " then"); + ps.PrintLine ("if " + (string_of_exp90 e) + " then"); ps.Indent (); ps.PrintLine ("let " + (string_of_outs_formals outs) + " ="); emit_block ps "" outs ss; @@ -462,7 +462,7 @@ let emit_proc (ps:print_state) (loc:loc) (p:proc_decl):unit = ps.PrintLine ("(requires " + (string_of_exp rs) + ")"); let sprets = String.concat ", " (List.map (fun (x, _, _, _, _) -> sid x) p.prets) in let sDep = if isDependent then "|" else "" in - ps.PrintLine ("(ensures (" + (match p.prets with [] -> "" | _ -> "fun (" + sDep + sprets + sDep + ") -> ") + (string_of_exp es) + "))"); + ps.PrintLine ("(ensures (" + (match p.prets with [] -> "" | _ -> "fun (" + sDep + sprets + sDep + ") -> ") + (string_of_exp_prec 5 es) + "))"); ps.Unindent (); in let dArgs = match decreaseExps with Some es -> es | None -> List.map (fun (x, _) -> EVar x) args in From b17f1ed5f43e6072aeb3dc2ba022defd6ec8ed21 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Sun, 14 Oct 2018 17:23:31 -0700 Subject: [PATCH 7/7] Apply va_expand_state to while-loop state to allow more eta-expansion --- fstar/code/arch/x64/X64.Vale.Decls.fsti | 5 ++++- fstar/code/arch/x64/X64.Vale.InsBasic.vaf | 1 + fstar/code/arch/x64/X64.Vale.InsMem.vaf | 1 + fstar/code/arch/x64/X64.Vale.InsVector.vaf | 1 + fstar/code/arch/x64/X64.Vale.Lemmas.fsti | 1 + fstar/code/arch/x64/X64.Vale.QuickCode.fst | 1 + fstar/code/arch/x64/X64.Vale.QuickCodes.fsti | 1 + fstar/code/arch/x64/X64.Vale.Regs.fsti | 1 + fstar/code/arch/x64/X64.Vale.State.fsti | 1 + fstar/code/arch/x64/X64.Vale.Xmms.fsti | 1 + fstar/code/test/Test.Memcpy.vaf | 1 + fstar/specs/defs/Defs_s.fst | 5 +++++ fstar/specs/hardware/X64.Machine_s.fst | 2 +- fstar/specs/hardware/X64.Semantics_s.fst | 1 + tools/Vale/src/emit_common_quick_code.fs | 9 ++++++++- tools/Vale/src/transform.fs | 8 ++++---- tools/Vale/test/quick.vaf | 1 + 17 files changed, 34 insertions(+), 7 deletions(-) create mode 100644 fstar/specs/defs/Defs_s.fst diff --git a/fstar/code/arch/x64/X64.Vale.Decls.fsti b/fstar/code/arch/x64/X64.Vale.Decls.fsti index e3d8a1c3..7426acef 100644 --- 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 index 86a2913a..d2116593 100644 --- 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 diff --git a/fstar/code/arch/x64/X64.Vale.InsMem.vaf b/fstar/code/arch/x64/X64.Vale.InsMem.vaf index b8773220..771fd489 100644 --- 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 diff --git a/fstar/code/arch/x64/X64.Vale.InsVector.vaf b/fstar/code/arch/x64/X64.Vale.InsVector.vaf index afbded09..b9691ef2 100644 --- 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 diff --git a/fstar/code/arch/x64/X64.Vale.Lemmas.fsti b/fstar/code/arch/x64/X64.Vale.Lemmas.fsti index c099d450..e5a1baaf 100644 --- 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 index 49358cab..ee61f662 100644 --- 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 index 3e0e8f7c..f4f243d1 100644 --- 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 index 5835f507..13f61801 100644 --- 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 index 78477ea6..ce4cba92 100644 --- 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 index a526321f..4e6b1a07 100644 --- 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 index 8a420e6c..3977daad 100644 --- 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 new file mode 100644 index 00000000..207d6905 --- /dev/null +++ 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 = () diff --git a/fstar/specs/hardware/X64.Machine_s.fst b/fstar/specs/hardware/X64.Machine_s.fst index 3fd33e98..f5142829 100755 --- a/fstar/specs/hardware/X64.Machine_s.fst +++ b/fstar/specs/hardware/X64.Machine_s.fst @@ -1,6 +1,6 @@ module X64.Machine_s +open Defs_s -irreducible let va_qattr = () unfold let pow2_32 = Words_s.pow2_32 unfold let pow2_64 = Words_s.pow2_64 unfold let pow2_128 = Words_s.pow2_128 diff --git a/fstar/specs/hardware/X64.Semantics_s.fst b/fstar/specs/hardware/X64.Semantics_s.fst index c0f40b39..4b7499a1 100644 --- a/fstar/specs/hardware/X64.Semantics_s.fst +++ b/fstar/specs/hardware/X64.Semantics_s.fst @@ -1,5 +1,6 @@ module X64.Semantics_s +open Defs_s open Opaque_s open X64.Machine_s open Words_s diff --git a/tools/Vale/src/emit_common_quick_code.fs b/tools/Vale/src/emit_common_quick_code.fs index 1a842cfc..cae0382a 100644 --- a/tools/Vale/src/emit_common_quick_code.fs +++ b/tools/Vale/src/emit_common_quick_code.fs @@ -293,6 +293,13 @@ let build_qcode (env:env) (loc:loc) (p:proc_decl) (ss:stmt list):decls = let build_proc_body (env:env) (loc:loc) (p:proc_decl) (code:exp) (ens:exp):stmt list = let makeArg (x, t, storage, io, attrs) = EVar x let args = List.map makeArg p.pargs in + // let va_old = expand_state va_old in + let expand_arg (x, t, _, _, a) = + if attrs_get_bool (Reserved "expand_state") false a then + [SAssign ([(x, None)], eapply (Reserved "expand_state") [EVar x])] + else [] + in + let expansions = List.collect expand_arg p.pargs in // let (sM, fM, g) = wpSound_X code (qCodes_X ARGS) s0 (fun s0 sM gs -> let (g1, ..., gn) = g in ENS) in // let (g1, ..., gn) = g in let s0 = Reserved "s0" in @@ -326,4 +333,4 @@ let build_proc_body (env:env) (loc:loc) (p:proc_decl) (code:exp) (ens:exp):stmt | [] -> [] | _ -> [SAssign (gAssigns, EVar g)] in - qmods_opt sMods @ [sQc; sWpSound] @ qmods_opt sQcNorm @ qmods_opt sLemmaNormMods @ sAssignGs + expansions @ qmods_opt sMods @ [sQc; sWpSound] @ qmods_opt sQcNorm @ qmods_opt sLemmaNormMods @ sAssignGs diff --git a/tools/Vale/src/transform.fs b/tools/Vale/src/transform.fs index ee108cbe..9a68148b 100644 --- a/tools/Vale/src/transform.fs +++ b/tools/Vale/src/transform.fs @@ -725,8 +725,8 @@ and rewrite_vars_args (rctx:rewrite_ctx) (env:env) (p:proc_decl) (rets:lhs list) | (x, t, XAlias _, io, _) -> let _ = rewrite_vars_arg rctx NotGhost None io env ea in // check argument validity [] // drop argument - | (x, t, XGhost, In, []) -> [EOp (Uop UGhostOnly, [rewrite_vars_exp rctx env ea])] - | (x, t, XGhost, _, []) -> err ("out/inout ghost parameters are not supported") + | (x, t, XGhost, In, _) -> [EOp (Uop UGhostOnly, [rewrite_vars_exp rctx env ea])] + | (x, t, XGhost, _, _) -> err ("out/inout ghost parameters are not supported") | (x, _, _, _, _) -> err ("unexpected argument for parameter " + (err_id x) + " in call to " + (err_id p.pname)) in let rewrite_ret (pp, ((xlhs, _) as lhs)) = @@ -735,7 +735,7 @@ and rewrite_vars_args (rctx:rewrite_ctx) (env:env) (p:proc_decl) (rets:lhs list) | (x, t, XAlias _, _, _) -> let _ = rewrite_vars_arg rctx NotGhost None Out env (EVar xlhs) in // check argument validity ([], []) // drop argument - | (x, t, XGhost, _, []) -> ([lhs], []) + | (x, t, XGhost, _, _) -> ([lhs], []) | (x, _, _, _, _) -> err ("unexpected variable for return value " + (err_id x) + " in call to " + (err_id p.pname)) in let args = List.concat (List.map rewrite_arg margs) in @@ -1080,7 +1080,7 @@ let hoist_while_loops (env:env) (loc:loc) (p:proc_decl):decl list = let storage = match find_var x with InlineLocal _ -> XInline | _ -> XGhost in (in_id x, getType x, storage, In, []) in - let pf_state = (s_old, tState, XGhost, In, []) in + let pf_state = (s_old, tState, XGhost, In, [(Reserved "expand_state", [])]) in let p_ins_in = List.map to_pformal_in ins in let p_outs = List.map to_pformal outs in let subst_ins (ins:id list) (e:exp) = diff --git a/tools/Vale/test/quick.vaf b/tools/Vale/test/quick.vaf index d25d860e..54f4cfb2 100644 --- a/tools/Vale/test/quick.vaf +++ b/tools/Vale/test/quick.vaf @@ -3,6 +3,7 @@ include "../../../fstar/code/arch/x64/X64.Vale.InsBasic.vaf" module Quick #verbatim{:interface}{:implementation} +open Defs_s open Words_s open X64.Machine_s open X64.Vale