Remove sideconditions which are always true (#25)

spectec/src/middlend/sideconditions.ml

@@ -20,10 +20,15 @@ let _error at msg = Source.error at "sideconditions" msg
 
 module Env = Map.Make(String)
 
+(* Smart constructor for LenE that optimizes |x^n| into n *)
+let lenE e = match e.it with
+| IterE (_, (ListN ne, _)) -> ne
+| _ -> LenE e $$ no_region % (NatT $ no_region)
+
 let is_null e = CmpE (EqOp, e, OptE None $$ no_region % e.note) $$ no_region % (BoolT $ e.at)
 let iffE e1 e2 = IfPr (BinE (EquivOp, e1, e2) $$ no_region % (BoolT $ no_region)) $ no_region
-let same_len e1 e2 = IfPr (CmpE (EqOp, LenE e1 $$ no_region % (NatT $ e1.at), LenE e2 $$ no_region % (NatT $ e2.at)) $$ no_region % (BoolT $ no_region)) $ no_region
-let has_len ne e = IfPr (CmpE (EqOp, LenE e $$ no_region % (NatT $ e.at), ne) $$ no_region % (BoolT $ no_region)) $ no_region
+let same_len e1 e2 = IfPr (CmpE (EqOp, lenE e1, lenE e2) $$ no_region % (BoolT $ no_region)) $ no_region
+let has_len ne e = IfPr (CmpE (EqOp, lenE e, ne) $$ no_region % (BoolT $ no_region)) $ no_region
 
 let iter_side_conditions env ((iter, vs) : iterexp) : premise list =
   let iter' = if iter = Opt then Opt else List in
@@ -102,18 +107,30 @@ let rec t_prem env prem = match prem.it with
 
 let t_prems env = List.concat_map (t_prem env)
 
+let is_identity e = match e.it with
+  | CmpE (EqOp, e1, e2) -> Il.Eq.eq_exp e1 e2
+  | _ -> false
+
+(* Is prem always true? *)
+let is_true prem = match prem.it with
+  | IfPr e -> is_identity e
+  | _ -> false
+
 (* Does prem1 obviously imply prem2? *)
 let rec implies prem1 prem2 = Il.Eq.eq_prem prem1 prem2 ||
   match prem2.it with
   | IterPr (prem2', _) -> implies prem1 prem2'
   | _ -> false
 
+let reduce_prems prems = prems
+  |> Util.Lib.List.filter_not is_true
+  |> Util.Lib.List.nub implies
 
 let t_rule' = function
   | RuleD (id, binds, mixop, exp, prems) ->
     let env = List.fold_left (fun env (v, t, _) -> Env.add v.it t env) Env.empty binds in
     let extra_prems = t_prems env prems @ t_exp env exp in
-    let prems' = Util.Lib.List.nub implies (extra_prems @ prems) in
+    let prems' = reduce_prems (extra_prems @ prems) in
     RuleD (id, binds, mixop, exp, prems')
 
 let t_rule x = { x with it = t_rule' x.it }

spectec/src/util/lib.ml

@@ -14,6 +14,9 @@ struct
   let rec nub pred = function
     | [] -> []
     | x::xs -> x :: nub pred (List.filter (fun y -> not (pred x y)) xs)
+
+  let filter_not pred = List.filter (fun x -> not (pred x))
+
 end
 
 module String =

spectec/src/util/lib.mli

@@ -5,6 +5,7 @@ sig
   val split_hd : 'a list -> 'a * 'a list (* raises Failure *)
   val split_last : 'a list -> 'a list * 'a (* raises Failure *)
   val nub : ('a -> 'a -> bool) -> 'a list -> 'a list
+  val filter_not : ('a -> bool) -> 'a list -> 'a list
 end
 
 module String :

spectec/test-middlend/TEST.md

@@ -7842,7 +7842,6 @@ relation Module_ok: `|-%:OK`(module)
     -- if (|table*{table}| = |tt*{tt}|)
     -- if (|mem*{mem}| = |mt*{mt}|)
     -- if (|elem*{elem}| = |rt*{rt}|)
-    -- if (|data^n{data}| = n)
     -- if (C = {FUNC ft*{ft}, GLOBAL gt*{gt}, TABLE tt*{tt}, MEM mt*{mt}, ELEM rt*{rt}, DATA OK^n{}, LOCAL [], LABEL [], RETURN ?()})
     -- (Func_ok: `%|-%:%`(C, func, ft))*{ft func}
     -- (Global_ok: `%|-%:%`(C, global, gt))*{global gt}
@@ -8226,17 +8225,11 @@ relation Step_pure: `%*~>%*`(admininstr*, admininstr*)
   ;; 6-reduction.watsup:35.1-37.28
   rule block {bt : blocktype, instr* : instr*, k : nat, n : n, t_1^k : valtype^k, t_2^n : valtype^n, val^k : val^k}:
     `%*~>%*`($admininstr_val(val)^k{val} :: [BLOCK_admininstr(bt, instr*{instr})], [LABEL__admininstr(n, [], $admininstr_val(val)^k{val} :: $admininstr_instr(instr)*{instr})])
-    -- if (|t_1^k{t_1}| = k)
-    -- if (|t_2^n{t_2}| = n)
-    -- if (|val^k{val}| = k)
     -- if (bt = `%->%`(t_1^k{t_1}, t_2^n{t_2}))
 
   ;; 6-reduction.watsup:39.1-41.28
   rule loop {bt : blocktype, instr* : instr*, k : nat, n : n, t_1^k : valtype^k, t_2^n : valtype^n, val^k : val^k}:
     `%*~>%*`($admininstr_val(val)^k{val} :: [LOOP_admininstr(bt, instr*{instr})], [LABEL__admininstr(k, [LOOP_instr(bt, instr*{instr})], $admininstr_val(val)^k{val} :: $admininstr_instr(instr)*{instr})])
-    -- if (|t_1^k{t_1}| = k)
-    -- if (|t_2^n{t_2}| = n)
-    -- if (|val^k{val}| = k)
     -- if (bt = `%->%`(t_1^k{t_1}, t_2^n{t_2}))
 
   ;; 6-reduction.watsup:43.1-45.16
@@ -8256,7 +8249,6 @@ relation Step_pure: `%*~>%*`(admininstr*, admininstr*)
   ;; 6-reduction.watsup:57.1-58.69
   rule br-zero {instr* : instr*, instr'* : instr*, n : n, val^n : val^n, val'* : val*}:
     `%*~>%*`([LABEL__admininstr(n, instr'*{instr'}, $admininstr_val(val')*{val'} :: $admininstr_val(val)^n{val} :: [BR_admininstr(0)] :: $admininstr_instr(instr)*{instr})], $admininstr_val(val)^n{val} :: $admininstr_instr(instr')*{instr'})
-    -- if (|val^n{val}| = n)
 
   ;; 6-reduction.watsup:60.1-61.65
   rule br-succ {instr* : instr*, instr'* : instr*, l : labelidx, n : n, val* : val*}:
@@ -8285,12 +8277,10 @@ relation Step_pure: `%*~>%*`(admininstr*, admininstr*)
   ;; 6-reduction.watsup:100.1-101.35
   rule frame-vals {f : frame, n : n, val^n : val^n}:
     `%*~>%*`([FRAME__admininstr(n, f, $admininstr_val(val)^n{val})], $admininstr_val(val)^n{val})
-    -- if (|val^n{val}| = n)
 
   ;; 6-reduction.watsup:103.1-104.55
   rule return-frame {f : frame, instr* : instr*, n : n, val^n : val^n, val'* : val*}:
     `%*~>%*`([FRAME__admininstr(n, f, $admininstr_val(val')*{val'} :: $admininstr_val(val)^n{val} :: [RETURN_admininstr] :: $admininstr_instr(instr)*{instr})], $admininstr_val(val)^n{val})
-    -- if (|val^n{val}| = n)
 
   ;; 6-reduction.watsup:106.1-107.60
   rule return-label {instr* : instr*, instr'* : instr*, k : nat, val* : val*}:
@@ -8380,9 +8370,6 @@ relation Step_read: `%~>%*`(config, admininstr*)
     `%~>%*`(`%;%*`(z, $admininstr_val(val)^k{val} :: [CALL_ADDR_admininstr(a)]), [FRAME__admininstr(n, f, [LABEL__admininstr(n, [], $admininstr_instr(instr)*{instr})])])
     -- if (|t*{t}| = |o0*{o0}|)
     -- if (a < |$funcinst(z)|)
-    -- if (|t_1^k{t_1}| = k)
-    -- if (|t_2^n{t_2}| = n)
-    -- if (|val^k{val}| = k)
     -- (if ($default_(t) = ?(o0)))*{t o0}
     -- if ($funcinst(z)[a] = `%;%`(m, `FUNC%%*%`(`%->%`(t_1^k{t_1}, t_2^n{t_2}), t*{t}, instr*{instr})))
     -- if (f = {LOCAL val^k{val} :: o0*{o0}, MODULE m})