[Draft] Prototype of auto-annot

bin/common.ml

@@ -282,13 +282,15 @@ type subcommand =
   | Instrument
   | Test
   | SeqTest
+  | AutoAnnot
 
 let tool_name cmd =
   match cmd with
   | Verify -> "CN"
   | Instrument -> "Fulminate"
   | Test -> "Bennet"
   | SeqTest -> "CN-Seq-Test"
+  | AutoAnnot -> "AutoAnnot"
 
 
 open Cmdliner

bin/instrument.ml

@@ -98,6 +98,7 @@ let generate_executable_specs
       experimental_ownership_stack_mode
       mktemp
       print_steps
+      with_auto_annot
   =
   (* flags *)
   Cerb_debug.debug_level := debug_level;
@@ -110,6 +111,7 @@ let generate_executable_specs
   Check.fail_fast := fail_fast;
   Diagnostics.diag_string := diag;
   Sym.executable_spec_enabled := true;
+  Fulminate.Config.with_auto_annot := with_auto_annot;
   let handle_error (e : TypeErrors.t) =
     let report = TypeErrors.pp_message e.msg in
     Pp.error e.loc report.short (Option.to_list report.descr);
@@ -271,6 +273,11 @@ module Flags = struct
        locations where ownership was taken for Fulminate-tracked memory"
     in
     Arg.(value & flag & info [ "ownership-stack-mode" ] ~doc)
+
+
+  let with_auto_annot =
+    let doc = "Instrument additional information for auto-annot (for debugging)" in
+    Arg.(value & flag & info [ "with-auto-annot" ] ~doc)
 end
 
 let cmd =
@@ -310,6 +317,7 @@ let cmd =
     $ Flags.experimental_ownership_stack_mode
     $ Flags.mktemp
     $ Flags.print_steps
+    $ Flags.with_auto_annot
   in
   let doc =
     "Instruments [FILE] with runtime C assertions that check the properties provided in \

bin/main.ml

@@ -1,6 +1,6 @@
 open Cmdliner
 
-let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd ]
+let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; Annot.cmd ]
 
 let () =
   let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]" in

bin/test.ml

@@ -145,7 +145,8 @@ let run_tests
           print_size_info;
           print_backtrack_info;
           print_satisfaction_info;
-          print_discard_info
+          print_discard_info;
+          with_auto_annot = false
         }
       in
       TestGeneration.set_config config;

cn.opam

@@ -24,6 +24,7 @@ depends: [
   "ounit2" {with-test}
   "qcheck" {with-test}
   "qcheck-ounit" {with-test}
+  "z3"
 ]
 pin-depends: [
   ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#9eb2ce2"]

lib/autoAnnot/autoAnnot.ml

@@ -0,0 +1,213 @@
+module CF = Cerb_frontend
+module A = CF.AilSyntax
+
+let log_filename = ref "cn_auto_annot.log"
+
+let get_log_filename filename =
+  Filename.(remove_extension (basename filename)) ^ ".autoannot.log"
+
+
+type assignment =
+  { accessor : string;
+    value : int
+  }
+
+type focus =
+  { filename : string;
+    line : int;
+    kind : string;
+    ty : string;
+    (* TODO: should be int64 *)
+    target : int;
+    assignments : assignment list
+  }
+
+type annot = Focus of focus
+
+let print_focus_suggestion filename line kind ty w0 coeffs =
+  let pos = filename ^ ":" ^ string_of_int line in
+  let body =
+    List.filter_map
+      (fun (v, c) ->
+         match c with 0 -> None | 1 -> Some v | c -> Some (string_of_int c ^ " * " ^ v))
+      coeffs
+  in
+  let signature = Printf.sprintf "focus %s<%s>, " kind ty in
+  let elems = if w0 = 0 then body else string_of_int w0 :: body in
+  let sum = String.concat " + " elems in
+  let annotation = signature ^ sum in
+  Pp.progress_simple pos annotation
+
+
+let generate_focus_annot_aux filename line (kind, ty, assignments_list) : unit =
+  Pp.(
+    debug
+      10
+      (lazy
+        (item
+           "Generating annotations"
+           (string filename ^^ string ":" ^^ (line |> string_of_int |> string)))));
+  let _, first = List.hd assignments_list in
+  let variables =
+    first |> List.map (fun a -> a.accessor) |> List.sort_uniq String.compare
+  in
+  (* Sanity: all occurrences have the same variable set *)
+  let all_unique =
+    List.for_all
+      (fun x ->
+         List.fold_left
+           (fun acc y -> if String.equal x y then acc + 1 else acc)
+           0
+           variables
+         = 1)
+      variables
+  in
+  if not all_unique then
+    failwith "AutoAnnot: inconsistent environment";
+  (* Create a template *)
+  (* like ax + by + c = 0, and try to find a, b, and c *)
+  (* For [[x = 1; y = 2]; [ x = 2; y = 4]] *)
+  (* generate a * 1 + b * 2 + c = 0 /\ a * 2 + b * 4 + c = 0 *)
+  (* and find a, b, and c that satisfy the above using Z3 Optimize *)
+  let open Z3 in
+  let ctx = Z3.mk_context [ ("model", "true") ] in
+  let opt = Optimize.mk_opt ctx in
+  let i_k n = Arithmetic.Integer.mk_numeral_i ctx n in
+  let mk_int name = Arithmetic.Integer.mk_const_s ctx name in
+  let add = Arithmetic.mk_add ctx in
+  let mul x y = Arithmetic.mk_mul ctx [ x; y ] in
+  let neg x = Arithmetic.mk_unary_minus ctx x in
+  let ge = Arithmetic.mk_ge ctx in
+  let eq = Boolean.mk_eq ctx in
+  (* constant *)
+  let w0 = mk_int "w0" in
+  (* coefficients *)
+  let coeffs = List.map (fun v -> (v, mk_int ("w_" ^ v))) variables in
+  (* For each sample env, assert: w0 + sum(w_v * val_v) = 0 *)
+  let value_of v (env : assignment list) =
+    (List.find (fun a -> String.equal a.accessor v) env).value
+  in
+  let sum_terms env =
+    let terms = List.map (fun (v, wv) -> mul wv (i_k (value_of v env))) coeffs in
+    add (w0 :: terms)
+  in
+  List.iter
+    (fun (target, env) -> Optimize.add opt [ eq (sum_terms env) (i_k target) ])
+    assignments_list;
+  (* L1 norm: minimize t_v where t_v >= w_v and t_v >= -w_v*)
+  let ts =
+    List.map
+      (fun (v, wv) ->
+         let tv = mk_int ("t_" ^ v) in
+         Optimize.add opt [ ge tv wv; ge tv (neg wv) ];
+         tv)
+      coeffs
+  in
+  let objective = add ts in
+  ignore (Optimize.minimize opt objective : Optimize.handle);
+  (* Solve and read model *)
+  match Optimize.check opt with
+  | Solver.SATISFIABLE ->
+    let m = Optimize.get_model opt in
+    let get_int e =
+      let m = match m with Some m -> m | None -> failwith "No model found" in
+      match Model.eval m e true with
+      | None -> 0
+      | Some v -> int_of_string (Expr.to_string v)
+    in
+    let w0_v = get_int w0 in
+    let coeff_vals = List.map (fun (v, wv) -> (v, get_int wv)) coeffs in
+    print_focus_suggestion filename line kind ty w0_v coeff_vals
+  | Solver.UNSATISFIABLE | Solver.UNKNOWN ->
+    Pp.(
+      debug
+        5
+        (lazy
+          (item
+             "AutoAnnot: no relation found"
+             (string (filename ^ ":" ^ string_of_int line)))))
+
+
+let generate_focus_annot (annots : focus list) : unit =
+  let tbl : (string * int, string * string * (int * assignment list) list) Hashtbl.t =
+    Hashtbl.create 16
+  in
+  let add filename line assigns kind ty =
+    let key = (filename, line) in
+    let prev =
+      match Hashtbl.find_opt tbl key with
+      | Some (kind2, ty2, xs) when String.equal kind kind2 && String.equal ty ty2 -> xs
+      | Some _ -> failwith "inconsistent focus types"
+      | None -> []
+    in
+    Hashtbl.replace tbl key (kind, ty, prev @ [ assigns ])
+  in
+  List.iter
+    (function
+      | { filename; line; assignments; target; kind; ty } ->
+        add filename line (target, assignments) kind ty)
+    annots;
+  Hashtbl.iter
+    (fun (filename, line) assigns -> generate_focus_annot_aux filename line assigns)
+    tbl
+
+
+let parse (log_file : string) : annot list =
+  (* Open the file *)
+  let ic = open_in log_file in
+  let prefix = "[auto annot (focus)]" in
+  let split_and_trim ch s = String.split_on_char ch s |> List.map String.trim in
+  let parse_line (line : string) : annot =
+    if not (String.starts_with ~prefix line) then
+      failwith "ill-formed auto annot line";
+    let rest =
+      String.sub line (String.length prefix) (String.length line - String.length prefix)
+      |> String.trim
+    in
+    match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with
+    | [] -> failwith "ill-formed focus annotation"
+    | loc :: assigns_parts ->
+      (match split_and_trim ':' loc with
+       (* ex: itres.c:46:12-16:RW:signed int *)
+       | [ filename; line_str; _; kind; ty ] ->
+         (match int_of_string_opt line_str with
+          | None -> failwith "ill-formed line number"
+          | Some line ->
+            let assignments =
+              assigns_parts
+              |> List.map (fun p ->
+                match String.split_on_char '=' p |> List.map String.trim with
+                | [ key; vstr ] ->
+                  let v = int_of_string vstr in
+                  { accessor = key; value = v }
+                | _ -> failwith "ill-formed")
+            in
+            (* assignments must be non-empty; as the first element is the target*)
+            let fst = List.hd assignments in
+            assert (String.equal fst.accessor "!index");
+            let assignments = List.tl assignments in
+            Focus { filename; line; kind; ty; assignments; target = fst.value })
+       | _ -> failwith "ill-formed line")
+  in
+  let rec loop res =
+    match input_line ic with
+    | line ->
+      let res = parse_line line :: res in
+      loop res
+    | exception End_of_file -> res
+  in
+  let res =
+    try loop [] with
+    | e ->
+      close_in_noerr ic;
+      raise e
+  in
+  close_in ic;
+  res
+
+
+let run_autoannot (log_file : string) : unit =
+  Pp.print stdout (Pp.string "[Result of auto-annotation]");
+  let data = parse log_file in
+  let focus_annots = data |> List.filter_map (function Focus f -> Some f) in
+  generate_focus_annot focus_annots

lib/autoAnnot/autoAnnot.mli

@@ -0,0 +1,8 @@
+module CF = Cerb_frontend
+module A = CF.AilSyntax
+
+val log_filename : string ref
+
+val get_log_filename : string -> string
+
+val run_autoannot : string -> unit

lib/dune

@@ -14,6 +14,7 @@
   ppx_deriving_yojson.runtime
   result
   str
+  z3
   unix
   yojson)
  (preprocess