From fca7f935547509f187be90c00e0be818fcacc2f4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 29 Jun 2017 17:07:30 +0100 Subject: Added support for set constraints Also added some additional tests in test/typecheck --- src/ast.ml | 2 ++ src/type_check_new.ml | 23 ++++++++++++++--------- test/typecheck/fail/bv_simple_index_no_cast.sail | 9 +++++++++ test/typecheck/fail/nat_set.sail | 9 +++++++++ test/typecheck/fail/word_width_bytes_mips.sail | 11 +++++++++++ test/typecheck/pass/bv_simple_index.sail | 11 +++++++++++ test/typecheck/pass/bv_simple_index_bit.sail | 9 +++++++++ test/typecheck/pass/nat_set.sail | 8 ++++++++ test/typecheck/pass/set_mark.sail | 6 ++++++ test/typecheck/pass/set_mark2.sail | 5 +++++ test/typecheck/run_tests.sh | 17 +++++++++++++++-- 11 files changed, 99 insertions(+), 11 deletions(-) create mode 100644 test/typecheck/fail/bv_simple_index_no_cast.sail create mode 100644 test/typecheck/fail/nat_set.sail create mode 100644 test/typecheck/fail/word_width_bytes_mips.sail create mode 100644 test/typecheck/pass/bv_simple_index.sail create mode 100644 test/typecheck/pass/bv_simple_index_bit.sail create mode 100644 test/typecheck/pass/nat_set.sail create mode 100644 test/typecheck/pass/set_mark.sail create mode 100644 test/typecheck/pass/set_mark2.sail diff --git a/src/ast.ml b/src/ast.ml index 6710c749..df3098b5 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -172,6 +172,8 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp | NC_nat_set_bounded of kid * (int) list + (* We need this for the new typechecker when as nexp is substituted for an id *) + | NC_set_subst of nexp * int list type diff --git a/src/type_check_new.ml b/src/type_check_new.ml index 5f997409..f33a7db1 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -210,6 +210,8 @@ let string_of_n_constraint = function | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_set_subst (nexp, ns), _) -> + string_of_nexp nexp ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}" | NC_aux (NC_nat_set_bounded (kid, ns), _) -> string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}" @@ -340,9 +342,10 @@ and nc_subst_nexp_aux l sv subst = function | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_nat_set_bounded (kid, ints) as set_nc -> - if compare kid sv = 0 - then typ_error l ("Cannot substitute " ^ string_of_kid sv ^ " into set constraint " ^ string_of_n_constraint (NC_aux (set_nc, l))) - else set_nc + if Kid.compare kid sv = 0 + then NC_set_subst (Nexp_aux (subst, Parse_ast.Unknown), ints) + else set_nc + | NC_set_subst (nexp, ints) -> NC_set_subst (nexp_subst sv subst nexp, ints) let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l) and typ_subst_nexp_aux sv subst = function @@ -784,7 +787,8 @@ end = struct | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2 | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2 | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) - + | NC_set_subst (nexp, ints) -> wf_nexp env nexp + let get_constraints env = env.constraints let add_constraint (NC_aux (_, l) as constr) env = @@ -985,16 +989,17 @@ let rec nexp_constraint var_of (Nexp_aux (nexp, l)) = | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint var_of nexp) | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint var_of nexp) -let nc_constraint var_of (NC_aux (nc, _)) = +let rec nc_constraint var_of (NC_aux (nc, l)) = match nc with | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) | NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) | NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2) - | NC_nat_set_bounded (_, []) -> Constraint.literal false - | NC_nat_set_bounded (kid, (int :: ints)) -> + | NC_nat_set_bounded (kid, ints) -> nc_constraint var_of (NC_aux (NC_set_subst (nvar kid, ints), l)) + | NC_set_subst (_, []) -> Constraint.literal false + | NC_set_subst (nexp, (int :: ints)) -> List.fold_left Constraint.disj - (Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int int))) - (List.map (fun i -> Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int i))) ints) + (Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int int))) + (List.map (fun i -> Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int i))) ints) let rec nc_constraints var_of ncs = match ncs with diff --git a/test/typecheck/fail/bv_simple_index_no_cast.sail b/test/typecheck/fail/bv_simple_index_no_cast.sail new file mode 100644 index 00000000..74f46ab7 --- /dev/null +++ b/test/typecheck/fail/bv_simple_index_no_cast.sail @@ -0,0 +1,9 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +function bool bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/fail/nat_set.sail b/test/typecheck/fail/nat_set.sail new file mode 100644 index 00000000..036183c5 --- /dev/null +++ b/test/typecheck/fail/nat_set.sail @@ -0,0 +1,9 @@ + +function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = +{ + true +} + +let x = test(1) +let y = test(3) +let z = test(4) \ No newline at end of file diff --git a/test/typecheck/fail/word_width_bytes_mips.sail b/test/typecheck/fail/word_width_bytes_mips.sail new file mode 100644 index 00000000..91f3e787 --- /dev/null +++ b/test/typecheck/fail/word_width_bytes_mips.sail @@ -0,0 +1,11 @@ +typedef WordType = enumerate {B; H; W; D} + +(* This fails because it's not true for all combinations of 'r and WordType *) +(* Needs existential types, i.e. return type should be exists Nat 'r, 'r in {1,2,4,8}. [:'r:] *) +function forall Nat 'r, 'r IN {1,2,4,8}. wordWidthBytes((WordType) w) = + switch(w) { + case B -> 1 + case H -> 2 + case W -> 4 + case D -> 8 + } diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail new file mode 100644 index 00000000..72e1b094 --- /dev/null +++ b/test/typecheck/pass/bv_simple_index.sail @@ -0,0 +1,11 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val cast bit -> bool effect pure cast_bit_bool + +function bool bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail new file mode 100644 index 00000000..2ba5b928 --- /dev/null +++ b/test/typecheck/pass/bv_simple_index_bit.sail @@ -0,0 +1,9 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +function bit bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail new file mode 100644 index 00000000..46338353 --- /dev/null +++ b/test/typecheck/pass/nat_set.sail @@ -0,0 +1,8 @@ + +function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = +{ + true +} + +let x = test(1) +let y = test(3) \ No newline at end of file diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail new file mode 100644 index 00000000..59710c46 --- /dev/null +++ b/test/typecheck/pass/set_mark.sail @@ -0,0 +1,6 @@ + +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv + +function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x + +let x = Foo32( (bit[32]) 0) diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail new file mode 100644 index 00000000..c1433058 --- /dev/null +++ b/test/typecheck/pass/set_mark2.sail @@ -0,0 +1,5 @@ +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv + +function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x + +let x = Foo32( (bit[64]) 0) diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index 7fca4770..f33f21ac 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -11,6 +11,9 @@ NC='\033[0m' mkdir -p $DIR/rtpass mkdir -p $DIR/rtfail +pass=0 +fail=0 + for i in `ls $DIR/pass/`; do printf "testing $i expecting pass: " @@ -18,11 +21,15 @@ do then if $DIR/../../sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null; then + (( pass += 2)) printf "${GREEN}pass${NC}\n" else - printf "${YELLOW}pass${NC}\n" + (( fail += 1 )) + (( pass += 1 )) + printf "${YELLOW}pass but failed re-check${NC}\n" fi else + (( fail += 2 )) printf "${RED}fail${NC}\n" fi done @@ -32,13 +39,19 @@ do printf "testing $i expecting fail: " if $DIR/../../sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i; then + (( fail += 2 )) printf "${RED}pass${NC}\n" else if $DIR/../../sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null; then - printf "${YELLOW}fail${NC}\n" + (( fail += 1 )) + (( pass += 1 )) + printf "${YELLOW}fail but passed re-check${NC}\n" else + (( pass += 2 )) printf "${GREEN}fail${NC}\n" fi fi done + +printf "Passed ${pass} out of $(( pass + fail ))\n" -- cgit v1.2.3