Merge branch 'main' of https://github.com/JetBrains-Research/verified…

…-cogen

.gitignore

@@ -15,3 +15,5 @@ log
 run.sh
 /dist/
 **/.pytest_cache
+run_nagini.py
+/tmp

gui/src/helpers.rs

@@ -3,6 +3,8 @@ use std::{
     process::{Command, Output},
 };
 
+use eframe::egui::{self, TextEdit};
+
 use crate::Settings;
 
 pub fn basename(file: &str) -> &str {
@@ -36,15 +38,36 @@ fn make_retries(retries: &str) -> String {
     }
 }
 
-fn add_common_arguments(cmd: &mut Command, token: &str, settings: &Settings) {
+fn make_timeout(timeout: &str) -> String {
+    if timeout.is_empty() {
+        String::from("60")
+    } else {
+        timeout.to_string()
+    }
+}
+
+fn make_runs(runs: &str) -> String {
+    if runs.is_empty() {
+        String::from("1")
+    } else {
+        runs.to_string()
+    }
+}
+
+fn add_common_arguments<'a>(
+    cmd: &'a mut Command,
+    token: &str,
+    settings: &Settings,
+) -> &'a mut Command {
     cmd.args(["--verifier-command", &settings.verifier_command])
         .args(["--prompts-directory", &settings.prompts_directory])
         .args(["--insert-conditions-mode", "llm-single-step"])
         .args(["--llm-profile", settings.llm_profile.as_grazie()])
         .args(["--grazie-token", token])
         .args(["--bench-type", &settings.bench_type.to_string()])
         .args(["--tries", &make_tries(&settings.tries)])
-        .args(["--retries", &make_retries(&settings.retries)]);
+        .args(["--retries", &make_retries(&settings.retries)])
+        .args(["--verifier-timeout", &make_timeout(&settings.timeout)])
 }
 
 fn parse_output(output: Output) -> (String, String) {
@@ -56,28 +79,30 @@ fn parse_output(output: Output) -> (String, String) {
 pub fn run_on_file(file: &str, settings: &Settings) -> (String, String) {
     log::info!("Running on file: {}", file);
 
-    let mut command = compose_command(settings);
-    add_common_arguments(&mut command, &settings.grazie_token, settings);
-
-    let output = command
-        .args(["-i", file])
-        .output()
-        .expect("Failed to run python to add information");
+    let output = add_common_arguments(
+        &mut compose_command(settings),
+        &settings.grazie_token,
+        settings,
+    )
+    .args(["-i", file])
+    .output()
+    .expect("Failed to run python to add information");
 
     parse_output(output)
 }
 
 pub fn run_on_directory(directory: &str, settings: &Settings) -> (String, String) {
     log::info!("Running on directory: {}", directory);
 
-    let mut command = compose_command(settings);
-    add_common_arguments(&mut command, &settings.grazie_token, settings);
-
-    let output = command
-        .args(["-d", directory])
-        .args(["--runs", &settings.runs])
-        .output()
-        .expect("Failed to run python to add information");
+    let output = add_common_arguments(
+        &mut compose_command(settings),
+        &settings.grazie_token,
+        settings,
+    )
+    .args(["-d", directory])
+    .args(["--runs", &make_runs(&settings.runs)])
+    .output()
+    .expect("Failed to run python to add information");
 
     parse_output(output)
 }
@@ -91,3 +116,17 @@ fn compose_command(settings: &Settings) -> Command {
         Command::new(&settings.generate_command)
     }
 }
+
+pub fn integer_edit_field(
+    ui: &mut egui::Ui,
+    hint: &str,
+    value: &mut String,
+    size: [f32; 2],
+) -> egui::Response {
+    let mut tmp_value = value.clone();
+    let res = ui.add_sized(size, TextEdit::singleline(&mut tmp_value).hint_text(hint));
+    if tmp_value.parse::<u8>().is_ok() || tmp_value.is_empty() {
+        *value = tmp_value;
+    }
+    res
+}

gui/src/main.rs

@@ -13,7 +13,7 @@ use std::{
 use once_cell::sync::Lazy;
 use serde::{Deserialize, Serialize};
 
-use helpers::{basename, extension, run_on_directory, run_on_file};
+use helpers::{basename, extension, integer_edit_field, run_on_directory, run_on_file};
 
 static APP_DIRS: Lazy<directories::ProjectDirs> = Lazy::new(|| {
     directories::ProjectDirs::from("", "", "verified-cogen").expect("Failed to get app directories")
@@ -149,6 +149,7 @@ struct Settings {
     bench_type: BenchMode,
     file_mode: FileMode,
     runs: String,
+    timeout: String,
 }
 
 impl Default for Settings {
@@ -165,6 +166,7 @@ impl Default for Settings {
             bench_type: BenchMode::Invariants,
             file_mode: FileMode::SingleFile,
             runs: String::from("1"),
+            timeout: String::from("60"),
         }
     }
 }
@@ -272,10 +274,6 @@ impl AppState {
                             if let Some(log) = log.as_ref() {
                                 *stderr += &format!("\nLog:\n{}", log)
                             }
-
-                            if let Ok(mut last_verified_extension) = last_verified_ext.write() {
-                                *last_verified_extension = None;
-                            }
                         }
                     }
                     *log = None;
@@ -360,6 +358,22 @@ impl AppState {
         }
     }
 
+    fn runner(&mut self, ui: &mut Ui) {
+        ui.horizontal(|ui| {
+            self.file_picker(ui);
+
+            let is_running = self.running.load(std::sync::atomic::Ordering::SeqCst);
+
+            if ui.button("Run").clicked() && !is_running {
+                self.run();
+            }
+
+            if is_running {
+                ui.spinner();
+            }
+        });
+    }
+
     fn token_input(&mut self, ui: &mut Ui) {
         let label = ui.heading("Grazie and verifier: ");
 
@@ -374,32 +388,41 @@ impl AppState {
                 .labelled_by(label.id);
             self.token_hovered = token.hovered();
         });
+    }
+
+    fn verifier_details(&mut self, ui: &mut Ui) {
+        ui.label("Prompts directory: ");
+        ui.horizontal(|ui| {
+            ui.add(
+                TextEdit::singleline(&mut self.settings.prompts_directory)
+                    .hint_text("Enter the prompts directory"),
+            );
+            if ui.button("Select").clicked() {
+                if let Some(dir) = rfd::FileDialog::new().pick_folder() {
+                    self.settings.prompts_directory = dir.to_string_lossy().to_string();
+                }
+            }
+        });
 
         ui.columns(2, |cols| {
             let [left_ui, right_ui] = cols else { return };
 
             left_ui.vertical(|ui| {
-                ui.horizontal(|ui| {
-                    ui.label("Prompts directory: ");
-                    if ui.button("Select").clicked() {
-                        if let Some(dir) = rfd::FileDialog::new().pick_folder() {
-                            self.settings.prompts_directory = dir.to_string_lossy().to_string();
-                        }
-                    }
-                });
-                ui.add(
-                    TextEdit::singleline(&mut self.settings.prompts_directory)
-                        .hint_text("Enter the prompts directory"),
-                );
-            });
-
-            right_ui.vertical(|ui| {
                 ui.label("Verifier command: ");
                 ui.add(
                     TextEdit::singleline(&mut self.settings.verifier_command)
                         .hint_text("Enter the verifier command"),
                 );
             });
+
+            right_ui.vertical(|ui| {
+                ui.label("Timeout: ");
+                let mut tmp_value = self.settings.timeout.clone();
+                ui.add(TextEdit::singleline(&mut tmp_value).hint_text("Enter the timeout"));
+                if tmp_value.parse::<u8>().is_ok() || tmp_value.is_empty() {
+                    self.settings.timeout = tmp_value;
+                }
+            });
         });
 
         ui.label("Generate code: ");
@@ -415,38 +438,11 @@ impl AppState {
         });
     }
 
-    fn runner(&mut self, ui: &mut Ui) {
-        ui.horizontal(|ui| {
-            self.file_picker(ui);
-
-            let is_running = self.running.load(std::sync::atomic::Ordering::SeqCst);
-
-            if ui.button("Run").clicked() && !is_running {
-                self.run();
-            }
-
-            if is_running {
-                ui.spinner();
-            }
-        });
-    }
-
     fn settings_ui(&mut self, ui: &mut Ui) {
-        fn integer_edit_field(
-            ui: &mut egui::Ui,
-            hint: &str,
-            value: &mut String,
-            size: [f32; 2],
-        ) -> egui::Response {
-            let mut tmp_value = value.clone();
-            let res = ui.add_sized(size, TextEdit::singleline(&mut tmp_value).hint_text(hint));
-            if tmp_value.parse::<u8>().is_ok() || tmp_value.is_empty() {
-                *value = tmp_value;
-            }
-            res
-        }
-
         ui.vertical(|ui| {
+            self.verifier_details(ui);
+            ui.separator();
+
             ui.heading("Settings:");
 
             egui::ComboBox::from_label("LLM Profile")

prompts/nagini_invariants/timeout.txt

@@ -0,0 +1,3 @@
+The verifier timed out during the verification.
+This usually means that the provided invariants were too broad or were difficult to check.
+Could you please try to improve the invariants and try again?

prompts/rust_invariants/timeout.txt

@@ -0,0 +1,3 @@
+The verifier timed out during the verification.
+This usually means that the provided invariants were too broad or were difficult to check.
+Could you please try to improve the invariants and try again?

prompts/rust_invariants_with_examples/timeout.txt

@@ -0,0 +1,3 @@
+The verifier timed out during the verification.
+This usually means that the provided invariants were too broad or were difficult to check.
+Could you please try to improve the invariants and try again?