[WIP] Support dereference of pointer to array in assert statement

src/.gitignore

@@ -1,3 +1,4 @@
 *.smt
 /recursive-tests/
 /benchmarks/consort/**/*.class
+/tmp/

src/consort.ml

@@ -1,3 +1,5 @@
+open Sexplib.Std
+
 type reason =
   | Timeout
   | Unsafe
@@ -193,6 +195,7 @@ let consort ~opts file =
   let simple_res = SimpleChecker.typecheck_prog simple_typing ast in
   let infer_res = OwnershipInference.infer ~opts simple_res ast in
   let ownership_res = OwnershipSolver.solve_ownership ~opts infer_res in
+  Log.debug ~src:"OWNERSHIP" !"Mapping from ownership variable to value: %{sexp:(int * float) list option}" ownership_res;
   match ownership_res with
   | None -> Unverified Aliasing
   | Some o_res ->

src/dune

@@ -50,6 +50,7 @@
  (name test)
  (preprocess (pps ppx_sexp_conv ppx_let with_monad ppx_custom_printf ppx_cast))
  (libraries consort yaml)
+ (flags (-linkall))
  (modules Test))
 
 (executable

src/flowInference.ml

@@ -322,12 +322,17 @@ let add_assert_cond assert_cond curr_relation =
    null flag of [v] happens to be represented as an extension (and thus "beneath") [v]; this requires an annoying special
    case when doing havoc queries, but *believe me*, it's far more annoying to use another strategy.
  *)
+
+let show_map m = OI.GenMap.fold (fun k d rest -> Printf.sprintf !"%{sexp:OI.magic_loc * P.path}" k ^ " -> " ^ string_of_float d ^ ", " ^ rest) m ""
+
 let rec havoc_oracle ctxt ml p =
   Log.debug ~src:"FLOW-OWN" !"Looking for %{P} @ %{sexp:OI.magic_loc}" p ml;
   let from_path p_ =
+    Log.debug ~src:"FLOW-OWN" !"Searching %{sexp:OI.magic_loc * P.path} in %s" (ml,p_) (show_map ctxt.o_hints.OI.gen);
     let o = OI.GenMap.find (ml,p_) ctxt.o_hints.OI.gen in
     o = 0.0
   in
+  Log.debug ~src:"FLOW-OWN" !"P.tail p is %s" (P.string_of_tail (P.tail p));
   match P.tail p with
   | Some `Deref
   | Some `Ind
@@ -2284,6 +2289,7 @@ let%lq get_iso_at e_id ctxt =
    labelled return statements) is described by the output argument.
 *)
 let rec process_expr ~output (((relation : relation),tyenv) as st) continuation ((e_id,_),e) =
+  Log.debug ~src:"DEBUG" !"processing %d: %{sexp:raw_exp}" e_id e;
   (* execute two branches, and then bring their results into sync. analyzes branch 1, b2 analyzes branch 2 *)
   let scoped_effect ~b1 ~b2 ctxt =
     (* some trickery here; we abuse the context to record information about the current
@@ -2911,6 +2917,7 @@ let analyze_main start_rel main ctxt =
   let ctxt,_ = process_expr (start_rel,[]) ~output:None None main ctxt in
   ctxt
 
+(* Take options "~opts", a result of simple type checking "(simple_theta,side_results)", ownership information "o_hints", and AST "(fns, main)" as arguments. *)
 let infer ~opts (simple_theta,side_results) o_hints (fns,main) =
   let lift_and_unfold = (fun p -> deep_type_normalization @@ simple_to_fltype p) in
   let simple_theta = StringMap.map (fun ft ->

src/ownershipInference.ml

@@ -18,6 +18,7 @@ module P = Paths
 type ownership =
     OVar of int (** A variable with id int *)
   | OConst of float (** a constant ownership with the given rational number *)
+[@@deriving sexp]
 
 type ocon =
   | Live of ownership (** The ownership must be greater than 0 (only emitted in relaxed mode) *)
@@ -35,8 +36,9 @@ type 'a otype_ =
   | Tuple of 'a otype_ list
   | TVar of int
   | Mu of int * 'a otype_
+[@@deriving sexp]
 
-type otype = ownership otype_
+type otype = ownership otype_ [@@deriving sexp]
 
 (** For the most part, the ownership and refinement inference passes may be run independently. The only intersection is
 handling 0 ownership references; when a reference drops to 0 ownership, all refinements must go to top (although we use
@@ -110,6 +112,13 @@ type 'a ownership_ops = {
    the function parameters, and b) the ownership returned back to the function.
  *) 
 
+type gamma = otype StringMap.t
+let sexp_of_gamma = StringMap.sexp_of_t ~v:sexp_of_otype
+
+(** Save the ownership types at each point in the program; only used for debugging *)
+type save_env = otype StringMap.t IntMap.t
+let sexp_of_save_env = IntMap.sexp_of_t ~v:(StringMap.sexp_of_t ~v:sexp_of_otype)
+
 type context = {
   relaxed : bool;
   ovars: int list;
@@ -121,12 +130,10 @@ type context = {
   v_counter: int;
   iso: SimpleChecker.SideAnalysis.results;
   ocons: ocon list;
-  gamma: otype StringMap.t;
+  gamma: gamma;
   theta: (otype RefinementTypes._funtype) StringMap.t;
   op_record: ownership ownership_ops;
-  save_env: otype StringMap.t IntMap.t (** Save the ownership types at
-                                          each point in the program;
-                                          only used for debugging *)
+  save_env: save_env
 }
 
 type infr_options = bool
@@ -838,6 +845,8 @@ let infer ~opts (simple_types,iso) (fn,prog) =
   in
   let ctxt = List.fold_left analyze_fn ctxt fn in
   let (ctxt,_) = process_expr ~output:None prog ctxt in
+  Log.debug ~src:"OWNERSHIP" !"Gamma: %{sexp:gamma}" ctxt.gamma;
+  Log.debug ~src:"OWNERSHIP" !"Owenrship types at each point: %{sexp:save_env}" ctxt.save_env;
   {
     Result.ocons = ctxt.ocons;
     Result.ovars = ctxt.ovars;

src/paths.ml

@@ -143,11 +143,11 @@ let unsafe_get_root (v,_,_) = match v with
   | Var n -> n
   | _ -> failwith "Not rooted in var"
 
-let parent (p,suff,fl) =
-  match suff,fl with
+let parent (p,fl,suff) =
+  match fl,suff with
   | [],`None -> raise @@ Invalid_argument "at root"
   | _::t,`None -> (p,t,`None)
-  | _,_ -> (p,suff,`None)
+  | _,_ -> (p,fl,`None)
 
 let root_at ~child:(r,steps,suff) ~parent:(root,steps2,suff2) =
   let () =
@@ -171,6 +171,17 @@ let tail (_,l,f) =
   | [],`None -> None
   | _,(#inh_tags as cr) -> Some cr
 
+let string_of_tail = function
+  | Some e -> 
+    (match e with
+      | `Null -> "Null"
+      | `Deref -> "Deref"
+      | `Proj i -> Printf.sprintf "Proj %d" i
+      | `Len -> "Len"
+      | `Elem -> "Elem"
+      | `Ind -> "Ind")
+  | None -> "None"
+
 module PathOrd = struct
   type t = path
   let compare = compare

src/paths.mli

@@ -28,6 +28,7 @@ type steps = [
 private (to protect crucial invariants), but may still be pattern matched over. To make extension O(1), the steps are stored in _reverse_ order
 in the path representation; i.e., the last step is the head of the list, etc. *)
 type path = private root * steps list * suff [@@deriving sexp]
+(* type path = root * steps list * suff [@@deriving sexp] *)
 type concr_ap = path [@@deriving sexp]
 
 (** Give a string representation of the path, suitable for use as a z3 identifier *)
@@ -143,6 +144,8 @@ val compare : path -> path -> int
 *)
 val tail : path -> [`Null | `Deref | `Proj of int | `Len | `Elem | `Ind ] option
 
+val string_of_tail: [`Null | `Deref | `Proj of int | `Len | `Elem | `Ind ] option -> string
+
 (** A (printable) set of paths *)
 module PathSet : Std.PRINTSET with type elt = path
 

src/regnant/.gitignore

@@ -6,3 +6,4 @@ build/
 sootOutput/
 tmp/
 minepump
+bin/

src/std.ml

@@ -18,7 +18,15 @@ module PrintSet(P: sig
   let to_string e = elements e |> List.map P.to_string |> String.concat ", " |> Printf.sprintf "{%s}"
 end
 
-module IntMap = Map.Make(Int)
+module IntMap = struct
+  open Sexplib.Std
+  include Map.Make(Int)
+  let sexp_of_t (type v_type) ~(v: v_type -> Sexplib.Sexp.t) t =
+    let sexp_of_v_type = v in
+    bindings t
+    |> [%sexp_of: (int * v_type) list]
+end
+
 module IntSet = PrintSet(Int)
 module StringSet = PrintSet(struct include String let to_string = Fun.id end)