diff options
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 86 |
1 files changed, 46 insertions, 40 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index b35bc48f..23ce6663 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -101,64 +101,64 @@ let rec default_order (Defs defs) = | (Nneg n, Nconst max) | (Nneg n, N2n(_, Some max))-> (match n.nexp with | Nconst abs_min | N2n(_,Some abs_min) -> - (minus_big_int abs_min), max + (Big_int.negate abs_min), max | _ -> assert false (*Put a better error message here*)) | (Nconst min,Nneg n) | (N2n(_, Some min), Nneg n) -> (match n.nexp with | Nconst abs_max | N2n(_,Some abs_max) -> - min, (minus_big_int abs_max) + min, (Big_int.negate abs_max) | _ -> assert false (*Put a better error message here*)) | (Nneg nmin, Nneg nmax) -> ((match nmin.nexp with - | Nconst abs_min | N2n(_,Some abs_min) -> (minus_big_int abs_min) + | Nconst abs_min | N2n(_,Some abs_min) -> (Big_int.negate abs_min) | _ -> assert false (*Put a better error message here*)), (match nmax.nexp with - | Nconst abs_max | N2n(_,Some abs_max) -> (minus_big_int abs_max) + | Nconst abs_max | N2n(_,Some abs_max) -> (Big_int.negate abs_max) | _ -> assert false (*Put a better error message here*))) | _ -> assert false - in le_big_int min candidate && le_big_int candidate max + in Big_int.less_equal min candidate && Big_int.less_equal candidate max | _ -> assert false (*Rmove me when switch to zarith*) let rec power_big_int b n = - if eq_big_int n zero_big_int - then unit_big_int - else mult_big_int b (power_big_int b (sub_big_int n unit_big_int)) + if Big_int.equal n Big_int.zero + then (Big_int.of_int 1) + else Big_int.mul b (power_big_int b (Big_int.sub n (Big_int.of_int 1))) let unpower_of_2 b = - let two = big_int_of_int 2 in - let four = big_int_of_int 4 in - let eight = big_int_of_int 8 in - let sixteen = big_int_of_int 16 in - let thirty_two = big_int_of_int 32 in - let sixty_four = big_int_of_int 64 in - let onetwentyeight = big_int_of_int 128 in - let twofiftysix = big_int_of_int 256 in - let fivetwelve = big_int_of_int 512 in - let oneotwentyfour = big_int_of_int 1024 in - let to_the_sixteen = big_int_of_int 65536 in - let to_the_thirtytwo = big_int_of_string "4294967296" in - let to_the_sixtyfour = big_int_of_string "18446744073709551616" in - let ck i = eq_big_int b i in - if ck unit_big_int then zero_big_int - else if ck two then unit_big_int + let two = Big_int.of_int 2 in + let four = Big_int.of_int 4 in + let eight = Big_int.of_int 8 in + let sixteen = Big_int.of_int 16 in + let thirty_two = Big_int.of_int 32 in + let sixty_four = Big_int.of_int 64 in + let onetwentyeight = Big_int.of_int 128 in + let twofiftysix = Big_int.of_int 256 in + let fivetwelve = Big_int.of_int 512 in + let oneotwentyfour = Big_int.of_int 1024 in + let to_the_sixteen = Big_int.of_int 65536 in + let to_the_thirtytwo = Big_int.of_string "4294967296" in + let to_the_sixtyfour = Big_int.of_string "18446744073709551616" in + let ck i = Big_int.equal b i in + if ck (Big_int.of_int 1) then Big_int.zero + else if ck two then (Big_int.of_int 1) else if ck four then two - else if ck eight then big_int_of_int 3 + else if ck eight then Big_int.of_int 3 else if ck sixteen then four - else if ck thirty_two then big_int_of_int 5 - else if ck sixty_four then big_int_of_int 6 - else if ck onetwentyeight then big_int_of_int 7 + else if ck thirty_two then Big_int.of_int 5 + else if ck sixty_four then Big_int.of_int 6 + else if ck onetwentyeight then Big_int.of_int 7 else if ck twofiftysix then eight - else if ck fivetwelve then big_int_of_int 9 - else if ck oneotwentyfour then big_int_of_int 10 + else if ck fivetwelve then Big_int.of_int 9 + else if ck oneotwentyfour then Big_int.of_int 10 else if ck to_the_sixteen then sixteen else if ck to_the_thirtytwo then thirty_two else if ck to_the_sixtyfour then sixty_four else let rec unpower b power = - if eq_big_int b unit_big_int + if Big_int.equal b (Big_int.of_int 1) then power - else (unpower (div_big_int b two) (succ_big_int power)) in - unpower b zero_big_int + else (unpower (Big_int.div b two) (Big_int.succ power)) in + unpower b Big_int.zero let is_within_range candidate range constraints = let candidate_actual = match candidate.t with @@ -183,7 +183,7 @@ let is_within_range candidate range constraints = | Tapp("vector", [_; TA_nexp size ; _; _]) -> (match size.nexp with | Nconst i | N2n(_, Some i) -> - if check_in_range (power_big_int (big_int_of_int 2) i) range + if check_in_range (power_big_int (Big_int.of_int 2) i) range then Yes else No | _ -> Maybe) @@ -342,7 +342,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset. | E_let(lebind,e) -> let b,u,s = fv_of_let consider_var bound used set lebind in fv_of_exp consider_var b u s e - | E_internal_let (lexp, exp1, exp2) -> + | E_var (lexp, exp1, exp2) -> let b,u,s = fv_of_lexp consider_var bound used set lexp in let _,used,set = fv_of_exp consider_var bound used set exp1 in fv_of_exp consider_var b used set exp2 @@ -367,13 +367,13 @@ and fv_of_pes consider_var bound used set pes = let bound_g,us_g,set_g = fv_of_exp consider_var bound_p us_p set g in let bound_e,us_e,set_e = fv_of_exp consider_var bound_g us_g set_g e in fv_of_pes consider_var bound us_e set_e pes - + and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with | LB_val(pat,exp) -> let bound_p, us_p = pat_bindings consider_var bound used pat in let _,us_e,set_e = fv_of_exp consider_var bound used set exp in bound_p,Nameset.union us_p us_e,set_e - + and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) = match lexp with | LEXP_id id -> @@ -382,6 +382,8 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) = if Nameset.mem i bound then bound, used, Nameset.add i set else Nameset.add i bound, Nameset.add i used, set + | LEXP_deref exp -> + fv_of_exp consider_var bound used set exp | LEXP_cast(typ,id) -> let used = Nameset.union (free_type_names_tannot consider_var tannot) used in let i = string_of_id id in @@ -432,8 +434,8 @@ let fv_of_type_def consider_var (TD_aux(t,_)) = match t with typ_variants consider_var bindings tunions | TD_enum(id,_,ids,_) -> Nameset.of_list (List.map string_of_id (id::ids)),mt - | TD_register(id,n1,n2,_) -> - init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2 + | TD_bitfield(id,typ,_) -> + init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *) let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) = match t with @@ -577,6 +579,10 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_fixity _ -> mt,mt | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids | DEF_default def -> mt,mt + | DEF_internal_mutrec fdefs -> + let fvs = List.map (fv_of_fun consider_var) fdefs in + List.fold_left Nameset.union Nameset.empty (List.map fst fvs), + List.fold_left Nameset.union Nameset.empty (List.map snd fvs) | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef | DEF_reg_dec rdec -> fv_of_rd consider_var rdec | DEF_comm _ -> mt,mt @@ -621,7 +627,7 @@ let merge_mutrecs defs = | DEF_fundef fundef -> fundef :: fundefs | DEF_internal_mutrec fundefs' -> fundefs' @ fundefs | _ -> - (* let _ = Pretty_print_sail2.pp_defs stderr (Defs [def]) in *) + (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) raise (Reporting_basic.err_unreachable (def_loc def) "Trying to merge non-function definition with mutually recursive functions") in (* let _ = Printf.eprintf " - Merging %s (using %s)\n" (set_to_string binds') (set_to_string uses') in *) |