inline equalities

Author: redianthus

shell.nix

@@ -6,10 +6,10 @@
 let
   smtml = pkgs.ocamlPackages.smtml.overrideAttrs (old: {
     src = pkgs.fetchFromGitHub {
-      owner = "formalsec";
+      owner = "redianthus";
       repo = "smtml";
-      rev = "e259d5b7d108cb2d1102c188132a6c86bbf7705e";
-      hash = "sha256-8OzNJIyJhfqgDw3ioINN0D0WVTSliG9TP4cUNlrm4s8=";
+      rev = "84f727e98ceb793043a6e5984a2ce38dd64286a6";
+      hash = "sha256-0m4fDKYYKmC3UqHIc4ZQW1Fl06seDX5mAKLr4MTYsM4=";
     };
     doCheck = false;
   });

src/symbolic/symbolic_path_condition.ml

@@ -4,48 +4,124 @@
 
 module Union_find = Union_find.Make (Smtml.Symbol)
 
-type t = Smtml.Expr.Set.t Union_find.t
+type union_find = Smtml.Expr.Set.t Union_find.t
 
-let empty : t = Union_find.empty
+type equalities = Smtml.Expr.t Smtml.Symbol.Map.t
 
-let add_one (condition : Smtml.Expr.t) pc : t =
+type t =
+  { union_find : union_find
+      (** the union find contains many partitions of the whole path condition,
+          each partition is a set of expressions representing a conjunctions of
+          transitively related formula, that is, if we have a formula xRy and
+          yRz, then x, y and z end-up in the same partition. We can quickly
+          merge two partition and find the partition to which a symbol belongs.
+      *)
+  ; equalities : equalities
+      (** the equalities is a map of symbol to known constant values *)
+  }
+
+let empty : t =
+  let union_find = Union_find.empty in
+  let equalities = Smtml.Symbol.Map.empty in
+  { union_find; equalities }
+
+let add_one (condition : Smtml.Expr.t) (union_find : union_find) : union_find =
   match Smtml.Expr.get_symbols [ condition ] with
   | hd :: tl ->
-    (* We add the first symbol to the UF *)
-    let pc =
+    (* We add the first symbol to the union-find *)
+    let union_find =
       let c = Smtml.Expr.Set.singleton condition in
-      Union_find.add ~merge:Smtml.Expr.Set.union hd c pc
+      Union_find.add ~merge:Smtml.Expr.Set.union hd c union_find
     in
     (* We union-ize all symbols together, starting with the first one that has already been added *)
-    let pc, _last_sym =
+    let union_find, _last_sym =
       List.fold_left
         (fun (pc, last_sym) sym ->
           (Union_find.union ~merge:Smtml.Expr.Set.union last_sym sym pc, sym) )
-        (pc, hd) tl
+        (union_find, hd) tl
     in
-    pc
+    union_find
   | [] ->
     (* It means smtml did not properly simplified an expression! *)
     assert false
 
 let add (condition : Symbolic_boolean.t) (pc : t) : t =
-  (* we start by splitting the condition ((P & Q) & R) into a set {P; Q; R} before adding each of P, Q and R into the UF data structure, this way we maximize the independence of the PC *)
+  (* we start by splitting the condition ((P & Q) & R) into a set {P; Q; R} before adding each of P, Q and R into the union_find data structure, this way we maximize the independence of the PC *)
   let splitted_condition = Smtml.Typed.Bool.split_conjunctions condition in
-  Smtml.Expr.Set.fold add_one splitted_condition pc
+  let splitted_condition =
+    Smtml.Expr.Set.map Smtml.Expr.simplify splitted_condition
+  in
+  let equalities =
+    Smtml.Expr.Set.fold
+      (fun (condition : Smtml.Expr.t) equalities ->
+        match Smtml.Expr.view condition with
+        | Relop (_, Smtml.Ty.Relop.Eq, e1, e2) -> begin
+          match (Smtml.Expr.view e1, Smtml.Expr.view e2) with
+          | Smtml.Expr.Symbol s, _ ->
+            if Smtml.Expr.is_symbolic e2 then equalities
+            else Smtml.Symbol.Map.add s e2 equalities
+          | _, Symbol s ->
+            if Smtml.Expr.is_symbolic e1 then equalities
+            else Smtml.Symbol.Map.add s e1 equalities
+          | _ -> equalities
+        end
+        | _ -> equalities )
+      splitted_condition pc.equalities
+  in
+  let union_find =
+    Smtml.Expr.Set.fold add_one splitted_condition pc.union_find
+  in
+  { union_find; equalities }
+
+let equality_to_expr sym expr =
+  Smtml.Expr.Bool.equal (Smtml.Expr.symbol sym) expr
+
+let equalities_to_expr_list (equalities : equalities) : Smtml.Expr.t list =
+  Smtml.Symbol.Map.bindings equalities
+  |> List.map (fun (sym, expr) -> equality_to_expr sym expr)
+
+let equalities_to_set (equalities : equalities) : Smtml.Expr.Set.t =
+  Smtml.Symbol.Map.fold
+    (fun sym expr set ->
+      let e = equality_to_expr sym expr in
+      Smtml.Expr.Set.add e set )
+    equalities Smtml.Expr.Set.empty
+
+let filter_set (set : Smtml.Expr.Set.t) : Smtml.Expr.Set.t =
+  Smtml.Expr.Set.fold
+    (fun expr set ->
+      match Smtml.Expr.view expr with
+      | Val True -> set
+      | _ -> Smtml.Expr.Set.add expr set )
+    set Smtml.Expr.Set.empty
 
 (* Get all sub conditions of the path condition as a list of independent sets of constraints. *)
-let slice pc = Union_find.explode pc
+let slice (pc : t) =
+  let slice =
+    Union_find.explode pc.union_find
+    |> List.map (Smtml.Expr.Set.inline_symbol_values pc.equalities)
+    |> List.map filter_set
+  in
+  let equalities =
+    equalities_to_expr_list pc.equalities |> List.map Smtml.Expr.Set.singleton
+  in
+  slice @ equalities
 
 (* Return the set of constraints from [pc] that are relevant for [sym]. *)
-let slice_on_symbol (sym : Smtml.Symbol.t) pc : Smtml.Expr.Set.t =
-  match Union_find.find_opt sym pc with
-  | Some s -> s
+let slice_on_symbol (sym : Smtml.Symbol.t) (pc : t) : Smtml.Expr.Set.t =
+  match Union_find.find_opt sym pc.union_find with
+  | Some s ->
+    let set =
+      Smtml.Expr.Set.inline_symbol_values pc.equalities s |> filter_set
+    in
+    let equalities = equalities_to_set pc.equalities in
+    Smtml.Expr.Set.union set equalities
   | None ->
     (* if there is a symbol, it should have been added to the union-find structure before, otherwise it means `add` has not been called properly before *)
     assert false
 
 (* Return the set of constraints from [pc] that are relevant for [c]. *)
-let slice_on_condition (c : Symbolic_boolean.t) pc : Smtml.Expr.Set.t =
+let slice_on_condition (c : Symbolic_boolean.t) (pc : t) : Smtml.Expr.Set.t =
   match Smtml.Typed.get_symbols [ c ] with
   | sym0 :: _tl ->
     (* we need only the first symbol as all the others should have been merged with it *)