diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt.lem | 33 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 14 | ||||
| -rw-r--r-- | src/pretty_print.ml | 48 | ||||
| -rw-r--r-- | src/rewriter.ml | 212 | ||||
| -rw-r--r-- | src/test/power.sail | 31 |
5 files changed, 181 insertions, 157 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 0b616b7e..8e1e1f67 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -133,25 +133,26 @@ type M 'a = outcome 'a val return : forall 'a. 'a -> M 'a let return a = Done a -val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b -let rec bind m f = match m with +val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b +val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c) + +let rec (>>=) m f = match m with | Done a -> f a - | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> bind (k v) f) - | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> bind (k b) f) - | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (bind k f) - | Write_memv v rs k -> Write_memv v rs (fun b -> bind (k b) f) - | Barrier bk k -> Barrier bk (bind k f) - | Footprint k -> Footprint (bind k f) - | Read_reg reg k -> Read_reg reg (fun v -> bind (k v) f) - | Write_reg reg v k -> Write_reg reg v (bind k f) - | Nondet_choice actions k -> Nondet_choice actions (fun c -> bind (k c) f) + | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> (k v) >>= f) + | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> (k b) >>= f) + | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (k >>= f) + | Write_memv v rs k -> Write_memv v rs (fun b -> (k b) >>= f) + | Barrier bk k -> Barrier bk (k >>= f) + | Footprint k -> Footprint (k >>= f) + | Read_reg reg k -> Read_reg reg (fun v -> (k v) >>= f) + | Write_reg reg v k -> Write_reg reg v (k >>= f) + | Nondet_choice actions k -> Nondet_choice actions (fun c -> (k c) >>= f) | Escape -> Escape end val exit : forall 'a 'e. 'e -> M 'a let exit _ = Escape -let (>>=) = bind let (>>) m n = m >>= fun _ -> n val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) @@ -240,11 +241,11 @@ let read_reg_field reg rfield = val write_reg_field : register -> register_field -> vector bit -> M unit let write_reg_field reg rfield = write_reg_range reg (field_indices rfield) -val read_reg_field_bit : register -> register_field_bit -> M bit -let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) +val read_reg_bitfield : register -> register_bitfield -> M bit +let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) -val write_reg_field_bit : register -> register_field_bit -> bit -> M unit -let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit) +val write_reg_bitfield : register -> register_bitfield -> bit -> M unit +let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) val foreach_inc : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars -> (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 481a4e5b..2681d334 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -329,15 +329,15 @@ 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) = +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 (((V _ start is_inc) 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 + let n = arith_op_no0 op l' r' in let (representable,n') = match n with | Just n' -> @@ -353,13 +353,13 @@ let mod_VVV = arith_op_vec_no0 integerMod false 1 let quot_VVV = arith_op_vec_no0 integerDiv false 1 let quotS_VVV = arith_op_vec_no0 integerDiv true 1 -let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) 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 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 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') -> @@ -380,7 +380,7 @@ let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1 let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1 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)) + arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) let mod_VIV = arith_op_vec_range_no0 integerMod false 1 diff --git a/src/pretty_print.ml b/src/pretty_print.ml index b9b32ac4..1d2c89f3 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1903,45 +1903,33 @@ 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 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)) -> - (match annot with - | Base(_,Constructor _,_,_,_,_) -> - doc_unop (doc_id_lem_ctor true id) (separate_map space pat pats) - | _ -> empty) +let rec doc_pat_lem apat_needed (P_aux (p,(l,annot)) as pa) = match p with + | P_app(id, ((_ :: _) as pats)) -> + (match annot with + | Base(_,Constructor _,_,_,_,_) -> + let ppp = doc_unop (doc_id_lem_ctor true id) + (separate_map space (doc_pat_lem true) pats) in + if apat_needed then parens ppp else ppp + | _ -> empty) | P_lit lit -> doc_lit_lem true lit | P_wild -> underscore | P_id id -> doc_id_lem id - | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_lem id]) - | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_lem typ) + | P_as(p,id) -> parens (separate space [doc_pat_lem true p; string "as"; doc_id_lem id]) + | P_typ(typ,p) -> doc_op colon (doc_pat_lem true p) (doc_typ_lem typ) | P_app(id,[]) -> (match annot with | Base(_,Constructor n,_,_,_,_) -> doc_id_lem_ctor apat_needed id | _ -> empty) | P_vector pats -> - let non_bit_print () = - parens - (separate space [string "V"; - (separate space [brackets (separate_map semi pat pats); - underscore;underscore])]) in - (match annot with - | Base(([],t),_,_,_,_,_) -> - if is_bit_vector t - 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 ()) + let ppp = + (separate space) + [string "V";brackets (separate_map semi (doc_pat_lem true) pats);underscore;underscore] in + if apat_needed then parens ppp else ppp | 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*) - in pat + | [p] -> doc_pat_lem apat_needed p + | _ -> parens (separate_map comma_sp (doc_pat_lem false) pats)) + | P_list pats -> brackets (separate_map semi (doc_pat_lem false) pats) (*Never seen but easy in lem*) let rec getregtyp_annot (Base ((_,t),_,_,_,_,_)) = match t with @@ -2343,7 +2331,7 @@ let doc_exp_lem, doc_let_lem = | "mult_overflow_vec" -> aux2 "multO_VVV" | "mult_overflow_vec_signed" -> aux2 "multSO_VVV" | "quot_overflow_vec" -> aux2 "quotO_VVV" - | "quot_overflow_vec_signed" -> aux2 "quot_SO_VVV" + | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV" | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV" | "minus_overflow_vec_bit" -> aux2 "minusO_VBV" | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV" diff --git a/src/rewriter.ml b/src/rewriter.ml index 1d5efb7a..55c19a41 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -118,10 +118,13 @@ let fix_effsum_fexp (FE_aux (fexp,(l,annot))) = FE_aux (fexp,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) let fix_effsum_fexps (FES_aux (fexps,(l,annot))) = - let (Base (t,tag,nexps,eff,_,bounds)) = annot in - let effsum = match fexps with - | FES_Fexps (fexps,_) -> union_effs (List.map get_effsum_fexp fexps) in - FES_aux (fexps,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) + match annot with + | NoTyp -> + raise ((Reporting_basic.err_unreachable l) ("fix_effsum_fexps missing type information")) + | Base (t,tag,nexps,eff,_,bounds) -> + let effsum = match fexps with + | FES_Fexps (fexps,_) -> union_effs (List.map get_effsum_fexp fexps) in + FES_aux (fexps,(l,(Base (t,tag,nexps,eff,union_effects eff effsum,bounds)))) let fix_effsum_opt_default (Def_val_aux (opt_default,(l,annot))) = let (Base (t,tag,nexps,eff,_,bounds)) = annot in @@ -226,7 +229,7 @@ let explode s = exp (String.length s - 1) [] -let vector_string_to_bit_list lit = +let vector_string_to_bit_list l lit = let hexchar_to_binlist = function | '0' -> ['0';'0';'0';'0'] @@ -245,24 +248,24 @@ let vector_string_to_bit_list lit = | 'D' -> ['1';'1';'0';'1'] | 'E' -> ['1';'1';'1';'0'] | 'F' -> ['1';'1';'1';'1'] - | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "hexchar_to_binlist given unrecognized character") in + | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in let s_bin = match lit with | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex))) | L_bin s_bin -> explode s_bin - | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "s_bin given non vector literal") in + | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in - List.map (function '0' -> L_aux (L_zero, Parse_ast.Unknown) - | '1' -> L_aux (L_one,Parse_ast.Unknown) - | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "binary had non-zero or one")) s_bin + List.map (function '0' -> L_aux (L_zero, Parse_ast.Generated l) + | '1' -> L_aux (L_one,Parse_ast.Generated l) + | _ -> raise (Reporting_basic.err_unreachable (Parse_ast.Generated l) "binary had non-zero or one")) s_bin let rewrite_pat rewriters nmap (P_aux (pat,(l,annot))) = let rewrap p = P_aux (p,(l,annot)) in let rewrite = rewriters.rewrite_pat rewriters nmap in match pat with | P_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let ps = List.map (fun p -> P_aux (P_lit p,(Parse_ast.Unknown,simple_annot {t = Tid "bit"}))) - (vector_string_to_bit_list lit) in + let ps = List.map (fun p -> P_aux (P_lit p,(Generated l,simple_annot {t = Tid "bit"}))) + (vector_string_to_bit_list l lit) in rewrap (P_vector ps) | P_lit _ | P_wild | P_id _ -> rewrap pat | P_as(pat,id) -> rewrap (P_as( rewrite pat, id)) @@ -284,8 +287,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | E_block exps -> rewrap (E_block (List.map rewrite exps)) | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let es = List.map (fun p -> E_aux (E_lit p ,(Parse_ast.Unknown,simple_annot {t = Tid "bit"}))) - (vector_string_to_bit_list lit) in + let es = List.map (fun p -> E_aux (E_lit p ,(Generated l,simple_annot {t = Tid "bit"}))) + (vector_string_to_bit_list l lit) in rewrap (E_vector es) | E_id _ | E_lit _ -> rewrap exp | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp)) @@ -330,7 +333,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body)) | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp)) | E_exit e -> rewrap (E_exit (rewrite e)) - | E_internal_cast ((_,casted_annot),exp) -> + | E_internal_cast ((l,casted_annot),exp) -> let new_exp = rewrite exp in (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*) (match casted_annot,exp with @@ -348,8 +351,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | Odec -> (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) - rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Unknown)), - Parse_ast.Unknown),new_exp)) + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Generated l)), + Generated l),new_exp)) | _ -> new_exp)) | _ -> new_exp) | Base((_,t),_,_,_,_,_),_ -> @@ -361,8 +364,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | Odec -> (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*) - rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Unknown)), - Parse_ast.Unknown), new_exp)) + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Generated l)), + Generated l), new_exp)) | _ -> new_exp) | _ -> new_exp) | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp) @@ -770,9 +773,9 @@ let remove_vector_concat_pat pat = let pat = (fold_pat remove_tannot_in_vector_concats pat) false in - let fresh_name () = + let fresh_name l = let current = fresh_name () in - Id_aux (Id ("__v" ^ string_of_int current), Parse_ast.Unknown) in + Id_aux (Id ("__v" ^ string_of_int current), Generated l) in (* expects that P_typ elements have been removed from AST, that the length of all vectors involved is known, @@ -793,12 +796,12 @@ let remove_vector_concat_pat pat = ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_aux = - (fun (pat,annot) contained_in_p_as -> + (fun (pat,((l,_) as annot)) contained_in_p_as -> match pat with | P_vector_concat pats -> (if contained_in_p_as then P_aux (pat,annot) - else P_aux (P_as (P_aux (pat,annot),fresh_name()),annot)) + else P_aux (P_as (P_aux (pat,annot),fresh_name l),annot)) | _ -> P_aux (pat,annot) ) ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) @@ -811,8 +814,8 @@ let remove_vector_concat_pat pat = (* introduce names for all unnamed child nodes of P_vector_concat *) let name_vector_concat_elements = let p_vector_concat pats = - let aux ((P_aux (p,a)) as pat) = match p with - | P_vector _ -> P_aux (P_as (pat,fresh_name()),a) + let aux ((P_aux (p,((l,_) as a))) as pat) = match p with + | P_vector _ -> P_aux (P_as (pat,fresh_name l),a) (* | P_vector_concat. cannot happen after folding function name_vector_concat_roots *) | _ -> pat in (* this can only be P_as and P_id *) P_vector_concat (List.map aux pats) in @@ -832,11 +835,12 @@ let remove_vector_concat_pat pat = (* build a let-expression of the form "let child = root[i..j] in body" *) let letbind_vec (rootid,rannot) (child,cannot) (i,j) = + let (l,_) = cannot in let index n = let typ = simple_annot {t = Tapp ("atom",[TA_nexp (mk_c (big_int_of_int n))])} in - E_aux (E_lit (L_aux (L_num n,Parse_ast.Unknown)), (Parse_ast.Unknown,typ)) in + E_aux (E_lit (L_aux (L_num n,Parse_ast.Generated l)), (Parse_ast.Generated l,typ)) in let subv = E_aux (E_vector_subrange (E_aux (E_id rootid,rannot),index i,index j),cannot) in - let typ = (Parse_ast.Unknown,simple_annot {t = Tid "unit"}) in + let typ = (Parse_ast.Generated l,simple_annot {t = Tid "unit"}) in let letbind = LB_val_implicit (P_aux (P_id child,cannot),subv) in let (Id_aux (Id rootname,_)) = rootid in let (Id_aux (Id childname,_)) = child in @@ -948,15 +952,17 @@ let remove_vector_concat_pat pat = let remove_vector_concats = let p_vector_concat ps = - let aux acc (P_aux (p,annot)) = match p,annot with + let aux acc (P_aux (p,annot)) = + let (l,_) = annot in + match p,annot with | P_vector ps,_ -> acc @ ps | P_id _, (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) -> - let wild _ = P_aux (P_wild,(Parse_ast.Unknown,simple_annot {t = Tid "bit"})) in + let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in acc @ (List.map wild (range 0 ((int_of_big_int length) - 1))) | P_wild, (_,Base((_,{t = Tapp ("vector", [_;TA_nexp {nexp = Nconst length};_;_])}),_,_,_,_,_)) -> - let wild _ = P_aux (P_wild,(Parse_ast.Unknown,simple_annot {t = Tid "bit"})) in + let wild _ = P_aux (P_wild,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})) in acc @ (List.map wild (range 0 ((int_of_big_int length) - 1))) | P_lit _,(l,_) -> raise (Reporting_basic.err_unreachable l "remove_vector_concats: P_lit pattern in vector-concat pattern") @@ -1059,10 +1065,10 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful let exps' = walker exps in fst ((Envmap.fold (fun (res,effects) i (t,e) -> - let bitlit = E_aux (E_lit (L_aux(L_zero, Parse_ast.Unknown)), - (Parse_ast.Unknown, simple_annot bit_t)) in - let rangelit = E_aux (E_lit (L_aux (L_num 0, Parse_ast.Unknown)), - (Parse_ast.Unknown, simple_annot nat_t)) in + let bitlit = E_aux (E_lit (L_aux(L_zero, Parse_ast.Generated l)), + (Parse_ast.Generated l, simple_annot bit_t)) in + let rangelit = E_aux (E_lit (L_aux (L_num 0, Parse_ast.Generated l)), + (Parse_ast.Generated l, simple_annot nat_t)) in let set_exp = match t.t with | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> bitlit @@ -1075,16 +1081,16 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful [_;_;_;TA_typ ( {t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) -> E_aux (E_vector_indexed([], Def_val_aux(Def_val_dec bitlit, - (Parse_ast.Unknown,simple_annot bit_t))), - (Parse_ast.Unknown, simple_annot t)) + (Parse_ast.Generated l,simple_annot bit_t))), + (Parse_ast.Generated l, simple_annot t)) | _ -> e in let unioneffs = union_effects effects (get_effsum_exp set_exp) in - ([E_aux (E_internal_let (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Unknown)), - (Parse_ast.Unknown, (tag_annot t Emp_intro))), + ([E_aux (E_internal_let (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Generated l)), + (Parse_ast.Generated l, (tag_annot t Emp_intro))), set_exp, - E_aux (E_block res, (Parse_ast.Unknown, (simple_annot_efr unit_t effects)))), - (Parse_ast.Unknown, simple_annot_efr unit_t unioneffs))],unioneffs))) - (E_aux(E_if(c',t',e'),(Unknown, annot))::exps',eff_union_exps exps') new_vars) + E_aux (E_block res, (Parse_ast.Generated l, (simple_annot_efr unit_t effects)))), + (Parse_ast.Generated l, simple_annot_efr unit_t unioneffs))],unioneffs))) + (E_aux(E_if(c',t',e'),(Parse_ast.Generated l, annot))::exps',eff_union_exps exps') new_vars) | e::exps -> (rewrite_rec e)::(walker exps) in rewrap (E_block (walker exps)) @@ -1138,53 +1144,54 @@ let rewrite_defs_ocaml defs = let remove_blocks = - let letbind_wild v body = - let annot_pat = (Parse_ast.Unknown,simple_annot (get_type v)) in - let annot_lb = (Parse_ast.Unknown,simple_annot_efr (get_type v) (get_effsum_exp v)) in - let annot_let = (Parse_ast.Unknown,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + let letbind_wild v body = + let (E_aux (_,(l,_))) = v in + let annot_pat = (Parse_ast.Generated l,simple_annot (get_type v)) in + let annot_lb = (Parse_ast.Generated l,simple_annot_efr (get_type v) (get_effsum_exp v)) in + let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in - let rec f = function - | [] -> E_aux (E_lit (L_aux (L_unit,Unknown)), (Unknown,simple_annot ({t = Tid "unit"}))) + let rec f l = function + | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (Parse_ast.Generated l,simple_annot ({t = Tid "unit"}))) | [e] -> e (* check with Kathy if that annotation is fine *) - | e :: es -> letbind_wild e (f es) in + | e :: es -> letbind_wild e (f l es) in let e_aux = function - | (E_block es,annot) -> f es + | (E_block es,(l,_)) -> f l es | (e,annot) -> E_aux (e,annot) in fold_exp { id_exp_alg with e_aux = e_aux } -let fresh_id annot = +let fresh_id ((l,_) as annot) = let current = fresh_name () in - let id = Id_aux (Id ("__w" ^ string_of_int current), Parse_ast.Unknown) in - let annot_var = (Parse_ast.Unknown,simple_annot (get_type_annot annot)) in + let id = Id_aux (Id ("__w" ^ string_of_int current), Parse_ast.Generated l) in + let annot_var = (Parse_ast.Generated l,simple_annot (get_type_annot annot)) in E_aux (E_id id, annot_var) let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = (* body is a function : E_id variable -> actual body *) match get_type v with | {t = Tid "unit"} -> - let (E_aux (_,annot)) = v in - let e = E_aux (E_lit (L_aux (L_unit,Unknown)),(Unknown,simple_annot unit_t)) in + let (E_aux (_,(l,annot))) = v in + let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(Parse_ast.Generated l,simple_annot unit_t)) in let body = body e in - let annot_pat = (Parse_ast.Unknown,simple_annot unit_t) in + let annot_pat = (Parse_ast.Generated l,simple_annot unit_t) in let annot_lb = annot_pat in - let annot_let = (Parse_ast.Unknown,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in let pat = P_aux (P_wild,annot_pat) in if effectful v then E_aux (E_internal_plet (pat,v,body),annot_let) else E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let) | _ -> - let (E_aux (_,annot)) = v in + let (E_aux (_,((l,_) as annot))) = v in let ((E_aux (E_id id,_)) as e_id) = fresh_id annot in let body = body e_id in - let annot_pat = (Parse_ast.Unknown,simple_annot (get_type v)) in + let annot_pat = (Parse_ast.Generated l,simple_annot (get_type v)) in let annot_lb = annot_pat in - let annot_let = (Parse_ast.Unknown,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in + let annot_let = (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body])) in let pat = P_aux (P_id id,annot_pat) in if effectful v @@ -1299,9 +1306,10 @@ and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp = k (fix_effsum_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) and n_exp_term (new_return : bool) (exp : 'a exp) : 'a exp = + let (E_aux (_,(l,_))) = exp in let exp = if new_return then - E_aux (E_internal_return exp,(Unknown,simple_annot_efr (get_type exp) (get_effsum_exp exp))) + E_aux (E_internal_return exp,(Parse_ast.Generated l,simple_annot_efr (get_type exp) (get_effsum_exp exp))) else exp in (* changed this from n_exp to n_exp_pure so that when we return updated variables @@ -1543,30 +1551,30 @@ let find_updated_vars exp = let swaptyp t (l,(Base ((t_params,_),tag,nexps,eff,effsum,bounds))) = (l,Base ((t_params,t),tag,nexps,eff,effsum,bounds)) -let mktup es = +let mktup l es = if es = [] then - E_aux (E_lit (L_aux (L_unit,Unknown)),(Unknown,simple_annot unit_t)) + E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(Parse_ast.Generated l,simple_annot unit_t)) else let effs = List.fold_left (fun acc e -> union_effects acc (get_effsum_exp e)) {effect = Eset []} es in let typs = List.map get_type es in - E_aux (E_tuple es,(Parse_ast.Unknown,simple_annot_efr {t = Ttup typs} effs)) + E_aux (E_tuple es,(Parse_ast.Generated l,simple_annot_efr {t = Ttup typs} effs)) -let mktup_pat es = +let mktup_pat l es = if es = [] then - P_aux (P_wild,(Unknown,simple_annot unit_t)) + P_aux (P_wild,(Parse_ast.Generated l,simple_annot unit_t)) else let typs = List.map get_type es in let pats = List.map (fun (E_aux (E_id id,_) as exp) -> - P_aux (P_id id,(Unknown,simple_annot (get_type exp)))) es in - P_aux (P_tup pats,(Parse_ast.Unknown,simple_annot {t = Ttup typs})) + P_aux (P_id id,(Parse_ast.Generated l,simple_annot (get_type exp)))) es in + P_aux (P_tup pats,(Parse_ast.Generated l,simple_annot {t = Ttup typs})) type 'a updated_term = | Added_vars of 'a exp * 'a pat | Same_vars of 'a exp -let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = +let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let rec add_vars (*overwrite*) ((E_aux (expaux,annot)) as exp) vars = match expaux with @@ -1602,11 +1610,11 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = else*) E_aux (E_tuple [exp;vars],swaptyp {t = Ttup [get_type exp;get_type vars]} annot) in - let rewrite (E_aux (expaux,annot)) (P_aux (_,pannot) as pat) = + let rewrite (E_aux (expaux,((el,_) as annot))) (P_aux (_,(pl,pannot)) as pat) = match expaux with | E_for(id,exp1,exp2,exp3,order,exp4) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars exp4) in - let vartuple = mktup vars in + let vartuple = mktup el vars in (* let overwrite = match get_type exp with | {t = Tid "unit"} -> true | _ -> false in*) @@ -1615,8 +1623,8 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = | Ord_aux (Ord_inc,_) -> true | Ord_aux (Ord_dec,_) -> false in let funcl = match effectful exp4 with - | false -> Id_aux (Id (if orderb then "foreach_inc" else "foreach_dec"),Unknown) - | true -> Id_aux (Id (if orderb then "foreachM_inc" else "foreachM_dec"),Unknown) in + | false -> Id_aux (Id (if orderb then "foreach_inc" else "foreach_dec"),Parse_ast.Generated el) + | true -> Id_aux (Id (if orderb then "foreachM_inc" else "foreachM_dec"),Parse_ast.Generated el) in let loopvar = let (bf,tf) = match get_type exp1 with | {t = Tapp ("atom",[TA_nexp f])} -> (TA_nexp f,TA_nexp f) @@ -1631,14 +1639,14 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = | {t = Tapp ("atom",[TA_typ {t = Tapp ("range",[TA_nexp bt;TA_nexp tt])}])} -> (TA_nexp bt,TA_nexp tt) | {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in let t = {t = Tapp ("range",if orderb then [bf;tt] else [tf;bt])} in - E_aux (E_id id,(Unknown,simple_annot t)) in - let v = E_aux (E_app (funcl,[loopvar;mktup [exp1;exp2;exp3];exp4;vartuple]), - (Unknown,simple_annot_efr (get_type exp4) (get_effsum_exp exp4))) in + E_aux (E_id id,(Parse_ast.Generated el,simple_annot t)) in + let v = E_aux (E_app (funcl,[loopvar;mktup el [exp1;exp2;exp3];exp4;vartuple]), + (Parse_ast.Generated el,simple_annot_efr (get_type exp4) (get_effsum_exp exp4))) in let pat = (* if overwrite then mktup_pat vars else *) - P_aux (P_tup [pat; mktup_pat vars], (Unknown,simple_annot (get_type v))) in + P_aux (P_tup [pat; mktup_pat pl vars], (Parse_ast.Generated pl,simple_annot (get_type v))) in Added_vars (v,pat) | E_if (c,e1,e2) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) @@ -1646,7 +1654,7 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = if vars = [] then (Same_vars (E_aux (E_if (c,rewrite_var_updates e1,rewrite_var_updates e2),annot))) else - let vartuple = mktup vars in + let vartuple = mktup el vars in (* let overwrite = match get_type exp with | {t = Tid "unit"} -> true | _ -> false in *) @@ -1655,12 +1663,12 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = (* after a-normalisation c shouldn't need rewriting *) let t = get_type e1 in (* let () = assert (simple_annot t = simple_annot (get_type e2)) in *) - let v = E_aux (E_if (c,e1,e2), (Unknown,simple_annot_efr t (eff_union_exps [e1;e2]))) in + let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el,simple_annot_efr t (eff_union_exps [e1;e2]))) in let pat = (* if overwrite then mktup_pat vars else*) - P_aux (P_tup [pat; mktup_pat vars],(Unknown,simple_annot (get_type v))) in + P_aux (P_tup [pat; mktup_pat pl vars],(Parse_ast.Generated pl,simple_annot (get_type v))) in Added_vars (v,pat) | E_case (e1,ps) -> (* after a-normalisation e1 shouldn't need rewriting *) @@ -1672,7 +1680,7 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = let ps = List.map (fun (Pat_aux (Pat_exp (p,e),a)) -> Pat_aux (Pat_exp (p,rewrite_var_updates e),a)) ps in Same_vars (E_aux (E_case (e1,ps),annot)) else - let vartuple = mktup vars in + let vartuple = mktup el vars in (* let overwrite = match get_type exp with | {t = Tid "unit"} -> true | _ -> false in*) @@ -1684,17 +1692,17 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = let etyp = get_type e in let () = assert (simple_annot etyp = simple_annot typ) in let e = rewrite_var_updates (add_vars (*overwrite*) e vartuple) in - let pannot = (Parse_ast.Unknown,simple_annot (get_type e)) in + let pannot = (Parse_ast.Generated pl,simple_annot (get_type e)) in let effs = union_effects effs (get_effsum_exp 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 - let v = E_aux (E_case (e1,ps), (Unknown,simple_annot_efr typ effs)) in + let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl,simple_annot_efr typ effs)) in let pat = (* if overwrite then P_aux (P_tup [mktup_pat vars],(Unknown,simple_annot (get_type v))) else*) - P_aux (P_tup [pat; mktup_pat vars],(Unknown,simple_annot (get_type v))) in + P_aux (P_tup [pat; mktup_pat pl vars],(Parse_ast.Generated pl,simple_annot (get_type v))) in Added_vars (v,pat) | E_assign (lexp,vexp) -> let {effect = Eset effs} = get_effsum_annot annot in @@ -1703,21 +1711,23 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = else (match lexp with | LEXP_aux (LEXP_id id,annot) -> - let pat = P_aux (P_id id,(Unknown,simple_annot (get_type vexp))) in + let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in Added_vars (vexp,pat) | LEXP_aux (LEXP_cast (_,id),annot) -> - let pat = P_aux (P_id id,(Unknown,simple_annot (get_type vexp))) in + let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in Added_vars (vexp,pat) - | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,annot2),i),annot) -> - let eid = E_aux (E_id id,(Unknown,simple_annot (get_type_annot annot2))) in - let vexp = E_aux (E_vector_update (eid,i,vexp),(Unknown,simple_annot (get_type_annot annot))) in - let pat = P_aux (P_id id,(Unknown,simple_annot (get_type vexp))) in + | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) -> + let eid = E_aux (E_id id,(Parse_ast.Generated l2,simple_annot (get_type_annot annot2))) in + let vexp = E_aux (E_vector_update (eid,i,vexp), + (Parse_ast.Generated l1,simple_annot (get_type_annot annot))) in + let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in Added_vars (vexp,pat) - | LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,annot2),i,j),annot) -> - let eid = E_aux (E_id id,(Unknown,simple_annot (get_type_annot annot2))) in + | LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i,j), + ((l,_) as annot)) -> + let eid = E_aux (E_id id,(Parse_ast.Generated l2,simple_annot (get_type_annot annot2))) in let vexp = E_aux (E_vector_update_subrange (eid,i,j,vexp), - (Unknown,simple_annot (get_type_annot annot))) in - let pat = P_aux (P_id id,(Unknown,simple_annot (get_type vexp))) in + (Parse_ast.Generated l,simple_annot (get_type_annot annot))) in + let pat = P_aux (P_id id,(Parse_ast.Generated pl,simple_annot (get_type vexp))) in Added_vars (vexp,pat)) | _ -> (* assumes everying's a-normlised: an expression is a sequence of let-expressions, @@ -1731,23 +1741,25 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = | LB_aux (LB_val_implicit (pat,v),lbannot) -> (match rewrite v pat with | Added_vars (v,pat) -> - let lbannot = (Parse_ast.Unknown,simple_annot (get_type v)) in + let (E_aux (_,(l,_))) = v in + let lbannot = (Parse_ast.Generated l,simple_annot (get_type v)) in (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot)) | Same_vars v -> (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot))) | LB_aux (LB_val_explicit (typ,pat,v),lbannot) -> (match rewrite v pat with | Added_vars (v,pat) -> - let lbannot = (Parse_ast.Unknown,simple_annot (get_type v)) in + let (E_aux (_,(l,_))) = v in + let lbannot = (Parse_ast.Generated l,simple_annot (get_type v)) in (get_effsum_exp v,LB_aux (LB_val_implicit (pat,v),lbannot)) | Same_vars v -> (get_effsum_exp v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in E_aux (E_let (lb,body), - (Unknown,simple_annot_efr (get_type body) (union_effects eff (get_effsum_exp body)))) + (Parse_ast.Generated l,simple_annot_efr (get_type body) (union_effects eff (get_effsum_exp body)))) | E_internal_plet (pat,v,body) -> let body = rewrite_var_updates body in (match rewrite v pat with | Added_vars (v,pat) -> E_aux (E_internal_plet (pat,v,body), - (Unknown,simple_annot_efr (get_type body) (eff_union_exps [v;body]))) + (Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body]))) | Same_vars v -> E_aux (E_internal_plet (pat,v,body),annot)) | E_internal_let (lexp,v,body) -> (* After a-normalisation E_internal_lets can only bind values to names, those don't @@ -1756,10 +1768,10 @@ let rec rewrite_var_updates ((E_aux (expaux,annot)) as exp) = let id = match lexp with | LEXP_aux (LEXP_id id,_) -> id | LEXP_aux (LEXP_cast (_,id),_) -> id in - let pat = P_aux (P_id id, (Parse_ast.Unknown,simple_annot (get_type v))) in - let lbannot = (Parse_ast.Unknown,simple_annot_efr (get_type v) (get_effsum_exp v)) in + let pat = P_aux (P_id id, (Parse_ast.Generated l,simple_annot (get_type v))) in + let lbannot = (Parse_ast.Generated l,simple_annot_efr (get_type v) (get_effsum_exp v)) in let lb = LB_aux (LB_val_implicit (pat,v),lbannot) in - E_aux (E_let (lb,body),(Unknown,simple_annot_efr (get_type body) (eff_union_exps [v;body]))) + E_aux (E_let (lb,body),(Parse_ast.Generated l,simple_annot_efr (get_type body) (eff_union_exps [v;body]))) (* In tail-position there shouldn't be anything we need to do as the terms after * a-normalisation are pure and don't update local variables. There can't be any variable * assignments in tail-position (because of the effect), there could be pure pattern-match diff --git a/src/test/power.sail b/src/test/power.sail index 232f542a..7a66cb20 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -163,7 +163,8 @@ let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 ] -register (bit[32:63]) VRSAVE +(* adapted to make type checker accept SPR definition *) +register (bit[(* 32 *) 0:63]) VRSAVE register (bit[64]) SPRG3 register (bit[64]) SPRG4 @@ -172,7 +173,7 @@ register (bit[64]) SPRG6 register (bit[64]) SPRG7 let (vector <0, 1024, inc, (register<(bit[64])>) >) SPR = - [ 1=XER, 8=LR, 9=CTR(*, 256=VRSAVE (*32 bit, so not 64, caught by type checker at last*)*), 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7 + [ 1=XER, 8=LR, 9=CTR, 256=VRSAVE, 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7 ] (* XXX DCR is implementation-dependent; also, some DCR are only 32 bits @@ -1421,6 +1422,7 @@ function clause execute (Stdux (RS, RA, RB)) = MEMw(EA,8) := GPR[RS] } +(* union ast member (bit[5], bit[5], bit[12], bit[4]) Lq function clause decode (0b111000 : @@ -1448,7 +1450,9 @@ function clause execute (Lq (RTp, RA, DQ, PT)) = GPR[RTp + 1] := bytereverse[64 .. 127] } } +*) +(* union ast member (bit[5], bit[5], bit[14]) Stq function clause decode (0b111110 : @@ -1458,6 +1462,7 @@ function clause decode (0b111110 : 0b10 as instr) = Stq (RSp,RA,DS) + function clause execute (Stq (RSp, RA, DS)) = { (bit[64]) b := 0; @@ -1476,6 +1481,7 @@ function clause execute (Stq (RSp, RA, DS)) = EA := b + EXTS (DS : 0b00); MEMw(EA,8) := RSp } +*) union ast member (bit[5], bit[5], bit[5]) Lhbrx @@ -2223,6 +2229,7 @@ function clause execute (Mullw (RT, RA, RB, OE, Rc)) = if OE then set_SO_OV (overflow) else () } +(* union ast member (bit[5], bit[5], bit[5], bit) Mulhw function clause decode (0b011111 : @@ -2254,7 +2261,9 @@ function clause execute (Mulhw (RT, RA, RB, Rc)) = } else () } +*) +(* union ast member (bit[5], bit[5], bit[5], bit) Mulhwu function clause decode (0b011111 : @@ -2280,7 +2289,9 @@ function clause execute (Mulhwu (RT, RA, RB, Rc)) = } else () } +*) +(* union ast member (bit[5], bit[5], bit[5], bit, bit) Divw function clause decode (0b011111 : @@ -2318,6 +2329,7 @@ function clause execute (Divw (RT, RA, RB, OE, Rc)) = if OE then set_SO_OV (overflow) else () } + union ast member (bit[5], bit[5], bit[5], bit, bit) Divwu function clause decode (0b011111 : @@ -2430,6 +2442,7 @@ function clause execute (Divweu (RT, RA, RB, OE, Rc)) = else (); if OE then set_SO_OV (overflow) else () } +*) union ast member (bit[5], bit[5], bit[5], bit, bit) Mulld @@ -2732,6 +2745,7 @@ function clause execute (Cmpl (BF, L, RA, RB)) = CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO] } +(* union ast member (bit[5], bit[5], bit[16]) Twi function clause decode (0b000011 : @@ -2770,6 +2784,7 @@ function clause execute (Tw (TO, RA, RB)) = if a <_u b & TO[3] then trap () else (); if a >_u b & TO[4] then trap () else () } +*) union ast member (bit[5], bit[5], bit[16]) Tdi @@ -5905,6 +5920,7 @@ function clause decode (0b011111 : function clause execute (Lvsr (VRT, RA, RB)) = () +(* union ast member (bit[5], bit[5], bit[5]) Vpkpx function clause decode (0b000100 : @@ -5927,6 +5943,7 @@ function clause execute (Vpkpx (VRT, VRA, VRB)) = (VR[VRT])[i + 75..i + 79] := (VR[VRB])[i * 2 + 24 .. i * 2 + 28] } + union ast member (bit[5], bit[5], bit[5]) Vpkshss function clause decode (0b000100 : @@ -6005,6 +6022,7 @@ function clause execute (Vpkswus (VRT, VRA, VRB)) = 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuhum function clause decode (0b000100 : @@ -6021,6 +6039,7 @@ function clause execute (Vpkuhum (VRT, VRA, VRB)) = (VR[VRT])[i + 64..i + 71] := (VR[VRB])[i * 2 + 8 .. i * 2 + 15] } + union ast member (bit[5], bit[5], bit[5]) Vpkuhus function clause decode (0b000100 : @@ -6039,6 +6058,7 @@ function clause execute (Vpkuhus (VRT, VRA, VRB)) = (Clamp (EXTZ ((VR[VRB])[i * 2 .. i * 2 + 15]),0,255))[24 .. 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuwum function clause decode (0b000100 : @@ -6055,6 +6075,7 @@ function clause execute (Vpkuwum (VRT, VRA, VRB)) = (VR[VRT])[i + 64..i + 79] := (VR[VRB])[i * 2 + 16 .. i * 2 + 31] } + union ast member (bit[5], bit[5], bit[5]) Vpkuwus function clause decode (0b000100 : @@ -10355,6 +10376,8 @@ function clause decode (0b011111 : Dcbf (L,RA,RB) function clause execute (Dcbf (L, RA, RB)) = () +*) + union ast member Isync @@ -10617,8 +10640,8 @@ function bit illegal_instructions_pred ((ast) instr) = { case (Stfdp(FRSp,RA,DS)) -> (FRSp mod 2 == 1) case (Lfdpx(FRTp,RA,RB)) -> (FRTp mod 2 == 1) case (Stfdpx(FRSp,RA,RB)) -> (FRSp mod 2 == 1) - case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA) - case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1) + (*case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA) + case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1) *) case (Mtspr(RS, spr)) -> ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 256) | (spr == 512) | (spr == 896) | (spr == 898)) |