From 79c039d7b33878d00f22ad8542dc30a78aa8b70a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 11:34:35 +0100 Subject: CSE3 + conditions proof --- backend/CSE3analysis.v | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 46ae4aea..383147bb 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -461,10 +461,33 @@ Section OPERATIONS. | _ => rel end. + Definition apply_cond1 cond args (rel : RELATION.t) : RB.t := + match eq_find (Cond (negate_condition cond) args) with + | Some eq_id => + if PSet.contains rel eq_id + then RB.bot + else Some rel + | None => Some rel + end. + + Definition apply_cond0 cond args (rel : RELATION.t) : RELATION.t := + match eq_find (Cond cond args) with + | Some eq_id => PSet.add eq_id rel + | None => rel + end. + + Definition apply_cond cond args (rel : RELATION.t) : RB.t := + match apply_cond1 cond args rel with + | Some rel => Some (apply_cond0 cond args rel) + | None => RB.bot + end. + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with | Inop pc' => (pc', (Some rel))::nil - | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil + | Icond cond args ifso ifnot _ => + (ifso, (apply_cond cond args rel)):: + (ifnot, (apply_cond (negate_condition cond) args rel))::nil | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets | Istore chunk addr args src pc' => (pc', (Some (store tenv chunk addr args src rel)))::nil -- cgit