feat: added ci option (#328)

* feat: added ci option

* cleanup

Author: andrii-a8c

.github/workflows/sui-prover.yml

@@ -130,13 +130,13 @@ jobs:
           git clone https://github.com/asymptotic-code/sui-kit.git sui-kit
 
           cd sui-kit/examples/amm
-          sui-prover
+          sui-prover --ci
 
           cd ../showcase
-          sui-prover
+          sui-prover --ci
 
           cd ../guide
-          sui-prover
+          sui-prover --ci
 
   internal-tests:
     # check if prover needed
@@ -229,10 +229,10 @@ jobs:
           git clone https://github.com/asymptotic-code/integer-library int-lib
 
           cd int-lib/specs
-          sui-prover
+          sui-prover --ci
 
           cd ../specs-bv
-          sui-prover --no-bv-int-encoding
+          sui-prover --no-bv-int-encoding --ci
 
   token-distribution-specs:
     needs: build-prover
@@ -270,7 +270,7 @@ jobs:
         run: |
           git clone --depth 1 -b fix/prover_specs https://github.com/asymptotic-code/sui-smart-contracts.git sui-smart-contracts
           cd sui-smart-contracts/token-distribution-specs 
-          sui-prover
+          sui-prover --ci
 
   scallop-bpl-generation:
     needs: build-prover
@@ -315,7 +315,7 @@ jobs:
       - name: Run
         run: |
           cd scallop/contracts/specs
-          sui-prover -g
+          sui-prover -g --ci
 
   cetus-bpl-generation:
     needs: build-prover
@@ -360,4 +360,4 @@ jobs:
       - name: Run
         run: |
           cd cetus/cetus_clmm_specs
-          sui-prover -g
+          sui-prover -g --ci

crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs

@@ -231,6 +231,17 @@ impl<'env> BoogieWrapper<'env> {
         individual_timeout: Option<u64>,
         individual_options: Option<String>,
     ) -> anyhow::Result<BoogieOutput> {
+        if self.options.ci {
+            if individual_timeout.is_some() {
+                println!("Individual Timeout: {:?}", individual_timeout.unwrap());
+            }
+            if individual_options.is_some() {
+                println!(
+                    "Individual Boogie Options: {:?}",
+                    individual_options.clone().unwrap()
+                );
+            }
+        }
         let res = self
             .call_remote(
                 boogie_file,
@@ -252,7 +263,20 @@ impl<'env> BoogieWrapper<'env> {
     ) -> anyhow::Result<BoogieOutput> {
         let args = self
             .options
-            .get_boogie_command(boogie_file, individual_options)?;
+            .get_boogie_command(boogie_file, individual_options.clone())?;
+
+        if self.options.ci {
+            println!("Boogie Execution Command: {}", args.iter().join(" "));
+            if individual_timeout.is_some() {
+                println!("Individual Timeout: {:?}", individual_timeout.unwrap());
+            }
+            if individual_options.is_some() {
+                println!(
+                    "Individual Boogie Options: {:?}",
+                    individual_options.unwrap()
+                );
+            }
+        }
         info!("running solver");
         debug!("command line: {}", args.iter().join(" "));
 

crates/move-prover-boogie-backend/src/boogie_backend/options.rs

@@ -164,6 +164,8 @@ pub struct BoogieOptions {
     pub sequential_task: bool,
     /// Whether to force timeout handling
     pub force_timeout: bool,
+    /// Whether to enable CI mode for continuous integration environments
+    pub ci: bool,
     /// A hard timeout for boogie execution; if the process does not terminate within
     /// this time frame, it will be killed. Zero for no timeout.
     pub hard_timeout_secs: u64,
@@ -236,6 +238,7 @@ impl Default for BoogieOptions {
             spec_no_abort_check_only: false,
             func_abort_check_only: false,
             no_verify: false,
+            ci: false,
         }
     }
 }

crates/move-stackless-bytecode/src/function_target_pipeline.rs

@@ -524,6 +524,14 @@ impl FunctionTargetsHolder {
             }
 
             if *focus {
+                if self.prover_options.ci {
+                    func_env.module_env.env.diag(
+                        Severity::Error,
+                        &func_env.get_loc(),
+                        "The 'focus' attribute is restricted in CI mode.",
+                    );
+                    return;
+                }
                 self.focus_specs.insert(func_env.get_qualified_id());
             } else {
                 self.no_focus_specs.insert(func_env.get_qualified_id());

crates/move-stackless-bytecode/src/options.rs

@@ -94,6 +94,8 @@ pub struct ProverOptions {
     pub bv_int_encoding: bool,
     /// Skip checking spec functions that do not abort
     pub skip_spec_no_abort: bool,
+    /// CI mode
+    pub ci: bool,
 }
 
 // add custom struct for mutation options
@@ -131,6 +133,7 @@ impl Default for ProverOptions {
             ban_int_2_bv: false,
             bv_int_encoding: true,
             skip_spec_no_abort: false,
+            ci: false,
         }
     }
 }

crates/sui-prover/src/prove.rs

@@ -113,6 +113,10 @@ pub struct GeneralConfig {
     /// Dump control-flow graphs to file
     #[clap(name = "stats", long, global = false)]
     pub stats: bool,
+
+    /// Whether to enable CI mode for continuous integration environments
+    #[clap(name = "ci", long, global = false)]
+    pub ci: bool,
 }
 
 #[derive(Args, Default)]
@@ -273,6 +277,8 @@ async fn execute_backend_boogie(
     options.remote = remote_config.to_config()?;
     options.prover.skip_spec_no_abort = general_config.skip_spec_no_abort;
     options.backend.force_timeout = general_config.force_timeout;
+    options.backend.ci = general_config.ci;
+    options.prover.ci = general_config.ci;
 
     if general_config.explain {
         let mut error_writer = Buffer::no_color();