Skip to content

Commit

Permalink
Remove unncessary iter-variables from premises injected by sidecondit…
Browse files Browse the repository at this point in the history 
…ion pass
  • Loading branch information
@f52985
f52985 committed Jul 17, 2024
1 parent 225e6e4 commit fc947bc
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 12 deletions.
13 changes: 11 additions & 2 deletions spectec/src/middlend/sideconditions.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ variable x and require e=?x. Maybe later.)
open Util
open Source
open Il.Ast
open Il.Free

(* Errors *)

Expand All @@ -25,6 +26,14 @@ let lenE e = match e.it with
| IterE (_, (ListN (ne, _), _)) -> ne
| _ -> LenE e $$ e.at % (NumT NatT $ e.at)

(* Smart constructor for IterPr that removes dead iter-variables *)
let iterPr (pr, (iter, vars)) =
let frees = free_prem pr in
let vars' = List.filter (fun (id, _) ->
Set.mem id.it frees.varid
) vars in
IterPr (pr, (iter, vars'))

let is_null e = CmpE (EqOp, e, OptE None $$ e.at % e.note) $$ e.at % (BoolT $ e.at)
let iffE e1 e2 = IfPr (BinE (EquivOp, e1, e2) $$ e1.at % (BoolT $ e1.at)) $ e1.at
let same_len e1 e2 = IfPr (CmpE (EqOp, lenE e1, lenE e2) $$ e1.at % (BoolT $ e1.at)) $ e1.at
Expand Down Expand Up @@ -106,7 +115,7 @@ let rec t_exp env e : prem list =
->
t_iterexp env iterexp @
let env' = env_under_iter env iterexp in
List.map (fun pr -> IterPr (pr, iterexp) $ e.at) (t_exp env' e1)
List.map (fun pr -> iterPr (pr, iterexp) $ e.at) (t_exp env' e1)

and t_iterexp env (iter, _) = t_iter env iter

Expand Down Expand Up @@ -135,7 +144,7 @@ let rec t_prem env prem = match prem.it with
-> iter_side_conditions env iterexp @
t_iterexp env iterexp @
let env' = env_under_iter env iterexp in
List.map (fun pr -> IterPr (pr, iterexp) $ prem.at) (t_prem env' prem)
List.map (fun pr -> iterPr (pr, iterexp) $ prem.at) (t_prem env' prem)

let t_prems env = List.concat_map (t_prem env)

Expand Down
20 changes: 10 additions & 10 deletions spectec/test-middlend/TEST.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22907,7 +22907,7 @@ relation Instrtype_ok: `%|-%:OK`(context, instrtype)
rule _{C : context, t_1* : valtype*, x* : idx*, t_2* : valtype*, lct* : localtype*}:
`%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x*{x : localidx}, `%`_resulttype(t_2*{t_2 : valtype})))
-- if (|lct*{lct : localtype}| = |x*{x : idx}|)
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{lct : localtype, x : idx}
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{x : idx}
-- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_1*{t_1 : valtype}))
-- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 : valtype}))
-- (if (C.LOCALS_context[x!`%`_idx.0] = lct))*{lct : localtype, x : idx}
Expand Down Expand Up @@ -23192,7 +23192,7 @@ relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx)
`%|-%:%`(C, SUB_subtype(`FINAL%?`_fin(w0), ($idx(typeidx) : typevar <: typeuse)*{typeidx : typeidx}, comptype), OK_oktypeidx(x_0))
-- if (|comptype'*{comptype' : comptype}| = |x*{x : idx}|)
-- if (|comptype'*{comptype' : comptype}| = |x'*{x' : idx}*{x' : idx}|)
-- (if (x!`%`_idx.0 < |C.TYPES_context|))*{comptype' : comptype, x : idx, x' : typeidx}
-- (if (x!`%`_idx.0 < |C.TYPES_context|))*{x : idx}
-- if (|x*{x : idx}| <= 1)
-- (if (x!`%`_idx.0 < x_0!`%`_idx.0))*{x : idx}
-- (if ($unrolldt(C.TYPES_context[x!`%`_idx.0]) = SUB_subtype(`FINAL%?`_fin(?()), ($idx(x') : typevar <: typeuse)*{x' : typeidx}, comptype')))*{comptype' : comptype, x : idx, x' : typeidx}
Expand Down Expand Up @@ -23334,7 +23334,7 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
rule _{C : context, t_11* : valtype*, x_1* : idx*, t_12* : valtype*, t_21* : valtype*, x_2* : idx*, t_22* : valtype*, x* : idx*, t* : valtype*}:
`%|-%<:%`(C, `%->_%%`_instrtype(`%`_resulttype(t_11*{t_11 : valtype}), x_1*{x_1 : localidx}, `%`_resulttype(t_12*{t_12 : valtype})), `%->_%%`_instrtype(`%`_resulttype(t_21*{t_21 : valtype}), x_2*{x_2 : localidx}, `%`_resulttype(t_22*{t_22 : valtype})))
-- if (|t*{t : valtype}| = |x*{x : idx}|)
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{t : valtype, x : idx}
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{x : idx}
-- Resulttype_sub: `%|-%<:%`(C, t_21*{t_21 : valtype}, t_11*{t_11 : valtype})
-- Resulttype_sub: `%|-%<:%`(C, t_12*{t_12 : valtype}, t_22*{t_22 : valtype})
-- if (x*{x : idx} = $setminus(x_2*{x_2 : idx}, x_1*{x_1 : idx}))
Expand Down Expand Up @@ -24071,7 +24071,7 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
`%|-%:%`(C, [instr_1] :: instr_2*{instr_2 : instr}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x_1*{x_1 : localidx} :: x_2*{x_2 : localidx}, `%`_resulttype(t_3*{t_3 : valtype})))
-- if (|init*{init : init}| = |t*{t : valtype}|)
-- if (|init*{init : init}| = |x_1*{x_1 : idx}|)
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{init : init, t : valtype, x_1 : idx}
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{x_1 : idx}
-- Instr_ok: `%|-%:%`(C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x_1*{x_1 : localidx}, `%`_resulttype(t_2*{t_2 : valtype})))
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init : init, t : valtype, x_1 : idx}
-- Instrs_ok: `%|-%:%`($with_locals(C, x_1*{x_1 : localidx}, `%%`_localtype(SET_init, t)*{t : valtype}), instr_2*{instr_2 : instr}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 : valtype}), x_2*{x_2 : localidx}, `%`_resulttype(t_3*{t_3 : valtype})))
Expand Down Expand Up @@ -25042,7 +25042,7 @@ relation Step_read: `%~>%`(config, instr*)
;; 8-reduction.watsup
rule array.new_data-num{z : state, i : nat, n : n, x : idx, y : idx, zt : storagetype, c^n : lit_(zt)^n, mut : mut}:
`%~>%`(`%;%`_config(z, [CONST_instr(I32_numtype, `%`_num_(i)) CONST_instr(I32_numtype, `%`_num_(n)) ARRAY.NEW_DATA_instr(x, y)]), $const(!($cunpack(zt)), $cunpacknum(zt, c))^n{c : lit_(zt)} :: [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))])
-- (if ($cunpack(zt) =/= ?()))^n{c : lit_(zt)}
-- (if ($cunpack(zt) =/= ?()))^n{}
-- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_arraytype(mut, zt)))
-- if ($concat_(syntax byte, $zbytes(zt, c)^n{c : lit_(zt)}) = $data(z, y).BYTES_datainst[i : ((n * $zsize(zt)) / 8)])

Expand Down Expand Up @@ -29520,7 +29520,7 @@ relation Instrtype_ok: `%|-%:OK`(context, instrtype)
rule _{C : context, t_1* : valtype*, x* : idx*, t_2* : valtype*, lct* : localtype*}:
`%|-%:OK`(C, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x*{x : localidx}, `%`_resulttype(t_2*{t_2 : valtype})))
-- if (|lct*{lct : localtype}| = |x*{x : idx}|)
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{lct : localtype, x : idx}
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{x : idx}
-- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_1*{t_1 : valtype}))
-- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 : valtype}))
-- (if (C.LOCALS_context[x!`%`_idx.0] = lct))*{lct : localtype, x : idx}
Expand Down Expand Up @@ -29806,7 +29806,7 @@ relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx)
-- Comptype_ok: `%|-%:OK`(C, comptype)
-- if (|comptype'*{comptype' : comptype}| = |x*{x : idx}|)
-- if (|comptype'*{comptype' : comptype}| = |x'*{x' : idx}*{x' : idx}|)
-- (if (x!`%`_idx.0 < |C.TYPES_context|))*{comptype' : comptype, x : idx, x' : typeidx}
-- (if (x!`%`_idx.0 < |C.TYPES_context|))*{x : idx}
-- if (|x*{x : idx}| <= 1)
-- (if (x!`%`_idx.0 < x_0!`%`_idx.0))*{x : idx}
-- (if ($unrolldt(C.TYPES_context[x!`%`_idx.0]) = SUB_subtype(`FINAL%?`_fin(?()), ($idx(x') : typevar <: typeuse)*{x' : typeidx}, comptype')))*{comptype' : comptype, x : idx, x' : typeidx}
Expand Down Expand Up @@ -29948,7 +29948,7 @@ relation Instrtype_sub: `%|-%<:%`(context, instrtype, instrtype)
rule _{C : context, t_11* : valtype*, x_1* : idx*, t_12* : valtype*, t_21* : valtype*, x_2* : idx*, t_22* : valtype*, x* : idx*, t* : valtype*}:
`%|-%<:%`(C, `%->_%%`_instrtype(`%`_resulttype(t_11*{t_11 : valtype}), x_1*{x_1 : localidx}, `%`_resulttype(t_12*{t_12 : valtype})), `%->_%%`_instrtype(`%`_resulttype(t_21*{t_21 : valtype}), x_2*{x_2 : localidx}, `%`_resulttype(t_22*{t_22 : valtype})))
-- if (|t*{t : valtype}| = |x*{x : idx}|)
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{t : valtype, x : idx}
-- (if (x!`%`_idx.0 < |C.LOCALS_context|))*{x : idx}
-- Resulttype_sub: `%|-%<:%`(C, t_21*{t_21 : valtype}, t_11*{t_11 : valtype})
-- Resulttype_sub: `%|-%<:%`(C, t_12*{t_12 : valtype}, t_22*{t_22 : valtype})
-- if (x*{x : idx} = $setminus(x_2*{x_2 : idx}, x_1*{x_1 : idx}))
Expand Down Expand Up @@ -30709,7 +30709,7 @@ relation Instrs_ok: `%|-%:%`(context, instr*, instrtype)
rule seq{C : context, instr_1 : instr, instr_2* : instr*, t_1* : valtype*, x_1* : idx*, x_2* : idx*, t_3* : valtype*, t_2* : valtype*, init* : init*, t* : valtype*}:
`%|-%:%`(C, [instr_1] :: instr_2*{instr_2 : instr}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x_1*{x_1 : localidx} :: x_2*{x_2 : localidx}, `%`_resulttype(t_3*{t_3 : valtype})))
-- Instr_ok: `%|-%:%`(C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 : valtype}), x_1*{x_1 : localidx}, `%`_resulttype(t_2*{t_2 : valtype})))
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{init : init, t : valtype, x_1 : idx}
-- (if (x_1!`%`_idx.0 < |C.LOCALS_context|))*{x_1 : idx}
-- if (|init*{init : init}| = |x_1*{x_1 : idx}|)
-- if (|init*{init : init}| = |t*{t : valtype}|)
-- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init : init, t : valtype, x_1 : idx}
Expand Down Expand Up @@ -31688,7 +31688,7 @@ relation Step_read: `%~>%`(config, instr*)
rule array.new_data-num{z : state, i : nat, n : n, x : idx, y : idx, zt : storagetype, c^n : lit_(zt)^n, mut : mut}:
`%~>%`(`%;%`_config(z, [CONST_instr(I32_numtype, `%`_num_(i)) CONST_instr(I32_numtype, `%`_num_(n)) ARRAY.NEW_DATA_instr(x, y)]), $const(!($cunpack(zt)), $cunpacknum(zt, c))^n{c : lit_(zt)} :: [ARRAY.NEW_FIXED_instr(x, `%`_u32(n))])
-- where ARRAY_comptype(`%%`_arraytype(mut, zt)) = $expanddt($type(z, x))
-- (if ($cunpack(zt) =/= ?()))^n{c : lit_(zt)}
-- (if ($cunpack(zt) =/= ?()))^n{}
-- where $concat_(syntax byte, $zbytes(zt, c)^n{c : lit_(zt)}) = $data(z, y).BYTES_datainst[i : ((n * $zsize(zt)) / 8)]

;; 8-reduction.watsup
Expand Down

0 comments on commit fc947bc

Please sign in to comment.