diff --git a/run_scons.sh b/run_scons.sh index 6fc97dff..5dbbbd3c 100755 --- a/run_scons.sh +++ b/run_scons.sh @@ -5,7 +5,7 @@ set -e -SCONS_PYTHON_MAJOR_MINOR=3.6 +SCONS_PYTHON_MAJOR_MINOR=3 # Windows-only: print out the directory of the Python associated to SCons windows_scons_python_dir () { diff --git a/tools/Vale/src/ast.fs b/tools/Vale/src/ast.fs index 36ec63b1..e65483f8 100644 --- a/tools/Vale/src/ast.fs +++ b/tools/Vale/src/ast.fs @@ -48,6 +48,9 @@ type op = | Bop of bop | TupleOp of typ list option | Subscript +| Slice +| SlicePrefix +| SliceSuffix | Update | Cond | FieldOp of id diff --git a/tools/Vale/src/emit_common_lemmas.fs b/tools/Vale/src/emit_common_lemmas.fs index e54eaec7..e3c98342 100644 --- a/tools/Vale/src/emit_common_lemmas.fs +++ b/tools/Vale/src/emit_common_lemmas.fs @@ -15,6 +15,7 @@ type build_env = proc:proc_decl; loc:loc; is_instruction:bool; + is_no_inline:bool; is_quick:bool; is_operand:bool; is_framed:bool; @@ -69,6 +70,11 @@ and build_code_stmts (env:env) (benv:build_env) (stmts:stmt list):exp = List.fold cons empty (List.rev slist) and build_code_block (env:env) (benv:build_env) (stmts:stmt list):exp = vaApp "Block" [build_code_stmts env benv stmts] +and build_function (env:env) (benv:build_env) (stmts:stmt list):exp = + // printfn "this is where we emit va_Function"; + match benv.proc.pname with + | Id(id) -> vaApp "Function" [EString id; build_code_stmts env benv stmts] + | _ -> internalErr "Function call unexpected ID" (* Build codegen_success value for body of procedure Q *) let rec build_codegen_success_stmt (q:id) (env:env) (s:stmt):exp option list = @@ -255,7 +261,7 @@ let rec build_lemma_stmt (senv:stmt_env) (s:stmt):ghost * bool * stmt list = let codeBody = vaApp "get_whileBody" [code] in let i1 = string (gen_lemma_sym ()) in let i2 = string (gen_lemma_sym ()) in - let (n1, s1, sw1, fw1) = (Reserved ("n" + i1), Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in + let (n1, s1, sw1, fw1) = (Id "loop_ctr", Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in let (sw2, fw2) = (Reserved ("sW" + i2), Reserved ("fW" + i2)) in let (codeCond, codeBody, sCodeVars) = if !fstar then @@ -458,6 +464,7 @@ let build_pre_code_via_transform (loc:loc) (env:env) (benv:build_env) (stmts:stm { fname = Reserved ("transform_" + string_of_id p.pname); fghost = NotGhost; + // finline = benv.binline; ftargs = []; fargs = fParams; fret_name = None; @@ -482,6 +489,7 @@ function method{:opaque} va_code_Q(iii:int, dummy:va_operand_reg, dummy2:va_oper let build_code (loc:loc) (env:env) (benv:build_env) (stmts:stmt list):(loc * decl) list = let p = benv.proc in let isTransform = List_mem_assoc (Id "transform") p.pattrs in + let isNoInline = benv.is_no_inline in let precode = if isTransform then build_pre_code_via_transform loc env benv stmts else [] in if p.pghost = Ghost then [] else let fParams = make_fun_params p.prets p.pargs in @@ -498,6 +506,7 @@ let build_code (loc:loc) (env:env) (benv:build_env) (stmts:stmt list):(loc * dec fbody = if benv.is_instruction then Some (attrs_get_exp (Id "instruction") p.pattrs) else if isTransform then Some (eapply (Reserved "get_result") [vaApp ("transform_" + string_of_id p.pname) (List.map EVar fParams)]) + else if isNoInline then Some(build_function env benv stmts) else Some (build_code_block env benv stmts); fattrs = if benv.is_quick then @@ -753,6 +762,8 @@ let rec build_proc (envBody:env) (env:env) (loc:loc) (p:proc_decl):decls = else [] in let isInstruction = List_mem_assoc (Id "instruction") p.pattrs in + let isNoInline = List_mem_assoc (Id "noInline") p.pattrs in + // printfn "setting no inline: %b" isNoInline; let isOperand = List_mem_assoc (Id "operand") p.pattrs in let codeName prefix = Reserved ("code_" + prefix + (string_of_id p.pname)) in let isQuick = is_quick_body p.pattrs in @@ -786,6 +797,7 @@ let rec build_proc (envBody:env) (env:env) (loc:loc) (p:proc_decl):decls = proc = p; loc = loc; is_instruction = isInstruction; + is_no_inline = isNoInline; is_quick = isQuick; is_operand = isOperand; is_framed = attrs_get_bool (Id "frame") (p.pghost = NotGhost) p.pattrs; diff --git a/tools/Vale/src/emit_dafny_text.fs b/tools/Vale/src/emit_dafny_text.fs index 092b8071..563e8f06 100644 --- a/tools/Vale/src/emit_dafny_text.fs +++ b/tools/Vale/src/emit_dafny_text.fs @@ -87,6 +87,11 @@ let rec string_of_exp_prec prec e = | EApply (e, _, es, _) when is_id e && id_of_exp e = (Id "set") -> ("{" + (String.concat ", " (List.map (r 5) es)) + "}", 90) | EOp (Subscript, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + "]", 90) | EOp (Update, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " := " + (r 90 e3) + "]", 90) + + | EOp (Slice, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + (r 90 e3) + "]", 90) + | EOp (SlicePrefix, [e1; e2; e3], _) -> ((r 90 e1) + "[" + " .. " + (r 90 e2) + "]", 90) + | EOp (SliceSuffix, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + "]", 90) + | 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 (FieldUpdate x, [e1; e2], _) -> ((r 90 e1) + ".(" + (sid x) + " := " + (r 90 e2) + ")", 90) @@ -149,7 +154,7 @@ let rec emit_stmt (ps:print_state) (s:stmt):unit = ps.PrintLine ("ghost var " + (String.concat ", " (List.map string_of_lhs_formal lhss)) + " := " + (string_of_exp e) + ";") | SAssign _ -> emit_stmts ps (eliminate_assign_lhss s) | SLetUpdates _ -> internalErr "SLetUpdates" - | SBlock ss -> notImplemented "block" + | SBlock ss -> emit_block ps ss | SIfElse (_, e, ss1, []) -> ps.PrintLine ("if (" + (string_of_exp e) + ")"); emit_block ps ss1 diff --git a/tools/Vale/src/emit_vale_text.fs b/tools/Vale/src/emit_vale_text.fs index 9b23a027..c7e00528 100644 --- a/tools/Vale/src/emit_vale_text.fs +++ b/tools/Vale/src/emit_vale_text.fs @@ -110,6 +110,11 @@ let rec string_of_exp_prec (prec:int) (e:exp):string = | EOp (Bop _, ([] | [_] | (_::_::_::_)), _) -> internalErr "binary operator" | EOp (Subscript, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + "]", 90) | EOp (Update, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " := " + (r 90 e3) + "]", 90) + + | EOp (Slice, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + (r 90 e3) + "]", 90) + | EOp (SlicePrefix, [e1; e2], _) -> ((r 90 e1) + "[" + " .. " + (r 90 e2) + "]", 90) + | EOp (SliceSuffix, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + "]", 90) + | 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 (FieldUpdate x, [e1; e2], _) -> ((r 90 e1) + ".(" + (sid x) + " := " + (r 90 e2) + ")", 90) diff --git a/tools/Vale/src/lex.fsl b/tools/Vale/src/lex.fsl index c93c053b..119b02ed 100644 --- a/tools/Vale/src/lex.fsl +++ b/tools/Vale/src/lex.fsl @@ -35,6 +35,9 @@ let operatorToken (tok:string) (isCustom:bool) (s:string):(loc -> token) option | "=" -> Some (fun loc -> EQ (loc, (isCustom, s))) | "|" -> Some (fun loc -> BAR (loc, (isCustom, s))) | ":=" -> Some (fun loc -> COLONEQ (loc, (isCustom, s))) + + | ".." -> Some (fun loc -> DOTDOT (loc, (isCustom, s))) + | "@=" -> Some (fun loc -> ATEQ (loc, (isCustom, s))) | "<=" -> Some (fun loc -> LE (loc, (isCustom, s))) | ">=" -> Some (fun loc -> GE (loc, (isCustom, s))) diff --git a/tools/Vale/src/parse.fsy b/tools/Vale/src/parse.fsy index 522ff353..5d4efc62 100644 --- a/tools/Vale/src/parse.fsy +++ b/tools/Vale/src/parse.fsy @@ -57,6 +57,7 @@ let storageAttrs (a:attrs):(var_storage * attrs) = %token PLUS MINUS STAR SLASH PERCENT %token AMPAMP BARBAR LTEQEQ EQEQGT LTEQEQGT %token ATEQ COLONEQ +%token DOTDOT %token HAVOC OLD THIS %token IS THEN ELSE LET IN OUT INOUT REVEAL GHOST INLINE %token TTYPE TYPE OPERAND_TYPE VAR CONST READONLY FUNCTION AXIOM EXTERN PROCEDURE STATIC MODULE IMPORT OPERATOR @@ -171,6 +172,11 @@ Exp1 | Exp1 QLBRACKET Exp RBRACKET { expAt $2 (EOp (Bop BIn, [$3; $1], None)) } | Exp1 LBRACKET Exp RBRACKET { expAt $2 (EOp (Subscript, [$1; $3], None)) } | Exp1 LBRACKET Exp COLONEQ Exp RBRACKET { expAt $2 (EOp (Update, [$1; $3; $5], None)) } + + | Exp1 LBRACKET Exp DOTDOT Exp RBRACKET { expAt $2 (EOp (Slice, [$1; $3; $5], None)) } + | Exp1 LBRACKET DOTDOT Exp RBRACKET { expAt $2 (EOp (SlicePrefix, [$1; $4], None)) } + | Exp1 LBRACKET Exp DOTDOT RBRACKET { expAt $2 (EOp (SliceSuffix, [$1; $3], None)) } + | Exp1 DOT AnyId { expAt $2 (EOp (FieldOp $3, [$1], None)) } | Exp1 DOT AnyId LPAREN Exps RPAREN { expAt $4 (EApply (EVar (exp2id $1 $3, None), None, $5, None)) } | Exp1 DOT LPAREN AnyId COLONEQ Exp RPAREN { expAt $2 (EOp (FieldUpdate $4, [$1; $6], None)) } @@ -233,6 +239,9 @@ OpToken | LTEQEQGT { $1 } | LBRACKET RBRACKET { ($1, (false, "[]")) } | LBRACKET COLONEQ RBRACKET { ($1, (false, "[:=]")) } + + | LBRACKET DOTDOT RBRACKET { ($1, (false, "[..]")) } + | QLBRACKET RBRACKET { ($1, (false, "?[]")) } | DOT ID { ($1, (false, "." + snd $2 )) } | DOT ID COLONEQ { ($1, (false, "." + snd $2 + ":=")) } diff --git a/tools/Vale/src/typechecker.fs b/tools/Vale/src/typechecker.fs index d82f9d5e..904e2c71 100644 --- a/tools/Vale/src/typechecker.fs +++ b/tools/Vale/src/typechecker.fs @@ -1461,6 +1461,48 @@ and infer_exp (env:env) (u:unifier) (e:exp) (expected_typ:typ option):(typ * aex | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (Update, es)) | _ -> internalErr ("EOp Update") ) + | EOp (Slice, [e1; e2; e3], _) -> + ( + let (t1, ae1) = infer_exp_force env u e1 expected_typ in + let x = + match t1 with + | TName (Id x) | TApply (Id x, _) -> x + | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1)) + in + let e = eapply (Operator (x + "[..]")) [e1; e2; e3] in + let (t, ae) = infer_exp env u e expected_typ in + match ae with + | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (Slice, es)) + | _ -> internalErr ("EOp Slice") + ) + | EOp (SlicePrefix, [e1; e2], _) -> + ( + let (t1, ae1) = infer_exp_force env u e1 expected_typ in + let x = + match t1 with + | TName (Id x) | TApply (Id x, _) -> x + | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1)) + in + let e = eapply (Operator (x + "[..]")) [e1; e2; e2] in // repeated e2, probably not the best workaround + let (t, ae) = infer_exp env u e expected_typ in + match ae with + | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (SlicePrefix, es)) + | _ -> internalErr ("EOp SlicePrefix") + ) + | EOp (SliceSuffix, [e1; e2], _) -> + ( + let (t1, ae1) = infer_exp_force env u e1 expected_typ in + let x = + match t1 with + | TName (Id x) | TApply (Id x, _) -> x + | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1)) + in + let e = eapply (Operator (x + "[..]")) [e1; e2; e2] in // repeated e2,probably not the best workaround + let (t, ae) = infer_exp env u e expected_typ in + match ae with + | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (SliceSuffix, es)) + | _ -> internalErr ("EOp SliceSuffix") + ) | EOp (Bop BIn, [e1; e2], _) -> ( let (t2, ae2) = infer_exp_force env u e2 expected_typ in @@ -1931,6 +1973,7 @@ let rec tc_stmt (env:env) (s:stmt):stmt = SIfElse (g, e, b1, b2) | SWhile (e, invs, ed, b) -> let (t, e) = tc_exp env e (Some tBool) in + let env = push_id env (Id "loop_ctr") (TInt (NegInf, Inf)) in let invs = List_mapSnd (fun e -> let (_, e) = tc_exp env e (Some tProp) in e) invs in let ed = mapSnd (List.map (fun e -> let (_, e) = tc_exp env e None in e)) ed in let (_, b) = tc_stmts env b in @@ -2101,6 +2144,10 @@ let tc_decl (env:env) (decl:((loc * decl) * bool)):(env * ((loc * decl) * bool) | (Operator "[]", _) -> err "operator([]) expects two arguments (the first argument must be a named type)" | (Operator "[:=]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _; _]) -> Operator (x + "[:=]") | (Operator "[:=]", _) -> err "operator([:=]) expects three arguments (the first argument must be a named type)" + + | (Operator "[..]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _; _]) -> Operator (x + "[..]") + | (Operator "[..]", _) -> err "operator([..]) expects three arguments (the first argument must be a named type)" + | (Operator "?[]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _]) -> Operator (x + "?[]") | (Operator "?[]", _) -> err "operator(?[]) expects two arguments (the first argument must be a named type)" | (Operator xf, [(_, Some (TName (Id xt) | (TApply (Id xt, _)))); _])