fix in CSE3 move propagation

3 files changed, 62 insertions, 22 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index b495371d..91064a5d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -274,11 +274,20 @@ Section OPERATIONS.
 
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
-    match rhs_find op (forward_move_l rel args) rel with
-    | Some r => RELATION.glb (move r dst rel)
-                             (oper1 dst op args rel)
-    | None => oper1 dst op args rel
-    end.
+    if is_smove op
+    then
+      match args with
+      | src::nil =>
+        move (forward_move rel src) dst rel
+      | _ => kill_reg dst rel
+      end
+    else
+      let args' := forward_move_l rel args in
+      match rhs_find op args' rel with
+      | Some r => (* FIXME RELATION.glb ( *) move r dst rel (* )
+                                                               (oper1 dst op args' rel) *)
+      | None => oper1 dst op args' rel
+      end.
   
   Definition clever_kill_store
              (chunk : memory_chunk) (addr: addressing) (args : list reg)
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index 0260f3b1..e8e608da 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -32,10 +32,10 @@ let print_eq channel (lhs, sop, args) =
      Printf.printf "%a = %s @ %a\n" print_reg lhs (string_of_chunk chunk)
        (PrintOp.print_addressing print_reg) (addr, args);;
 
-let print_set s =
-  Printf.printf "{ ";
-  List.iter (fun i -> Printf.printf "%d; " (P.to_int i)) (PSet.elements s);
-  Printf.printf "}\n";;
+let pp_set oc s =
+  Printf.fprintf oc "{ ";
+  List.iter (fun i -> Printf.fprintf oc "%d; " (P.to_int i)) (PSet.elements s);
+  Printf.fprintf oc "}";;
 
 let pp_rhs oc (sop, args) =
   match sop with
@@ -45,6 +45,16 @@ let pp_rhs oc (sop, args) =
        (PrintAST.name_of_chunk chunk)
          (PrintOp.print_addressing PrintRTL.reg) (addr, args);;
 
+let pp_eq oc eq =
+  Printf.fprintf oc "x%d = %a" (P.to_int eq.eq_lhs)
+    pp_rhs (eq.eq_op, eq.eq_args);;
+
+let pp_P oc x = Printf.fprintf oc "%d" (P.to_int x)
+              
+let pp_option pp oc = function
+  | None -> output_string oc "none"
+  | Some x -> pp oc x;;
+
 let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   let cur_eq_id = ref 0
   and cur_catalog = ref PTree.empty
@@ -54,14 +64,21 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
   and cur_kill_mem = ref PSet.empty
   and cur_moves = ref (PMap.init PSet.empty) in
   let eq_find_oracle node eq =
-    Hashtbl.find_opt eq_table (flatten_eq eq)
+    let o = Hashtbl.find_opt eq_table (flatten_eq eq) in
+    Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node)
+      pp_eq eq (pp_option pp_P) o;
+    o
   and rhs_find_oracle node sop args =
-    (* Printf.printf "query for %a\n" pp_rhs (sop, args); *)
-    match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
-    | None -> PSet.empty
-    | Some s -> s in
+    let o =
+      match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
+      | None -> PSet.empty
+      | Some s -> s in
+    Printf.printf "@%d: rhs_find %a = %a\n" (P.to_int node) pp_rhs (sop, args)
+      pp_set o;
+    o in
   let mutating_eq_find_oracle node eq : P.t option =
     let (flat_eq_lhs, flat_eq_op, flat_eq_args) as flat_eq = flatten_eq eq in
+    let o =
     match Hashtbl.find_opt eq_table flat_eq with
     | Some x ->
        Some x
@@ -88,6 +105,10 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) =
           | _, _ -> ());
          Some coq_id
        end
+    in
+    Printf.printf "@%d: mutating_eq_find %a -> %a\n" (P.to_int node)
+      pp_eq eq (pp_option pp_P) o;    
+    o
   in
   match
     internal_analysis
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 3ea5e078..116353fa 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -778,15 +778,25 @@ Section SOUNDNESS.
     intros until v.
     intros REL RHS.
     unfold oper.
-    destruct rhs_find as [src |] eqn:RHS_FIND.
-    - apply sem_rel_glb; split.
-      + pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
-        eapply forward_move_rhs_sound in RHS.
-        2: eassumption.
-        rewrite <- (sem_rhs_det SOUND RHS).
-        apply move_sound; auto.
+    destruct (is_smove sop).
+    - subst.
+      simpl in RHS.
+      destruct args. contradiction.
+      destruct args. 2: contradiction.
+      cbn in *.
+      subst.
+      rewrite <- (forward_move_sound rel rs m r) by auto.
+      apply move_sound; auto.
+    - destruct rhs_find as [src |] eqn:RHS_FIND.
+      + (* FIXME apply sem_rel_glb; split. *)
+        * pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
+          eapply forward_move_rhs_sound in RHS.
+          2: eassumption.
+          rewrite <- (sem_rhs_det SOUND RHS).
+          apply move_sound; auto.
+        (* FIXME * apply oper1_sound; auto. *)
       + apply oper1_sound; auto.
-    - apply oper1_sound; auto.
+        apply forward_move_rhs_sound; auto.
   Qed.
 
   Hint Resolve oper_sound : cse3.