diff options
| -rw-r--r-- | src/gen_lib/sail_values.lem | 193 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 12 | ||||
| -rw-r--r-- | src/gen_lib/vector.lem | 4 | ||||
| -rw-r--r-- | src/pretty_print.ml | 310 | ||||
| -rw-r--r-- | src/rewriter.ml | 30 |
5 files changed, 328 insertions, 221 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 00b3e3ab..2104d072 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -4,26 +4,22 @@ open import Vector open import Arch let to_bool = function - | B0 -> false - | B1 -> true -(* | BU -> assert false *) + | O -> false + | I -> true end -let get_start (Vector _ s) = s -let length (Vector bs _) = length bs +let get_start (V _ s _) = s +let length (V bs _ _) = length bs let write_two_regs r1 r2 vec = let size = length_reg r1 in let start = get_start vec in let vsize = length vec in - let r1_v = - (slice vec) - start - ((if is_inc then size - start else start - size) - 1) in + let r1_v = slice vec start ((if defaultDir then size - start else start - size) - 1) in let r2_v = (slice vec) - (if is_inc then size - start else start - size) - (if is_inc then vsize - start else start - vsize) in + (if defaultDir then size - start else start - size) + (if defaultDir then vsize - start else start - vsize) in write_reg r1 r1_v >> write_reg r2 r2_v let rec replace bs ((n : nat),b') = match (n,bs) with @@ -32,57 +28,82 @@ let rec replace bs ((n : nat),b') = match (n,bs) with | (n+1, b::bs) -> b :: replace bs (n,b') end -let make_indexed_vector entries default start length = - let default = match default with Nothing -> BU | Just v -> v end in - Vector (List.foldl replace (replicate length default) entries) start +let make_indexed_vector_reg entries default start length = + let (Just v) = default in + V (List.foldl replace (replicate length v) entries) start + +let make_indexed_vector_bit entries default start length = + let default = match default with Nothing -> U | Just v -> v end in + V (List.foldl replace (replicate length default) entries) start + +let make_bitvector_undef length = + V (replicate length U) 0 true -let vector_concat (Vector bs start) (Vector bs' _) = Vector(bs ++ bs') start +let vector_concat (V bs start is_inc) (V bs' _ _) = + V(bs ++ bs') start is_inc -let has_undef (Vector bs _) = List.any (function BU -> true | _ -> false end) bs +let (^^) = vector_concat -let most_significant (Vector bs _) = - let (b :: _) = bs in b +let has_undef (V bs _ _) = List.any (function U -> true | _ -> false end) bs + +let most_significant (V bs _ _) = let (b :: _) = bs in b let bitwise_not_bit = function - | B1 -> B0 - | B0 -> B1 - | _ -> BU + | I -> O + | O -> I + | _ -> U end -let bitwise_not (Vector bs start) = - Vector (List.map bitwise_not_bit bs) start +let (~) = bitwise_not_bit + +let bitwise_not (V bs start is_inc) = + V (List.map bitwise_not_bit bs) start is_inc -let bool_to_bit b = if b then B1 else B0 +let bool_to_bit b = if b then I else O let bitwise_binop_bit op = function - | (BU,_) -> BU (*Do we want to do this or to respect | of B1 and & of B0 rules?*) - | (_,BU) -> BU (*Do we want to do this or to respect | of B1 and & of B0 rules?*) + | (U,_) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*) + | (_,U) -> U (*Do we want to do this or to respect | of I and & of B0 rules?*) | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y)) end +val bitwise_and_bit : bit * bit -> bit let bitwise_and_bit = bitwise_binop_bit (&&) + +val bitwise_or_bit : bit * bit -> bit let bitwise_or_bit = bitwise_binop_bit (||) + +val bitwise_xor_bit : bit * bit -> bit let bitwise_xor_bit = bitwise_binop_bit xor -let bitwise_binop op (Vector bsl start, Vector bsr _) = +val (&.) : bit -> bit -> bit +let (&.) x y = bitwise_and_bit (x,y) + +val (|.) : bit -> bit -> bit +let (|.) x y = bitwise_or_bit (x,y) + +val (+.) : bit -> bit -> bit +let (+.) x y = bitwise_xor_bit (x,y) + +let bitwise_binop op (V bsl start is_inc, V bsr _ _) = let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in - Vector (reverse revbs) start + V (reverse revbs) start is_inc let bitwise_and = bitwise_binop (&&) let bitwise_or = bitwise_binop (||) let bitwise_xor = bitwise_binop xor -let unsigned (Vector bs _ as v) : integer = +let unsigned (V bs _ _ as v) : integer = match has_undef v with | true -> fst (List.foldl - (fun (acc,exp) b -> (acc + (if b = B1 then integerPow 2 exp else 0),exp +1)) (0,0) bs) + (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs) end let signed v = match most_significant v with - | B1 -> 0 - (1 + (unsigned (bitwise_not v))) - | B0 -> unsigned v + | I -> 0 - (1 + (unsigned (bitwise_not v))) + | O -> unsigned v end let to_num sign = if sign then signed else unsigned @@ -120,35 +141,36 @@ let rec divide_by_2 bs i (n : integer) = then bs else if (n mod 2 = 1) - then divide_by_2 (replace bs (i,B1)) (i - 1) (n / 2) + then divide_by_2 (replace bs (i,I)) (i - 1) (n / 2) else divide_by_2 bs (i-1) (n div 2) let rec add_one_bit bs co i = if i < 0 then bs else match (nth bs i,co) with - | (B0,false) -> replace bs (i,B1) - | (B0,true) -> add_one_bit (replace bs (i,B1)) true (i-1) - | (B1,false) -> add_one_bit (replace bs (i,B0)) true (i-1) - | (B1,true) -> add_one_bit bs true (i-1) + | (O,false) -> replace bs (i,I) + | (O,true) -> add_one_bit (replace bs (i,I)) true (i-1) + | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1) + | (I,true) -> add_one_bit bs true (i-1) (* | Vundef,_ -> assert false*) end -let to_vec (len,(n : integer)) = - let bs = List.replicate len B0 in +let to_vec is_inc (len,(n : integer)) = + let bs = List.replicate len O in let start = if is_inc then 0 else len-1 in - if n = 0 then Vector bs start - else if n > 0 - then Vector (divide_by_2 bs (len-1) n) start + if n = 0 then + V bs start is_inc + else if n > 0 then + V (divide_by_2 bs (len-1) n) start is_inc else let abs_bs = divide_by_2 bs (len-1) (abs n) in - let (Vector bs start) = bitwise_not (Vector abs_bs start) in - Vector (add_one_bit bs false (len-1)) start + let (V bs start is_inc) = bitwise_not (V abs_bs start is_inc) in + V (add_one_bit bs false (len-1)) start is_inc -let to_vec_inc = to_vec -let to_vec_dec = to_vec +let to_vec_inc = to_vec true +let to_vec_dec = to_vec false -let to_vec_undef len = - Vector (replicate len BU) (if is_inc then 0 else len-1) +let to_vec_undef is_inc len = + V (replicate len U) (if is_inc then 0 else len-1) is_inc let add = uncurry integerAdd let add_signed = uncurry integerAdd @@ -158,10 +180,10 @@ let modulo = uncurry integerMod let quot = uncurry integerDiv let power = uncurry integerPow -let arith_op_vec op sign size (l,r) = +let arith_op_vec op sign size ((V _ _ is_inc as l),r) = let (l',r') = (to_num sign l, to_num sign r) in let n = op l' r' in - to_vec (size * (length l),n) + to_vec is_inc (size * (length l),n) let add_vec = arith_op_vec integerAdd false 1 let add_vec_signed = arith_op_vec integerAdd true 1 @@ -169,8 +191,8 @@ let minus_vec = arith_op_vec integerMinus false 1 let multiply_vec = arith_op_vec integerMult false 2 let multiply_vec_signed = arith_op_vec integerMult true 2 -let arith_op_vec_range op sign size (l,r) = - arith_op_vec op sign size (l, to_vec (length l,r)) +let arith_op_vec_range op sign size ((V _ _ is_inc as l),r) = + arith_op_vec op sign size (l, to_vec is_inc (length l,r)) let add_vec_range = arith_op_vec_range integerAdd false 1 let add_vec_range_signed = arith_op_vec_range integerAdd true 1 @@ -178,8 +200,8 @@ let minus_vec_range = arith_op_vec_range integerMinus false 1 let mult_vec_range = arith_op_vec_range integerMult false 2 let mult_vec_range_signed = arith_op_vec_range integerMult true 2 -let arith_op_range_vec op sign size (l,r) = - arith_op_vec op sign size (to_vec (length r, l), r) +let arith_op_range_vec op sign size (l,(V _ _ is_inc as r)) = + arith_op_vec op sign size (to_vec is_inc (length r, l), r) let add_range_vec = arith_op_range_vec integerAdd false 1 let add_range_vec_signed = arith_op_range_vec integerAdd true 1 @@ -199,35 +221,35 @@ let add_vec_range_range = arith_op_vec_range_range integerAdd false let add_vec_range_range_signed = arith_op_vec_range_range integerAdd true let minus_vec_range_range = arith_op_vec_range_range integerMinus false -let arith_op_vec_vec_range op sign (l,r) = +let arith_op_vec_vec_range op sign ((V _ _ is_inc as l),r) = let (l',r') = (to_num sign l,to_num sign r) in op l' r' let add_vec_vec_range = arith_op_vec_vec_range integerAdd false let add_vec_vec_range_signed = arith_op_vec_vec_range integerAdd true -let arith_op_vec_bit op sign (size : nat) (l,r) = +let arith_op_vec_bit op sign (size : nat) ((V _ _ is_inc as l),r) = let l' = to_num sign l in - let n = op l' match r with | B1 -> (1 : integer) | _ -> 0 end in - to_vec (length l * size,n) + let n = op l' match r with | I -> (1 : integer) | _ -> 0 end in + to_vec is_inc (length l * size,n) let add_vec_bit = arith_op_vec_bit integerAdd false 1 let add_vec_bit_signed = arith_op_vec_bit integerAdd true 1 let minus_vec_bit = arith_op_vec_bit integerMinus true 1 -let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (l,r) = +let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size ((V _ _ is_inc as l),r) = let len = length l in let act_size = len * size in let (l_sign,r_sign) = (to_num sign l,to_num sign r) in let (l_unsign,r_unsign) = (to_num false l,to_num false r) in let n = op l_sign r_sign in let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_vec (act_size,n) in - let one_more_size_u = to_vec (act_size + 1,n_unsign) in + let correct_size_num = to_vec is_inc (act_size,n) in + let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in let overflow = if n <= get_max_representable_in sign len && n >= get_min_representable_in sign len - then B0 else B1 in + then O else I in let c_out = most_significant one_more_size_u in (correct_size_num,overflow,c_out) @@ -238,23 +260,24 @@ let minus_overflow_vec_signed = arith_op_overflow_vec integerMinus true 1 let mult_overflow_vec = arith_op_overflow_vec integerMult false 2 let mult_overflow_vec_signed = arith_op_overflow_vec integerMult true 2 -let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : nat) (l,r_bit) = +let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : nat) + ((V _ _ is_inc as l),r_bit) = let act_size = length l * size in let l' = to_num sign l in let l_u = to_num false l in let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) + | I -> (op l' 1, op l_u 1, true) + | O -> (l',l_u,false) end in (* | _ -> assert false *) - let correct_size_num = to_vec (act_size,n) in - let one_larger = to_vec (act_size + 1,nu) in + let correct_size_num = to_vec is_inc (act_size,n) in + let one_larger = to_vec is_inc (act_size + 1,nu) in let overflow = if changed then if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B1 in + then O else I + else I in (correct_size_num,overflow,most_significant one_larger) let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1 @@ -263,17 +286,17 @@ let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true type shift = LL | RR | LLL -let shift_op_vec op (((Vector bs start) as l),r) = +let shift_op_vec op ((V bs start is_inc as l),r) = let len = List.length bs in let n = r in match op with | LL (*"<<"*) -> - let right_vec = Vector (List.replicate n B0) 0 in + let right_vec = V (List.replicate n O) 0 true in let left_vec = slice l n (if is_inc then len + start else start - len) in vector_concat left_vec right_vec | RR (*">>"*) -> let right_vec = slice l start n in - let left_vec = Vector (List.replicate n B0) 0 in + let left_vec = V (List.replicate n O) 0 true in vector_concat left_vec right_vec | LLL (*"<<<"*) -> let left_vec = slice l n (if is_inc then len + start else start - len) in @@ -290,7 +313,7 @@ let rec arith_op_no0 (op : integer -> integer -> integer) (l,r) = then Nothing else Just (op l r) -let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((Vector _ start) as l),r) = +let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((V _ start is_inc) as l),r) = let act_size = length l * size in let (l',r') = (to_num sign l,to_num sign r) in let n = arith_op_no0 op (l',r') in @@ -302,14 +325,14 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((Vecto | _ -> (false,0) end in if representable - then to_vec (act_size,n') - else Vector (List.replicate act_size BU) start + then to_vec is_inc (act_size,n') + else V (List.replicate act_size U) start is_inc let mod_vec = arith_op_vec_no0 integerMod false 1 let quot_vec = arith_op_vec_no0 integerDiv false 1 let quot_vec_signed = arith_op_vec_no0 integerDiv true 1 -let arith_op_overflow_no0_vec op sign size (((Vector _ start) as l),r) = +let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) = let rep_size = length r * size in let act_size = length l * size in let (l',r') = (to_num sign l,to_num sign r) in @@ -325,24 +348,23 @@ let arith_op_overflow_no0_vec op sign size (((Vector _ start) as l),r) = end in let (correct_size_num,one_more) = if representable then - (to_vec (act_size,n'),to_vec (act_size + 1,n_u')) + (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) else - (Vector (List.replicate act_size BU) start, - Vector (List.replicate (act_size + 1) BU) start) in - let overflow = if representable then B0 else B1 in + (V (List.replicate act_size U) start is_inc, + V (List.replicate (act_size + 1) U) start is_inc) in + let overflow = if representable then O else I in (correct_size_num,overflow,most_significant one_more) let quot_overflow_vec = arith_op_overflow_no0_vec integerDiv false 1 let quot_overflow_vec_signed = arith_op_overflow_no0_vec integerDiv true 1 -let arith_op_vec_range_no0 op sign size (l,r) = - arith_op_vec_no0 op sign size (l,to_vec (length l,r)) +let arith_op_vec_range_no0 op sign size ((V _ _ is_inc as l),r) = + arith_op_vec_no0 op sign size (l,to_vec is_inc (length l,r)) let mod_vec_range = arith_op_vec_range_no0 integerMod false 1 let duplicate (bit,length) = - Vector (List.replicate length bit) 0 - + V (List.replicate length bit) 0 true let compare_op op (l,r) = bool_to_bit (op l r) @@ -360,11 +382,12 @@ let lt_vec = compare_op_vec (>) true let gt_vec = compare_op_vec (>) true let lteq_vec = compare_op_vec (<=) true let gteq_vec = compare_op_vec (>=) true + let lt_vec_signed = compare_op_vec (<) true let gt_vec_signed = compare_op_vec (>) true let lteq_vec_signed = compare_op_vec (<=) true let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false +let lt_vec_unsignedp = compare_op_vec (<) false let gt_vec_unsigned = compare_op_vec (>) false let lteq_vec_unsigned = compare_op_vec (<=) false let gteq_vec_unsigned = compare_op_vec (>=) false diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 268077da..dee300ef 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -54,27 +54,27 @@ let rec foreachM_dec (i,stop,by) vars body = -let slice (Vector bs start) n m = +let slice (V bs start is_inc) n m = let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in let (_,suffix) = List.splitAt offset bs in let (subvector,_) = List.splitAt length suffix in - Vector subvector n + V subvector n is_inc -let update (Vector bs start) n m (Vector bs' _) = +let update (V bs start is_inc) n m (V bs' _ _) = let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in let (prefix,_) = List.splitAt offset bs in let (_,suffix) = List.splitAt (offset + length) bs in - Vector (prefix ++ (List.take length bs') ++ suffix) start + V (prefix ++ (List.take length bs') ++ suffix) start is_inc let hd (x :: _) = x val access : forall 'a. vector 'a -> nat -> 'a -let access (Vector bs start) n = +let access (V bs start is_inc) n = if is_inc then nth bs (n - start) else nth bs (start - n) val update_pos : forall 'a. vector 'a -> nat -> 'a -> vector 'a let update_pos v n b = - update v n n (Vector [b] 0) + update v n n (V [b] 0 defaultDir) val read_reg_range : register -> (nat * nat) -> M state (vector bit) let read_reg_range reg (i,j) s = diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index 5f239e37..f409ceb7 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -1,7 +1,7 @@ open import Pervasives -type bit = B0 | B1 | BU -type vector 'a = Vector of list 'a * nat +type bit = O | I | U +type vector 'a = V of list 'a * nat * bool let rec nth xs (n : nat) = match (n,xs) with | (0,x :: xs) -> x diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 897330d7..457effbb 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1803,7 +1803,6 @@ let pp_defs_ocaml f d top_line opens = * PPrint-based sail-to-lem pprinter ****************************************************************************) - let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar @@ -1880,14 +1879,14 @@ let doc_typ_lem, doc_atomic_typ_lem = let doc_lit_lem in_pat (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" - | L_zero -> "B0" - | L_one -> "B1" - | L_false -> "B0" - | L_true -> "B1" + | L_zero -> "O" + | L_one -> "I" + | L_false -> "O" + | L_true -> "I" | L_num i -> if i < 0 then "(0 " ^ string_of_int i ^ ")" else string_of_int i | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) - | L_undef -> "BU" + | L_undef -> "U" | L_string s -> "\"" ^ s ^ "\"") (* typ_doc is the doc for the type being quantified *) @@ -1899,7 +1898,7 @@ let doc_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) = (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let doc_pat_lem = +let doc_pat_lem apat_needed = let rec pat pa = app_pat pa and app_pat ((P_aux(p,(l,annot))) as pa) = match p with | P_app(id, ((_ :: _) as pats)) -> @@ -1919,27 +1918,29 @@ let doc_pat_lem = | P_vector pats -> let non_bit_print () = parens - (separate space [string "Vector"; + (separate space [string "V"; (separate space [brackets (separate_map semi pat pats); - underscore])]) in + underscore;underscore])]) in (match annot with | Base(([],t),_,_,_,_,_) -> if is_bit_vector t - then parens (separate space [string "Vector"; - (separate space [brackets (separate_map semi pat pats); - underscore])]) + then + let ppp = + (separate space) + [string "V";brackets (separate_map semi pat pats);underscore;underscore] in + if apat_needed then parens ppp else ppp else non_bit_print() | _ -> non_bit_print ()) | P_tup pats -> (match pats with | [p] -> pat p | _ -> parens (separate_map comma_sp pat pats)) - | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in lem*) + | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in lem*) in pat let doc_exp_lem, doc_let_lem = - let rec top_exp (E_aux (e, (_,annot))) = - let exp = top_exp in + let rec top_exp (aexp_needed : bool) (E_aux (e, (_,annot))) = + let exp = top_exp true in match e with | E_assign((LEXP_aux(le_act,tannot) as le),e) -> (* can only be register writes *) @@ -1963,17 +1964,24 @@ let doc_exp_lem, doc_let_lem = | _ -> [string "write_reg";doc_lexp_deref_lem le;exp e] ) | E_vector_append(l,r) -> - parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) + let epp = (separate space [exp l;string "^^";exp r]) in + if aexp_needed then parens epp else epp | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) | E_if(c,t,e) -> - parens ( - (separate space [string "if";string "to_bool";parens (exp c)]) ^/^ - (prefix 2 1 (string "then") (exp t)) ^/^ - (prefix 2 1 (string "else") (exp e)) - ) ^^ hardline + let (E_aux (_,(_,cannot))) = c in + let epp = + group ( + (match cannot with + | Base ((_,({t = Tid "bit"})),_,_,_,_,_) -> + separate space [string "if";string "to_bool";exp c] + | _ -> separate space [string "if";exp c]) + ^/^ + (prefix 2 1 (string "then") (exp t)) ^^ (break 1) ^^ + (prefix 2 1 (string "else") (exp e))) in + if aexp_needed then parens epp else epp | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> failwith "E_for should have been removed till now" - | E_let(leb,e) -> (let_exp leb) ^^ space ^^ string "in" ^/^ (exp e) + | E_let(leb,e) -> let_exp leb ^^ space ^^ string "in" ^/^ top_exp false e | E_app(f,args) -> (match f with (* temporary hack to make the loop body a function of the temporary variables *) @@ -1985,22 +1993,35 @@ let doc_exp_lem, doc_let_lem = match vars with | [v] -> v | _ -> parens (separate comma vars) in - (separate space) - [string loopf;exp indices;exp e5] ^/^ - parens((prefix 2 1) - (separate space [string "fun";exp id;varspp;arrow]) - (exp body) - ) + (prefix 2 1) + (parens ((separate space) [string loopf;exp indices;exp e5])) + (parens + ((prefix 1 1) + (separate space [string "fun";exp id;varspp;arrow]) + (exp body) + ) + ) | _ -> let call = match annot with - | Base(_,External (Some n),_,_,_,_) -> string n + | Base(_,External (Some n),_,_,_,_) -> + (match n with + | "bitwise_not_bit" -> string "~" + | _ -> string n) | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f | _ -> doc_id_lem f in - parens (doc_unop call (parens (separate_map comma exp args))) + let epp = + (doc_unop call) + (match args with + | [a] -> exp a + | args -> parens (separate_map comma exp args)) in + if aexp_needed then parens epp else epp ) - | E_vector_access(v,e) -> separate space [string "access";exp v;exp e] + | E_vector_access(v,e) -> + let epp = separate space [string "access";exp v;exp e] in + if aexp_needed then parens epp else epp | E_vector_subrange(v,e1,e2) -> - parens ((string "slice") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) + let epp = (string "slice") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2) in + if aexp_needed then parens epp else epp | E_field((E_aux(_,(_,fannot)) as fexp),id) -> (match fannot with | Base((_,{t= Tapp("register",_)}),_,_,_,_,_) | @@ -2009,13 +2030,14 @@ let doc_exp_lem, doc_let_lem = | Base((_,{t = Tid "bit"}),_,_,_,_,_) | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> string "read_reg_field_bit" - | _ -> string "read_reg_field" in - parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id_lem id)) + | _ -> string "read_reg_field" in + + let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id_lem id) in + if aexp_needed then parens epp else epp | _ -> exp fexp ^^ dot ^^ doc_id_lem id) | E_block [] -> string "()" - | E_block exps | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - surround 2 1 (string "begin") exps_doc (string "end") + | E_block exps -> failwith "Blocks should have been removed till now." + | E_nondet exps -> failwith "Nondet blocks not supported." | E_id id -> (match annot with | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) -> @@ -2033,30 +2055,32 @@ let doc_exp_lem, doc_let_lem = | _ -> string "read_reg_field" in separate space [field_f; string reg; string_lit (string field)] | Alias_extract(reg,start,stop) -> - if start = stop - then parens (separate space [string "access";string reg;doc_int start]) - else parens - (separate space [string "slice"; string reg; doc_int start; doc_int stop]) + let epp = + if start = stop then + separate space [string "access";string reg;doc_int start] + else + separate space [string "slice"; string reg; doc_int start; doc_int stop] in + if aexp_needed then parens epp else epp | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; - string reg1; - string reg2]) + let epp = separate space [string "vector_concat";string reg1;string reg2] in + if aexp_needed then parens epp else epp | Alias_extract(reg,start,stop) -> - if start = stop - then - parens - (separate space - [string "access";doc_int start; - parens (string "read_reg" ^^ space ^^ string reg)]) - else - parens - (separate space - [string "slice"; doc_int start; doc_int stop; - parens (string "read_reg" ^^ space ^^ string reg)]) + let epp = + if start = stop then + (separate space) + [string "access";doc_int start; + parens (string "read_reg" ^^ space ^^ string reg)] + else + (separate space) + [string "slice"; doc_int start; doc_int stop; + parens (string "read_reg" ^^ space ^^ string reg)] in + if aexp_needed then parens epp else epp | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; - parens (string "read_reg" ^^ space ^^ string reg1); - parens (string "read_reg" ^^ space ^^ string reg2)])) + let epp = separate space [string "vector_concat"; + parens (string "read_reg" ^^ space ^^ string reg1); + parens (string "read_reg" ^^ space ^^ string reg2)] in + if aexp_needed then parens epp else epp + ) | _ -> doc_id_lem id) | E_lit lit -> doc_lit_lem false lit | E_cast(typ,e) -> @@ -2084,16 +2108,20 @@ let doc_exp_lem, doc_let_lem = | Nconst i -> string_of_big_int i | N2n(_,Some i) -> string_of_big_int i | _ -> if dir then "0" else string_of_int (List.length exps) in - parens (separate space [string "Vector"; brackets (separate_map semi exp exps); - string start])) - | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> + let epp = group (separate space [string "V"; brackets (separate_map (semi) exp exps); + string start;string dir_out]) in + if aexp_needed then parens epp else epp + ) + | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) -> (match annot with | Base((_,t),_,_,_,_,_) -> match t.t with | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _]) | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) -> - let call = string "make_indexed_vector" in + let call = + if is_bit_vector t then (string "make_indexed_vector_bit") + else (string "make_indexed_vector_reg") in let dir = match order.order with | Oinc -> true | _ -> false in let start = match start.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i @@ -2105,35 +2133,70 @@ let doc_exp_lem, doc_let_lem = in let default_string = (match default with - | Def_val_empty -> string "None" - | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in + | Def_val_empty -> string "Nothing" + | Def_val_dec e -> + if is_bit_vector t then + parens (string "Just " ^^ (exp e)) + else + let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in + let n = + match t with + Tapp ("register", + [TA_typ ({t = Tapp ("vector", + TA_nexp {nexp = Nconst i} :: + TA_nexp {nexp = Nconst j} ::_)})]) -> + abs_big_int (sub_big_int i j) + | _ -> + raise (Reporting_basic.err_unreachable dl "nono") in + parens (string "Just " ^^ parens (string ("UndefinedReg " ^ string_of_big_int n)))) in let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in - parens (separate space [call; - (brackets (separate_map semi iexp iexps)); - default_string; - string start; - string size])) + let epp = + (separate space) + [call;(brackets (separate_map semi iexp iexps)); + default_string; + string start; + string size] in + if aexp_needed then parens epp else epp) | E_vector_update(v,e1,e2) -> - separate space [string "update_pos";exp v;exp e1;exp e2] + let epp = separate space [string "update_pos";exp v;exp e1;exp e2] in + if aexp_needed then parens epp else epp | E_vector_update_subrange(v,e1,e2,e3) -> - separate space [string "update";exp v;exp e1;exp e2;exp e3] + let epp = separate space [string "update";exp v;exp e1;exp e2;exp e3] in + if aexp_needed then parens epp else epp | E_list exps -> brackets (separate_map semi exp exps) | E_case(e,pexps) -> - parens - ((prefix 2 1) - (separate space [string "match"; top_exp e; string "with"]) - ((separate_map (break 1) doc_case pexps) ^/^ - (string "end" ^^ hardline)) - ) + let epp = + (prefix 2 1) + (separate space [string "match"; exp e; string "with"]) + (separate_map (break 1) doc_case pexps) ^^ (break 1) ^^ + (string "end" ^^ (break 1)) in + if aexp_needed then parens epp else epp | E_exit e -> separate space [string "exit"; exp e;] | E_app_infix (e1,id,e2) -> - let call = - match annot with - | Base((_,t),External(Some name),_,_,_,_) -> string name - | _ -> doc_id_lem id in - parens (separate space [call; parens (separate_map comma exp [e1;e2])]) + (match annot with + | Base((_,t),External(Some name),_,_,_,_) -> + let epp = match name with + | "bitwise_and_bit" -> separate space [exp e1;string "&.";exp e2] + | "bitwise_or_bit" -> separate space [exp e1;string "|.";exp e2] + | "bitwise_xor_bit" -> separate space [exp e1;string "+.";exp e2] + | "add" -> separate space [exp e1;string "+";exp e2] + | "minus" -> separate space [exp e1;string "-";exp e2] + | "multiply" -> separate space [exp e1;string "*";exp e2] + (* | "lt" -> separate space [exp e1;string "<";exp e2] + | "gt" -> separate space [exp e1;string ">";exp e2] + | "lteq" -> separate space [exp e1;string "<=";exp e2] + | "gteq" -> separate space [exp e1;string ">=";exp e2] + | "lt_vec" -> separate space [exp e1;string "<";exp e2] + | "gt_vec" -> separate space [exp e1;string ">";exp e2] + | "lteq_vec" -> separate space [exp e1;string "<=";exp e2] + | "gteq_vec" -> separate space [exp e1;string ">=";exp e2] *) + | _ -> separate space [string name; parens (separate_map comma exp [e1;e2])] in + if aexp_needed then parens epp else epp + | _ -> + let epp = separate space [doc_id_lem id; parens (separate_map comma exp [e1;e2])] in + if aexp_needed then parens epp else epp) | E_internal_let(lexp, eq_exp, in_exp) -> failwith "E_internal_lets should have been removed till now" (* (separate @@ -2148,32 +2211,29 @@ let doc_exp_lem, doc_let_lem = (match pat with | P_aux (P_wild,_) -> (separate space [exp e1; string ">>"]) ^/^ - exp e2 + top_exp false e2 | _ -> - (separate space [exp e1; string ">>= fun"; doc_pat_lem pat;arrow]) ^/^ - exp e2) + (separate space [exp e1; string ">>= fun"; doc_pat_lem true pat;arrow]) ^/^ + top_exp false e2) | E_internal_return (e1) -> separate space [string "return"; exp e1;] and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(_,pat,e) | LB_val_implicit(pat,e) -> prefix 2 1 - (separate space [string "let"; doc_pat_lem pat; equals]) - (top_exp e) + (separate space [string "let"; doc_pat_lem true pat; equals]) + (top_exp false e) - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp e) + and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp false e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [pipe; doc_pat_lem pat]) (group (top_exp e)) + doc_op arrow (separate space [pipe; doc_pat_lem false pat]) (group (top_exp false e)) and doc_lexp_deref_lem ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_field (le,id) -> parens (separate empty [doc_lexp_deref_lem le;dot;doc_id_lem id]) | LEXP_vector(le,e) -> - parens - ((separate space) - [string "access";parens (doc_lexp_deref_lem le);parens (top_exp e)] - ) + parens ((separate space) [string "access";doc_lexp_deref_lem le;top_exp true e]) | LEXP_id id -> doc_id_lem id | _ -> empty @@ -2219,7 +2279,7 @@ let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem typ) let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op arrow (doc_pat_lem pat) (doc_exp_lem exp)) + group (doc_op arrow (doc_pat_lem false pat) (doc_exp_lem false exp)) let get_id = function | [] -> failwith "FD_function with empty list" @@ -2229,17 +2289,18 @@ let doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),_)) = match fcls with | [] -> failwith "FD_function with empty function list" | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> - prefix 2 1 - (separate space [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id); - (doc_pat_lem pat); - equals]) - (doc_exp_lem exp) + (prefix 2 1) + ((separate space) + [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id); + (doc_pat_lem true pat); + equals]) + (doc_exp_lem false exp) | _ -> let id = get_id fcls in (* let sep = hardline ^^ pipe ^^ space in *) - let clauses = separate_map - (break 1) - (fun fcl -> separate space [pipe;doc_funcl_lem fcl] ) fcls in + let clauses = + (separate_map (break 1)) + (fun fcl -> separate space [pipe;doc_funcl_lem fcl]) fcls in (prefix 2 1) ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"]) (clauses ^/^ string "end") @@ -2271,7 +2332,7 @@ let reg_decls (Defs defs) = let dir_pp = let is_inc = if is_inc then "true" else "false" in - separate space [string "let";string "is_inc";equals;string is_inc] in + separate space [string "let";string "defaultDir";equals;string is_inc] in let (regtypes,rsranges,rsbits,defs) = List.fold_left @@ -2311,7 +2372,8 @@ let reg_decls (Defs defs) = let regs_pp = (prefix 2 1) (separate space [string "type";string "register";equals]) - (separate_map space (fun (reg,_) -> pipe ^^ space ^^ string reg) regs) in + ((separate_map space (fun (reg,_) -> pipe ^^ space ^^ string reg) regs) + ^^ space ^^ pipe ^^ space ^^ string "UndefinedReg of nat") in let regfields_pp = (prefix 2 1) @@ -2335,23 +2397,23 @@ let reg_decls (Defs defs) = )) in let length_pp = + (separate space [string "val";string "length_reg";colon;string "register";arrow;string "nat"]) + ^/^ (prefix 2 1) - (separate space [string "let";string "length_reg";string "reg";equals]) - ( - (prefix 2 1) - (separate space [string "let";string "v";equals;string "match reg with"]) - ((separate_map (break 1)) - (fun (name,typ) -> - let ((n1,n2,_,_),typname) = - match typ with - | Some typname -> (List.assoc typname regtypes,"register_" ^ typname) - | None -> (default,"register") in - separate space [pipe;string name;arrow;string "abs"; - parens (separate space [doc_nexp n2;minus;doc_nexp n1]); - plus;string "1"]) - regs) ^/^ - string "end in" ^/^ - string "natFromInteger v") in + (separate space [string "let";string "length_reg";equals;string "function"]) + (((separate_map (break 1)) + (fun (name,typ) -> + let ((n1,n2,_,_),typname) = + match typ with + | Some typname -> (List.assoc typname regtypes,"register_" ^ typname) + | None -> (default,"register") in + separate space [pipe;string name;arrow;doc_nexp (if is_inc then n2 else n1); + minus;doc_nexp (if is_inc then n1 else n2);plus;string "1"]) + regs) ^/^ + separate space [pipe;string "UndefinedReg n";arrow; + string "failwith \"Trying to compute length of undefined register\""] ^/^ + string "end") in + let field_indices_pp = (prefix 2 1) @@ -2391,6 +2453,8 @@ let field_index_bit_pp = (fun (name,_) -> separate space [pipe;string name;arrow;string "s." ^^ (string (String.lowercase name))]) regs) ^/^ + separate space [pipe;string "UndefinedReg n";arrow; + string "failwith \"Trying to read from undefined register\""] ^/^ string "end" ^^ hardline ) in let write_regstate_pp = @@ -2408,6 +2472,8 @@ let field_index_bit_pp = [string "s";string"with";string (String.lowercase name);equals;string "v"] )] ) regs) ^/^ + separate space [pipe;string "UndefinedReg n";arrow; + string "failwith \"Trying to write to undefined register\""] ^/^ string "end" ^^ hardline ) in (separate (hardline ^^ hardline) @@ -2425,9 +2491,9 @@ let pp_defs_lem f_arch f d top_line opens = (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ ((separate_map hardline) (fun lib -> separate space [string "open import";string lib]) - ("Vector" :: "State" :: "Arch" :: opens)) ^/^ defs); + ("Pervasives" :: "Vector" :: "State" :: "Arch" :: opens)) ^/^ defs); print f_arch (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ ((separate_map hardline) (fun lib -> separate space [string "open import";string lib]) - ["Pervasives";"Vector"]) ^/^ decls) + ["Pervasives";"Assert_extra";"Vector"]) ^/^ decls) diff --git a/src/rewriter.ml b/src/rewriter.ml index d5f10efd..3c4ff5e8 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1057,14 +1057,37 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = else E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let) let rec value ((E_aux (exp_aux,_)) as exp) = - not (effectful exp) && not (updates_vars exp) && + not (effectful exp) (* && not (updates_vars exp) *) && match exp_aux with | E_id _ | E_lit _ -> true | E_tuple es | E_vector es | E_list es -> List.fold_left (&&) true (List.map value es) + + (* the ones below are debatable *) + | E_app (_,es) -> List.fold_left (fun b e -> b && value e) true es + | E_app_infix (e1,_,e2) -> value e1 && value e2 + + | E_cast (_,e) -> value e + | E_vector_indexed (ies,optdefault) -> + List.fold_left (fun b (i,e) -> b && value e) true ies && value_optdefault optdefault + | E_vector_append (e1,e2) + | E_vector_access (e1,e2) -> value e1 && value e2 + | E_vector_subrange (e1,e2,e3) + | E_vector_update (e1,e2,e3) -> value e1 && value e2 && value e3 + | E_vector_update_subrange (e1,e2,e3,e4) -> value e1 && value e2 && value e3 && value e4 + | E_cons (e1,e2) -> value e1 && value e2 + | E_record fexps -> value_fexps fexps + | E_record_update (e1,fexps) -> value e1 && value_fexps fexps + | E_field (e1,_) -> value e1 + | _ -> false +and value_optdefault (Def_val_aux (o,_)) = match o with + | Def_val_empty -> true + | Def_val_dec e -> value e +and value_fexps (FES_aux (FES_Fexps (fexps,_),_)) = + List.fold_left (fun b (FE_aux (FE_Fexp (_,e),_)) -> b && value e) true fexps let only_local_eff (l,(Base ((t_params,t),tag,nexps,eff,effsum,bounds))) = (l,Base ((t_params,t),tag,nexps,eff,eff,bounds)) @@ -1531,11 +1554,6 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = let e = rewrite_var_updates (add_vars (*overwrite*) e vartuple) in let pannot = (Parse_ast.Unknown,simple_annot (gettype e)) in let effs = union_effects effs (geteffs e) in - let p = -(* if overwrite then - mktup_pat vars - else*) - P_aux (P_tup [pat; mktup_pat vars],(Unknown,simple_annot (gettype e))) in let pat' = Pat_aux (Pat_exp (p,e),pannot) in (acc @ [pat'],typ,effs) in List.fold_left f ([],typ,{effect = Eset []}) ps in |