diff options
| -rw-r--r-- | src/gen_lib/sail_values.lem | 525 | ||||
| -rw-r--r-- | src/pretty_print.ml | 89 | ||||
| -rw-r--r-- | src/pretty_print.mli | 1 | ||||
| -rw-r--r-- | src/process_file.ml | 4 |
4 files changed, 581 insertions, 38 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem new file mode 100644 index 00000000..0d60efce --- /dev/null +++ b/src/gen_lib/sail_values.lem @@ -0,0 +1,525 @@ +open import Pervasives + +type M 's 'a = <| runState : 's -> ('a * 's) |> + +val return : forall 's 'a. 'a -> M 's 'a +let return a = <| runState = (fun s -> (a,s)) |> + +val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b +let bind m f = <| runState = (fun s -> let (a,s) = m.runState s in (f a).runState s) |> + +let (>>=) = bind +let (>>) m n = m >>= fun _ -> n + +(* only expected to be 0, 1, 2; 2 represents undef *) +type bit = Zero | One | Undef +let is_inc = true + +type register = + | CR | CR0 | CR1 + | CTR + | LR + | XER | XER_SO | XER_OV | XER_CA + | GPR0 + | GPR1 + | GPR2 + | GPR3 + | GPR4 + | VRSAVE + | SPRG3 + +type vector = Vector of list bit * nat + +(* auto-generate *) +let GPR = [GPR0;GPR1;GPR2;GPR3;GPR4] + +(* auto-generate *) +type state = + <| cr : vector; + ctr : vector; + lr : vector; + xer : vector; + gpr0 : vector; + gpr1 : vector; + gpr2 : vector; + gpr3 : vector; + gpr4 : vector; + vrsave : vector; + sprg3 : vector |> + +let to_bool = function + | Zero -> false + | One -> true +(* | Undef -> assert false *) + end + +let get_blist (Vector bs _) = bs +let get_start (Vector _ s) = s +let length (Vector bs _) = length bs + +(* auto-generate *) +let length_register : register -> nat = function + | CR -> 32 + | CR0 -> 4 + | CR1 -> 4 + | CTR -> 64 + | LR -> 64 + | XER -> 64 + | XER_SO -> 1 + | XER_OV -> 1 + | XER_CA -> 1 + | GPR0 -> 64 + | GPR1 -> 64 + | GPR2 -> 64 + | GPR3 -> 64 + | GPR4 -> 64 + | VRSAVE -> 32 + | SPRG3 -> 64 +end + +let vector_access (Vector bs start) n = + let (Just b) = if is_inc then List.index bs (n - start) + else List.index bs (start - n) in + b + + +let read_vector_subrange (Vector bs start) 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 + +let write_vector_subrange (Vector bs start) n m (Vector 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 + +(* auto-generate *) +let read_register reg = + <| runState = + fun s -> + let v = match reg with + | CR -> s.cr + | CR0 -> read_vector_subrange s.cr 32 35 + | CR1 -> read_vector_subrange s.cr 36 39 + | CTR -> s.ctr + | LR -> s.lr + | XER -> s.xer + | XER_SO -> read_vector_subrange s.xer 32 32 + | XER_OV -> read_vector_subrange s.xer 33 33 + | XER_CA -> read_vector_subrange s.xer 34 34 + | GPR0 -> s.gpr0 + | GPR1 -> s.gpr1 + | GPR2 -> s.gpr2 + | GPR3 -> s.gpr3 + | GPR4 -> s.gpr4 + | VRSAVE -> s.vrsave + | SPRG3 -> s.sprg3 + end in + (v,s) + |> + + (* auto-generate *) +let write_register reg v = + <| runState = + fun s -> + let s' = + match reg with + | CR -> <| s with cr = write_vector_subrange s.cr 32 64 v |> + | CR0 -> <| s with cr = write_vector_subrange s.cr 32 35 v |> + | CR1 -> <| s with cr = write_vector_subrange s.cr 36 39 v |> + | CTR -> <| s with ctr = write_vector_subrange s.cr 0 64 v |> + | LR -> <| s with lr = write_vector_subrange s.cr 0 64 v |> + | XER -> <| s with xer = write_vector_subrange s.cr 0 64 v |> + | XER_SO -> <| s with xer = write_vector_subrange s.xer 32 32 v |> + | XER_OV -> <| s with xer = write_vector_subrange s.xer 33 33 v |> + | XER_CA -> <| s with xer = write_vector_subrange s.xer 34 34 v |> + | GPR0 -> <| s with gpr0 = write_vector_subrange s.cr 0 64 v |> + | GPR1 -> <| s with gpr1 = write_vector_subrange s.cr 0 64 v |> + | GPR2 -> <| s with gpr2 = write_vector_subrange s.cr 0 64 v |> + | GPR3 -> <| s with gpr3 = write_vector_subrange s.cr 0 64 v |> + | GPR4 -> <| s with gpr4 = write_vector_subrange s.cr 0 64 v |> + | VRSAVE -> <| s with vrsave = write_vector_subrange s.vrsave 32 64 v |> + | SPRG3 -> <| s with sprg3 = write_vector_subrange s.vrsave 0 64 v |> + end in + ((),s') + |> + +let write_two_registers r1 r2 vec = + let size = length_register r1 in + let start = get_start vec in + let vsize = length vec in + let r1_v = read_vector_subrange vec start ((if is_inc then size - start else start - size) - 1) in + let r2_v = + read_vector_subrange + vec (if is_inc then size - start else start - size) + (if is_inc then vsize - start else start - vsize) in + write_register r1 r1_v >> write_register r2 r2_v + + +let rec replace bs ((n : nat),b') = match (n,bs) with + | (_, []) -> [] + | (0, _::bs) -> b' :: bs + | (n+1, b::bs) -> b :: replace bs (n,b') + end + +let make_indexed_vector entries default start length = + let default = match default with Nothing -> Undef | Just v -> v end in + Vector (List.foldl replace (replicate length default) entries) start + +let vector_concat (Vector bs start) (Vector bs' _) = Vector(bs ++ bs') start + +let has_undef (Vector bs _) = List.any (function Undef -> true | _ -> false end) bs + +let most_significant (Vector bs _) = + let (b :: _) = bs in b + +let bitwise_not_bit = function + | One -> Zero + | Zero -> One + | _ -> Undef + end + +let bitwise_not (Vector bs start) = + Vector (List.map bitwise_not_bit bs) start + +let bool_to_bit b = if b then One else Zero + +let bitwise_binop_bit op = function + | (Undef,_) -> Undef (*Do we want to do this or to respect | of One and & of Zero rules?*) + | (_,Undef) -> Undef (*Do we want to do this or to respect | of One and & of Zero rules?*) + | (x,y) -> bool_to_bit (op (to_bool x) (to_bool y)) + end + +let bitwise_and_bit = bitwise_binop_bit (&&) +let bitwise_or_bit = bitwise_binop_bit (||) +let bitwise_xor_bit = bitwise_binop_bit xor + +let bitwise_binop op (Vector bsl start, Vector bsr _) = + let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in + Vector (reverse revbs) start + +let bitwise_and = bitwise_binop (&&) +let bitwise_or = bitwise_binop (||) +let bitwise_xor = bitwise_binop xor + +let unsigned (Vector bs _ as v) : integer = + match has_undef v with + | true -> + fst (List.foldl + (fun (acc,exp) b -> (acc + (if b = One then integerPow 2 exp else 0),exp +1)) (0,0) bs) + end + +let signed v = + match most_significant v with + | One -> 0 - (1 + (unsigned (bitwise_not v))) + | Zero -> unsigned v + end + +let to_num sign = if sign then signed else unsigned + +let max_64u = (integerPow 2 64) - 1 +let max_64 = (integerPow 2 63) - 1 +let min_64 = 0 - (integerPow 2 63) +let max_32u = (4294967295 : integer) +let max_32 = (2147483647 : integer) +let min_32 = (0 - 2147483648 : integer) +let max_8 = (127 : integer) +let min_8 = (0 - 128 : integer) +let max_5 = (31 : integer) +let min_5 = (0 - 32 : integer) + +let get_max_representable_in sign n = + if (n = 64) then match sign with | true -> max_64 | false -> max_64u end + else if (n=32) then match sign with | true -> max_32 | false -> max_32u end + else if (n=8) then max_8 + else if (n=5) then max_5 + else match sign with | true -> integerPow 2 (n -1) + | false -> integerPow 2 n + end + +let get_min_representable_in _ n = + if n = 64 then min_64 + else if n = 32 then min_32 + else if n = 8 then min_8 + else if n = 5 then min_5 + else 0 - (integerPow 2 n) + + +let rec divide_by_2 bs i (n : integer) = + if i < 0 || n = 0 + then bs + else + if (n mod 2 = 1) + then divide_by_2 (replace bs (i,One)) (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 (List.index bs i,co) with + | (Just Zero,false) -> replace bs (i,One) + | (Just Zero,true) -> add_one_bit (replace bs (i,One)) true (i-1) + | (Just One, false) -> add_one_bit (replace bs (i,Zero)) true (i-1) + | (Just One, true) -> add_one_bit bs true (i-1) + (* | Vundef,_ -> assert false*) + end + +let to_vec len (n : integer) = + let bs = List.replicate len Zero 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 + 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 to_vec_undef len = + Vector (replicate len Undef) (if is_inc then 0 else len-1) + +let add = uncurry integerAdd +let add_signed = uncurry integerAdd +let minus = uncurry integerMinus +let multiply = uncurry integerMult +let modulo = uncurry integerMod +let quot = uncurry integerDiv +let power = uncurry integerPow + +let arith_op_vec op sign size (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 + +let add_vec = arith_op_vec integerAdd false 1 +let add_vec_signed = arith_op_vec integerAdd true 1 +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 add_vec_range = arith_op_vec_range integerAdd false 1 +let add_vec_range_signed = arith_op_vec_range integerAdd true 1 +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 add_range_vec = arith_op_range_vec integerAdd false 1 +let add_range_vec_signed = arith_op_range_vec integerAdd true 1 +let minus_range_vec = arith_op_range_vec integerMinus false 1 +let mult_range_vec = arith_op_range_vec integerMult false 2 +let mult_range_vec_signed = arith_op_range_vec integerMult true 2 + +let arith_op_range_vec_range op sign (l,r) = uncurry op (l, to_num sign r) + +let add_range_vec_range = arith_op_range_vec_range integerAdd false +let add_range_vec_range_signed = arith_op_range_vec_range integerAdd true +let minus_range_vec_range = arith_op_range_vec_range integerMinus false + +let arith_op_vec_range_range op sign (l,r) = uncurry op (to_num sign l,r) + +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 (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 l' = to_num sign l in + let n = op l' match r with | One -> (1 : integer) | _ -> 0 end in + to_vec (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 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 overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then Zero else One in + let c_out = most_significant one_more_size_u in + (correct_size_num,overflow,c_out) + +let add_overflow_vec = arith_op_overflow_vec integerAdd false 1 +let add_overflow_vec_signed = arith_op_overflow_vec integerAdd true 1 +let minus_overflow_vec = arith_op_overflow_vec integerMinus false 1 +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 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 + | One -> (op l' 1, op l_u 1, true) + | Zero -> (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 overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then Zero else One + else One in + (correct_size_num,overflow,most_significant one_larger) + +let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1 +let minus_overflow_vec_bit = arith_op_overflow_vec_bit integerMinus false 1 +let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true 1 + +type shift = LL | RR | LLL + +let shift_op_vec op (((Vector bs start) as l),r) = + let len = List.length bs in + let n = r in + match op with + | LL (*"<<"*) -> + let right_vec = Vector (List.replicate n Zero) 0 in + let left_vec = read_vector_subrange l n (if is_inc then len + start else start - len) in + vector_concat left_vec right_vec + | RR (*">>"*) -> + let right_vec = read_vector_subrange l start n in + let left_vec = Vector (List.replicate n Zero) 0 in + vector_concat left_vec right_vec + | LLL (*"<<<"*) -> + let left_vec = read_vector_subrange l n (if is_inc then len + start else start - len) in + let right_vec = read_vector_subrange l start n in + vector_concat left_vec right_vec + end + +let bitwise_leftshift = shift_op_vec LL (*"<<"*) +let bitwise_rightshift = shift_op_vec RR (*">>"*) +let bitwise_rotate = shift_op_vec LLL (*"<<<"*) + +let rec arith_op_no0 (op : integer -> integer -> integer) (l,r) = + if r = 0 + 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 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 + let (representable,n') = + match n with + | Just n' -> + (n' <= get_max_representable_in sign act_size && + n' >= get_min_representable_in sign act_size, n') + | _ -> (false,0) + end in + if representable + then to_vec act_size n' + else Vector (List.replicate act_size Undef) start + +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 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 + let (l_u,r_u) = (to_num false l,to_num false r) in + let n = arith_op_no0 op (l',r') in + let n_u = arith_op_no0 op (l_u,r_u) in + let (representable,n',n_u') = + match (n, n_u) with + | (Just n',Just n_u') -> + ((n' <= get_max_representable_in sign rep_size && + n' >= (get_min_representable_in sign rep_size)), n', n_u') + | _ -> (true,0,0) + end in + let (correct_size_num,one_more) = + if representable then + (to_vec act_size n',to_vec (act_size + 1) n_u') + else + (Vector (List.replicate act_size Undef) start, + Vector (List.replicate (act_size + 1) Undef) start) in + let overflow = if representable then Zero else One 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 mod_vec_range = arith_op_vec_range_no0 integerMod false 1 + +let duplicate (bit,length) = + Vector (List.replicate length bit) 0 + + +let compare_op op (l,r) = bool_to_bit (op l r) + +let lt = compare_op (<) +let gt = compare_op (>) +let lteq = compare_op (<=) +let gteq = compare_op (>=) + + +let compare_op_vec op sign (l,r) = + let (l',r') = (to_num sign l, to_num sign r) in + compare_op op (l',r') + +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 gt_vec_unsigned = compare_op_vec (>) false +let lteq_vec_unsigned = compare_op_vec (<=) false +let gteq_vec_unsigned = compare_op_vec (>=) false + +let compare_op_vec_range op sign (l,r) = + compare_op op ((to_num sign l),r) + +let lt_vec_range = compare_op_vec_range (<) true +let gt_vec_range = compare_op_vec_range (>) true +let lteq_vec_range = compare_op_vec_range (<=) true +let gteq_vec_range = compare_op_vec_range (>=) true + +let compare_op_range_vec op sign (l,r) = + compare_op op (l, (to_num sign r)) + +let lt_range_vec = compare_op_range_vec (<) true +let gt_range_vec = compare_op_range_vec (>) true +let lteq_range_vec = compare_op_range_vec (<=) true +let gteq_range_vec = compare_op_range_vec (>=) true + +let eq (l,r) = bool_to_bit (l = r) +let eq_vec_range (l,r) = eq (to_num false l,r) +let eq_range_vec (l,r) = eq (l, to_num false r) +let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) + +let neq (l,r) = bitwise_not_bit (eq (l,r)) +let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) + diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 7ec83696..a03209c9 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1769,7 +1769,7 @@ let pp_defs_ocaml f d top_line opens = * PPrint-based sail-to-lem pretty printer ****************************************************************************) -let doc_id_ocaml (Id_aux(i,_)) = +let doc_id_lem (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" | Id i -> string (if i.[0] = '\'' || is_number(i.[0]) then "_" ^ i else i) @@ -1783,23 +1783,23 @@ let doc_exp_lem, doc_let_lem = let exp = top_exp read_registers in match e with | E_assign((LEXP_aux(le_act,tannot) as le),e) -> - (match annot with + (match annot with | Base(_,(Emp_local | Emp_set),_,_,_,_) -> (match le_act with | LEXP_id _ | LEXP_cast _ -> (*Setting local variable fully *) - doc_op coloneq (doc_lexp_lem le) (exp e) + doc_op coloneq (doc_lexp_lem true le) (exp e) | LEXP_vector _ -> doc_op (string "<-") (doc_lexp_array_lem le) (exp e) | LEXP_vector_range _ -> - parens ((string "set_vector_range") ^^ space ^^ (doc_lexp_lem le) ^^ space ^^ (exp e))) + doc_lexp_rwrite le e) | _ -> (match le_act with | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> (doc_lexp_rwrite le e) | LEXP_memory _ -> (doc_lexp_fcall le e))) | E_vector_append(l,r) -> - parens (string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r) + parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) | E_if(c,t,E_aux(E_block [], _)) -> string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ @@ -1847,7 +1847,7 @@ let doc_exp_lem, doc_let_lem = | E_app(f,args) -> let call = match annot with | Base(_,External (Some n),_,_,_,_) -> string n - | Base(_,Constructor,_,_,_,_) -> doc_id_ocaml_ctor f + | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i f | _ -> doc_id_lem f in parens (doc_unop call (parens (separate_map comma exp args))) | E_vector_access(v,e) -> @@ -1878,12 +1878,12 @@ let doc_exp_lem, doc_let_lem = | E_id id -> (match annot with | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) -> - string "!" ^^ doc_id_lem id + doc_id_lem id | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),_,_,_,_,_) -> if read_registers then string "(read_register " ^^ doc_id_lem id ^^ string ")" else doc_id_lem id - | Base(_,(Constructor|Enum _),_,_,_,_) -> doc_id_ocaml_ctor id + | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_ocaml_ctor i id | Base((_,t),Alias alias_info,_,_,_,_) -> (match alias_info with | Alias_field(reg,field) -> @@ -1983,7 +1983,7 @@ let doc_exp_lem, doc_let_lem = parens (separate space [call; parens (separate_map comma exp [e1;e2])]) | E_internal_let(lexp, eq_exp, in_exp) -> separate space [string "let"; - doc_lexp_lem lexp; (*Rewriter/typecheck should ensure this is only cast or id*) + doc_lexp_lem true lexp; (*Rewriter/typecheck should ensure this is only cast or id*) equals; string "ref"; exp eq_exp; @@ -2000,53 +2000,70 @@ let doc_exp_lem, doc_let_lem = | LB_val_explicit(ts,pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) + (top_exp true e) | LB_val_implicit(pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) + (top_exp true e) - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp false e) + and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp true e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = - doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) + doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp true e)) - and doc_lexp_lem ((LEXP_aux(lexp,(l,annot))) as le) = - let exp = top_exp false in + and doc_lexp_lem top_call ((LEXP_aux(lexp,(l,annot))) as le) = + let exp = top_exp true in match lexp with - | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ doc_lexp_lem v) ^^ dot ^^ parens (exp e) + | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (exp e) | LEXP_vector_range(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ doc_lexp_lem v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> doc_lexp_lem v ^^ dot ^^ doc_id_lem id - | LEXP_id id -> doc_id_lem id - | LEXP_cast(typ,id) -> (doc_id_lem id) + parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) + | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id + | LEXP_id id + | LEXP_cast(_,id) -> + let name = doc_id_ocaml id in + match annot,top_call with + | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false + | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false -> + string "!" ^^ name + | _ -> name + and doc_lexp_array_lem ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> parens ((string "get_varray") ^^ space ^^ doc_lexp_lem v) ^^ dot ^^ parens (top_exp false e) - | _ -> empty - + | LEXP_vector(v,e) -> + (match annot with + | Base((_,t),_,_,_,_,_) -> + let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in + (match t_act.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> + parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e) + | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)) + | _ -> + parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)) + | _ -> empty + and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = - let exp = top_exp false in - let is_bit = match e_new_v with + let exp = top_exp true in + let (is_bit,is_bitv) = match e_new_v with | E_aux(_,(_,Base((_,t),_,_,_,_,_))) -> (match t.t with | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) | Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) -> - true - | _ -> false) - | _ -> false in + (false,true) + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false) + | _ -> (false,false)) + | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_lem v)) ^^ + (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^ dot ^^ parens (exp e)) (exp e_new_v) | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ - doc_lexp_lem v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) | LEXP_field(v,id) -> - parens ((string "set_register_field") ^^ space ^^ - doc_lexp_lem v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) + parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ + doc_lexp_ocaml false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) | LEXP_id id | LEXP_cast (_,id) -> (match annot with | Base(_,Alias alias_info,_,_,_,_) -> @@ -2062,7 +2079,7 @@ let doc_exp_lem, doc_let_lem = dot ^^ parens (doc_int start)) (exp e_new_v) else - parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) | Alias_pair(reg1,reg2) -> parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) @@ -2070,10 +2087,10 @@ let doc_exp_lem, doc_let_lem = parens (separate space [string "set_register"; doc_id_lem id; exp e_new_v])) and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with - | LEXP_memory(id,args) -> doc_id_lem id ^^ parens (separate_map comma (top_exp false) (args@[e_new_v])) + | LEXP_memory(id,args) -> doc_id_lem id ^^ parens (separate_map comma (top_exp true) (args@[e_new_v])) (* expose doc_exp and doc_let *) - in top_exp false, let_exp + in top_exp true, let_exp let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pat,exp),_)) = group (doc_op arrow (doc_pat_ocaml pat) (doc_exp_lem exp)) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 772258db..4b51db8a 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -10,3 +10,4 @@ val pat_to_string : tannot pat -> string val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit +val pp_defs_lem : out_channel -> tannot defs -> string -> string list -> unit diff --git a/src/process_file.ml b/src/process_file.ml index 443ea9b0..135f0931 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -174,12 +174,12 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo end | Lem_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values";]; + begin Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values";]; close_output_with_check ext_o end | Lem_out (Some lib) -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in - Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"; lib]; + Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values"; lib]; close_output_with_check ext_o | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in |