Get location information from goal

server/bin/creusot_lsp.ml

@@ -170,7 +170,7 @@ class lsp_server =
           match Why3findUtil.ProofPath.qualified_goal_of_json req with
           | None -> Lwt.return (`String "Error: invalid proof path")
           | Some path ->
-            let goal = Why3findUtil.get_goal path in
+            let goal = Why3findUtil.get_goal (Why3findUtil.get_env ()) path in
             let msg = match goal with
             | None -> "No goal found"
             | Some goal -> goal in

server/lib/dune

@@ -18,7 +18,7 @@
   ppx_yojson_conv
   ppx_yojson_conv_lib
   xmlm)
- (inline_tests)
+ (inline_tests (deps (source_tree ../testdata)))
  (preprocess
   (pps ppx_deriving.show ppx_expect ppx_yojson_conv))
  (modules_without_implementation types))

server/lib/tests.ml

@@ -4,15 +4,15 @@ let%expect_test _ =
   let coma = parse_coma_string "module M_qyi1 (* T *)\nmodule M_z__y\n" in
   List.iter (fun { name; demangled; _ } -> Format.printf "Module %s: %a\n" name.ident fprint_def_path demangled) coma.State.modules;
   [%expect {|
-    Module M_qyi1: impl{T}
-    Module M_z__y: z::y
+    Module M_qyi1: impl{T}::M
+    Module M_z__y: z::y::M
     |} ]
 
 let%expect_test _ =
   let open Creusot_demangler in
   Option.iter print_segments (demangle_ident "M_qyi3__qy65z");
   [%expect {|
-    ::impl{3}::A
+    ::impl{3}::A::M
   |}]
 
 let%expect_test _ =
@@ -23,7 +23,7 @@ let%expect_test _ =
   }" in
   let names = list_names lexbuf in
   List.iter (fun (def, _, _) -> Rust_syntax.print_def_path def) names;
-  [%expect {| impl{Node<K>}::f |}]
+  [%expect {| impl{Node<K>}::f::M |}]
 
 let%expect_test _ =
   let open Why3findUtil in
@@ -54,3 +54,49 @@ let%expect_test _ =
       vc2.split_vc.0.split_vc.1
       vc2.split_vc.1
     |}]
+
+let pp_range h loc =
+  let (file, bl, bc, el, ec) = Why3.Loc.get loc in
+  Format.fprintf h "%s#%d:%d-%d:%d" file bl bc el ec
+
+let%test_unit _ =
+  let open Why3findUtil in
+  let open ProofPath in
+  let env = get_test_env () in
+  let goal i = {
+    file = "../testdata/sum.coma";
+    theory = "M_sum__sum_first_n";
+    goal_info = {
+      vc = "vc_sum_first_n'0";
+      tactics = [("split_vc", i)];
+    }
+  } in
+  let p = Why3.Loc.user_position in
+  let expected = [|
+    Some (p "../testdata/sum.coma" 61 118 61 129); (* TODO: locate type invariants *)
+    Some (p "../testdata/sum.coma" 62 38 62 48);
+    Some (p "../testdata/sum.coma" 77 126 77 136);
+    Some (p "../../../creusot-contracts/src/std/iter.rs" 101 0 213 1);
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 8 16 8 65);
+    Some (p "../testdata/sum.coma" 154 119 154 129);
+    Some (p "sum.rs" 5 10 5 38);
+    Some (p "../testdata/prelude/prelude.coma" 49 59 49 76); (* TODO: locate overflows *)
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 9 4 9 7);
+    Some (p "sum.rs" 8 16 8 65);
+    None;
+  |] in
+  for i = 0 to 15 do
+    let loc = get_goal_loc env (goal i) in
+    match expected.(i), loc with
+    | None, None -> ()
+    | None, Some actual -> failwith (Format.asprintf "Expected: None\n Actual: Some(%a)" pp_range actual)
+    | Some expected, None -> failwith (Format.asprintf "Expected: Some(%a)\nActual: None" pp_range expected)
+    | Some expected, Some actual ->
+      if not (expected = actual) then
+        failwith (Format.asprintf "Expected: %a\nActual: %a" pp_range expected pp_range actual)
+  done

server/lib/why3findUtil.ml

@@ -243,18 +243,20 @@ let load_plugins =
       Why3.Whyconf.load_plugins @@ Why3.Whyconf.get_main env.Config.wenv.config
     )
 
-let load_config =
+let load_config ?(root = ".") ?(warn = true) =
   let lazy_config = lazy (
-  let config = Config.load_config "." in
-  (match config.packages with
-  | [] -> log Warning "No package found in config \"why3find.json\", at least prelude is needed for creusot proofs"
-  | _ -> ());
-  let check_warning w =
-    if not (List.mem w config.warnoff) then
-      log Warning "Disable warning \"%s\" in why3config.json, otherwise Why3 may produce lots of warnings on Creusot-generated code" w
-  in
-  check_warning "unused_variable";
-  check_warning "axiom_abstract";
+  let config = Config.load_config root in
+  if warn then (
+    (match config.packages with
+    | [] -> log Warning "No package found in config \"why3find.json\", at least prelude is needed for creusot proofs"
+    | _ -> ());
+    let check_warning w =
+      if not (List.mem w config.warnoff) then
+        log Warning "Disable warning \"%s\" in why3config.json, otherwise Why3 may produce lots of warnings on Creusot-generated code" w
+    in
+    check_warning "unused_variable";
+    check_warning "axiom_abstract";
+  );
   List.iter (fun unwarn ->
     Why3.Loc.disable_warning @@ Why3.Loc.register_warning unwarn Why3.Pp.empty_formatted)
     ("unused_variable" :: "axiom_abstract" :: config.warnoff);
@@ -267,6 +269,14 @@ let get_env () =
   load_plugins env;
   env
 
+(* Hack for the test suite. get_env must not have been called. *)
+let get_test_env () =
+  let root = "../testdata" in
+  let config = load_config ~root ~warn:false () in
+  let env = Config.create_env ~root ~config () in
+  load_plugins env;
+  env
+
 let rec path_goal_ theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.tactic_path) breadcrumbs : Session.goal option =
   let (let+) = Option.bind in
   match q with
@@ -284,24 +294,36 @@ let rec path_goal_ theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.t
 let path_goal ~theory (e : Why3.Env.env) (g : Session.goal) (q : ProofPath.tactic_path) : Session.goal option =
   path_goal_ theory e g q []
 
-let get_goal (q : qualified_goal) : string option =
+let warn_if_none msg x = (match x with
+  | None -> log Warning "%s" msg
+  | Some _ -> ()); x
+
+let for_goal (env : _) (q : qualified_goal) (f : Session.goal -> 'a option) : 'a option =
   try
     let session = true in
-    let env = get_env () in
     let file = q.file in
-    let dir, _lib = Wutil.filepath file in
     let (let+) = Option.bind in
     let theories, format = Wutil.load_theories env.Config.wenv.env file in
+    let dir, _lib = Wutil.filepath file in
     let s = Why3find.Session.create ~session ~dir ~file ~format theories in
-    let+ theory = List.find_opt (fun t -> Session.name t = q.theory) (Session.theories s) in
-    let+ goal = List.find_opt (fun g -> Session.goal_name g = q.goal_info.vc) (Session.split theory) in
+    let+ theory = List.find_opt (fun t -> Session.name t = q.theory) (Session.theories s) |> warn_if_none (Printf.sprintf "theory %s not found" q.theory) in
+    let+ goal = List.find_opt (fun g -> Session.goal_name g = q.goal_info.vc) (Session.split theory) |> warn_if_none (Printf.sprintf "vc %s not found" q.goal_info.vc) in
     let+ goal = path_goal ~theory:(Session.name theory) env.wenv.env goal q.goal_info.tactics in
-    let task = Session.goal_task goal in
-    Some (Format.asprintf "%a" Why3.Pretty.print_sequent task)
+    f goal
   with e -> log Error "get_goal: Failed to load why3: %s" (Printexc.to_string e); None
 
+let get_goal env q = for_goal env q (fun goal ->
+  let task = Session.goal_task goal in
+  Some (Format.asprintf "%a" Why3.Pretty.print_sequent task))
+
 let loc_to_range loc =
   let _, l1, c1, l2, c2 = Why3.Loc.get loc in
-  Lsp.Types.Range.create (* why is this necessary?       ----------v *)
+  Lsp.Types.Range.create
     ~start:(Lsp.Types.Position.create ~line:(l1 - 1) ~character:c1)
     ~end_:(Lsp.Types.Position.create ~line:(l2 - 1) ~character:c2)
+
+let goal_term_loc (g : Session.goal) =
+  let open Why3 in
+  (Task.task_goal_fmla (Session.goal_task g)).Term.t_loc
+
+let get_goal_loc env q = for_goal env q goal_term_loc

server/lib/why3findUtil.mli

@@ -1,5 +1,4 @@
 open Lsp.Types
-open Types
 open Util
 
 module ProofPath : sig
@@ -39,6 +38,9 @@ open ProofPath
 val parse_json : coma:string -> (theory -> unit) -> Jsonm.decoder -> unit
 val read_proof_json : coma:string -> source -> theory list
 
-val get_goal : ProofPath.qualified_goal -> string option
+val get_env : unit -> Why3find.Config.env
+val get_test_env : unit -> Why3find.Config.env
+val get_goal : Why3find.Config.env -> ProofPath.qualified_goal -> string option
+val get_goal_loc : Why3find.Config.env -> ProofPath.qualified_goal -> Why3.Loc.position option
 
 val loc_to_range : Why3.Loc.position -> Range.t

server/testdata/prelude/prelude.coma

@@ -0,0 +1,85 @@
+module Borrow
+  type borrowed 'a = { current : 'a; final : 'a; id : int }
+
+  function ( *_ ) (x : borrowed 'a) : 'a = x.current
+  function ( ^_ ) (x : borrowed 'a) : 'a = x.final
+
+  let borrow_final < 'a > (a : 'a) (id : int) (ret (result : borrowed 'a)) =
+    any [ ret' (fin : 'a) -> (! ret { { current = a; final = fin; id = id } })]
+
+  let borrow_mut < 'a > (a : 'a) (ret (result : borrowed 'a)) =
+    any [ ret (fin : 'a) (id: int) -> (! ret { { current = a; final = fin; id = id } })]
+
+  function borrow_logic (cur fin : 'a) (id : int) : borrowed 'a = { current = cur; final = fin; id = id }
+
+  function get_id (x : borrowed 'a) : int = x.id
+  function inherit_id (old_id inherit_path: int) : int
+end
+module Snapshot
+  type snap_ty 't
+
+  function new (x : 't) : snap_ty 't
+  function inner (x : snap_ty 't) : 't
+
+  axiom new_spec [@rewrite] : forall x: 't [new x]. inner (new x) = x
+  axiom inner_spec [@rewrite]: forall x: snap_ty 't [inner x]. new (inner x) = x
+end
+module Intrinsic
+  function any_l (a :'a) : 'b
+end
+module UInt32
+  use int.Int
+
+  type uint32 = < range -0x0 0xffff_ffff >
+
+  constant min : int = - 0x0
+  constant max : int =   0xffff_ffff
+
+  function to_int (x : uint32) : int = uint32'int x
+  meta coercion function to_int
+  meta "model_projection" function to_int
+
+  predicate in_bounds (n:int) = min <= n <= max
+
+  axiom to_int_in_bounds: forall n:uint32. in_bounds n
+
+  let of_int (n:int) { [@expl:integer overflow] in_bounds n }
+    (ret (result :uint32) { result = n }) = any
+
+  let add (a:uint32) (b:uint32) { [@expl:integer overflow] in_bounds (a + b) } (ret (result :uint32) { result = a + b }) = any
+
+  let sub (a:uint32) (b:uint32) { [@expl:integer overflow] in_bounds (a - b) } (ret (result :uint32) { result = a - b }) = any
+
+  let mul (a:uint32) (b:uint32) { [@expl:integer overflow] in_bounds (a * b) } (ret (result :uint32) { result = a * b }) = any
+
+  let neg (a:uint32) { [@expl:integer overflow] in_bounds (- a) } (ret (result :uint32) { result = - a }) = any
+
+  axiom extensionality: forall x y: uint32. to_int x = to_int y -> x = y
+
+  let eq (a:uint32) (b:uint32) (ret (result : bool) { result <-> a = b } { to_int a = to_int b -> result }) = any
+
+  let ne (a:uint32) (b:uint32) (ret (result : bool) { result <-> a <> b } { to_int a <> to_int b -> result }) = any
+
+  let le (a:uint32) (b:uint32) (ret (result : bool) { result <-> to_int a <= to_int b }) = any
+
+  let lt (a:uint32) (b:uint32) (ret (result : bool) { result <-> to_int a < to_int b }) = any
+
+  let ge (a:uint32) (b:uint32) (ret (result : bool) { result <-> to_int a >= to_int b }) = any
+
+  let gt (a:uint32) (b:uint32) (ret (result : bool) { result <-> to_int a > to_int b }) = any
+
+  use int.ComputerDivision
+
+  let div (a:uint32) (b:uint32)
+    { [@expl:division by zero] b <> 0 }
+    { [@expl:integer overflow] in_bounds (div a b) }
+    (ret (result :uint32) { result = div a b }) = any
+
+  let rem (a:uint32) (b:uint32)
+    { [@expl:division by zero] b <> 0 }
+    { [@expl:integer overflow] in_bounds (mod a b) }
+    (ret (result :uint32) { result = mod a b }) = any
+end
+module Int
+  use export mach.int.Int
+end