diff options
| -rw-r--r-- | lib/mono_rewrites.sail | 47 | ||||
| -rw-r--r-- | src/monomorphise.ml | 89 |
2 files changed, 134 insertions, 2 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 3190003f..a72cdd79 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -16,6 +16,10 @@ val "extz" : forall 'n 'm 'o 'p. (atom('p),atom('m),vector('o, 'n, dec, bit)) -> val extzv : forall 'n 'm 'o 'p. vector('o, 'n, dec, bit) -> vector('p, 'm, dec, bit) effect pure function extzv(v) = extz(sizeof('p), sizeof('m),v) +val "exts" : forall 'n 'm 'o 'p. (atom('p),atom('m),vector('o, 'n, dec, bit)) -> vector('p, 'm, dec, bit) effect pure +val extsv : forall 'n 'm 'o 'p. vector('o, 'n, dec, bit) -> vector('p, 'm, dec, bit) effect pure +function extsv(v) = exts(sizeof('p), sizeof('m),v) + (* Definitions for the rewrites *) val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure @@ -38,8 +42,8 @@ function is_ones_subrange (xs, i, j) = { (xs & m) == m } -val slice_slice_concat : forall 'n 'm 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'm >= 0 & 'p >= 0 & 'q >= 0. - (bits('n), int, atom('p), bits('m), int, atom('q)) -> bits('r) effect pure +val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. + (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure function slice_slice_concat (xs, i, l, ys, i', l') = { let xs = (xs & slice_mask(i,l)) >> i in @@ -47,6 +51,14 @@ function slice_slice_concat (xs, i, l, ys, i', l') = { extzv(xs) << l' | extzv(ys) } +val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. + (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure + +function slice_zeros_concat (xs, i, l, l') = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << l' +} + (* Assumes initial vectors are of equal size *) val subrange_subrange_eq : forall 'n, 'n >= 0. @@ -67,3 +79,34 @@ function subrange_subrange_concat (xs, i, j, ys, i', j') = { extzv(xs) << i' - (j' - 1) | extzv(ys) } +val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_subrange(xs,i,j,shift) = { + let xs = (xs & slice_mask(j,i-j)) >> j in + extzv(xs) << shift +} + +val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_slice(xs,i,l,shift) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << shift +} + +val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function zext_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) +} + +val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function sext_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + extsv(xs) +} diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 72db4c9d..bfa29e6a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2493,6 +2493,7 @@ let rewrite_app env typ (id,args) = if is_append id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in + let is_zeros = is_id env (Id "Zeros") in match args with (* (known-size-vector @ variable-vector) @ variable-vector *) | [E_aux (E_app (append, @@ -2518,6 +2519,29 @@ let rewrite_app env typ (id,args) = E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), (Unknown,None))),(Unknown,None))]) + | [E_aux (E_app (append, + [e1; + E_aux (E_app (slice1, + [vector1; start1; length1]),_)]),_); + E_aux (E_app (slice2, + [vector2; start2; length2]),_)] + when is_append append && is_slice slice1 && is_slice slice2 && + is_constant_vec_typ env (typ_of e1) && + not (is_constant length1 || is_constant length2) -> + let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in + let midsize = nminus size size1 in + let midstart = + if is_order_inc order + then nconstant zero_big_int + else nminus midsize (nconstant unit_big_int) in + let midtyp = vector_typ midstart midsize order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,None))),(Unknown,None))]) (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -2542,6 +2566,29 @@ let rewrite_app env typ (id,args) = E_aux (E_app (mk_id "slice_slice_concat", [vector1; start1; length1; vector2; start2; length2]),(Unknown,None))) + | [E_aux (E_app (append1, + [e1; + E_aux (E_app (slice1, [vector1; start1; length1]),_)]),_); + E_aux (E_app (zeros1, [length2]),_)] + when is_append append1 && is_slice slice1 && is_zeros zeros1 && + is_constant_vec_typ env (typ_of e1) && + not (is_constant length1 || is_constant length2) -> + let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in + let midsize = nminus size size1 in + let midstart = + if is_order_inc order + then nconstant zero_big_int + else nminus midsize (nconstant unit_big_int) in + let midtyp = vector_typ midstart midsize order bittyp in + E_cast (typ, + E_aux (E_app (mk_id "append", + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_zeros_concat", + [vector1; start1; length1; length2]),(Unknown,None))),(Unknown,None))]), + (Unknown,None))) + | _ -> E_app (id,args) else if is_id env (Id "eq_vec") id then @@ -2576,6 +2623,48 @@ let rewrite_app env typ (id,args) = [vector1; start1; end1]) | _ -> E_app (id,args) + else if is_id env (Id "Extend") id || is_id env (Id "ZeroExtend") id then + let is_subrange = is_id env (Id "vector_subrange") in + let is_slice = is_id env (Id "slice") in + let is_zeros = is_id env (Id "Zeros") in + match args with + | (E_aux (E_app (append1, + [E_aux (E_app (subrange1, [vector1; start1; end1]), _); + E_aux (E_app (zeros1, [len1]),_)]),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + when is_subrange subrange1 && is_zeros zeros1 && is_append append1 + -> E_app (mk_id "place_subrange", + [vector1; start1; end1; len1]) + + | (E_aux (E_app (append1, + [E_aux (E_app (slice1, [vector1; start1; length1]), _); + E_aux (E_app (zeros1, [length2]),_)]),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + when is_slice slice1 && is_zeros zeros1 && is_append append1 + -> E_app (mk_id "place_slice", + [vector1; start1; length1; length2]) + + (* If we've already rewritten to slice_slice_concat, we can just drop the + zero extension because it can do it *) + | (E_aux (E_cast (_, (E_aux (E_app (Id_aux (Id "slice_slice_concat",_), args),_))),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + -> E_app (mk_id "slice_slice_concat", args) + + | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] + when is_slice slice1 && not (is_constant length1) -> + E_app (mk_id "zext_slice", [vector1; start1; length1]) + + | _ -> E_app (id,args) + + else if is_id env (Id "SignExtend") id then + let is_slice = is_id env (Id "slice") in + match args with + | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] + when is_slice slice1 && not (is_constant length1) -> + E_app (mk_id "sext_slice", [vector1; start1; length1]) + + | _ -> E_app (id,args) + else E_app (id,args) let rewrite_aux = function |