Added Error to RawStatement (#208)

Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
AeneasVerif · Jun 4, 2024 · 438acf2 · 438acf2
1 parent f922038
commit 438acf2
Show file tree

Hide file tree

Showing 14 changed files with 27 additions and 7 deletions.
diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.5"
+let supported_charon_version = "0.1.6"
diff --git a/charon-ml/src/LlbcAst.ml b/charon-ml/src/LlbcAst.ml
@@ -31,6 +31,7 @@ and raw_statement =
   | Sequence of statement * statement
   | Switch of switch
   | Loop of statement
+  | Error of string
 
 and switch =
   | If of operand * statement * statement

diff --git a/charon-ml/src/LlbcAstUtils.ml b/charon-ml/src/LlbcAstUtils.ml
@@ -33,7 +33,7 @@ let mk_sequence (st1 : statement) (st2 : statement) : statement =
 let rec chain_statements (st1 : statement) (st2 : statement) : statement =
   match st1.content with
   | SetDiscriminant _ | Assert _ | Call _ | Assign _ | FakeRead _ | Drop _
-  | Loop _ ->
+  | Loop _ | Error _ ->
       (* Simply create a sequence *)
       mk_sequence st1 st2
   | Nop -> (* Ignore the nop *) st2

diff --git a/charon-ml/src/LlbcOfJson.ml b/charon-ml/src/LlbcOfJson.ml
@@ -70,6 +70,9 @@ and raw_statement_of_json (id_to_file : id_to_file_map) (js : json) :
     | `Assoc [ ("Loop", st) ] ->
         let* st = statement_of_json id_to_file st in
         Ok (Loop st)
+    | `Assoc [ ("Error", s) ] ->
+        let* s = string_of_json s in
+        Ok (Error s)
     | _ -> Error "")
 
 and switch_of_json (id_to_file : id_to_file_map) (js : json) :

diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml
@@ -107,6 +107,7 @@ module Ast = struct
         indent ^ "loop {\n"
         ^ statement_to_string env (indent ^ indent_incr) indent_incr loop_st
         ^ "\n" ^ indent ^ "}"
+    | Error s -> indent ^ "ERROR(' " ^ s ^ "')"
 
   let fun_sig_to_string (env : fmt_env) (indent : string) (indent_incr : string)
       (sg : fun_sig) : string =

diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.5"
+version = "0.1.6"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 

diff --git a/charon/src/ast/llbc_ast.rs b/charon/src/ast/llbc_ast.rs
@@ -59,6 +59,7 @@ pub enum RawStatement {
     Sequence(Box<Statement>, Box<Statement>),
     Switch(Switch),
     Loop(Box<Statement>),
+    Error(String),
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize)]

diff --git a/charon/src/ast/llbc_ast_utils.rs b/charon/src/ast/llbc_ast_utils.rs
@@ -178,6 +178,7 @@ pub trait AstVisitor: crate::expressions::ExprVisitor {
             RawStatement::Sequence(st1, st2) => self.visit_sequence(st1, st2),
             RawStatement::Switch(s) => self.visit_switch(s),
             RawStatement::Loop(lp) => self.visit_loop(lp),
+            RawStatement::Error(s) => self.visit_error(s),
         }
     }
 
@@ -211,6 +212,8 @@ pub trait AstVisitor: crate::expressions::ExprVisitor {
     fn visit_break(&mut self, _: &usize) {}
     fn visit_continue(&mut self, _: &usize) {}
     fn visit_nop(&mut self) {}
+    fn visit_error(&mut self, _: &String) {}
+
 
     fn visit_sequence(&mut self, st1: &Statement, st2: &Statement) {
         self.visit_statement(st1);

diff --git a/charon/src/ast/ullbc_ast.rs b/charon/src/ast/ullbc_ast.rs
@@ -37,6 +37,7 @@ pub enum RawStatement {
     StorageDead(VarId),
     /// We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC
     Deinit(Place),
+    Error(String),
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize)]

diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs
@@ -85,7 +85,8 @@ impl BlockData {
                 RawStatement::FakeRead(_)
                 | RawStatement::SetDiscriminant(_, _)
                 | RawStatement::StorageDead(_)
-                | RawStatement::Deinit(_) => {
+                | RawStatement::Deinit(_)
+                | RawStatement::Error(_) => {
                     // No operands: nothing to do
                 }
             }
@@ -187,6 +188,7 @@ pub trait AstVisitor: crate::expressions::ExprVisitor {
             SetDiscriminant(p, vid) => self.visit_set_discriminant(p, vid),
             StorageDead(vid) => self.visit_storage_dead(vid),
             Deinit(p) => self.visit_deinit(p),
+            Error(s) => self.visit_error(s),
         }
     }
 
@@ -211,6 +213,8 @@ pub trait AstVisitor: crate::expressions::ExprVisitor {
         self.visit_place(p);
     }
 
+    fn visit_error(&mut self, s: &String) {}
+
     fn visit_terminator(&mut self, st: &Terminator) {
         self.visit_span(&st.span);
         self.visit_raw_terminator(&st.content);

diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
@@ -789,6 +789,9 @@ impl<C: AstFormatter> FmtWithCtx<C> for ullbc::Statement {
             RawStatement::Deinit(place) => {
                 format!("@deinit({})", place.fmt_with_ctx(ctx))
             }
+            RawStatement::Error(s) => {
+                format!("@Error({})", s)
+            }
         }
     }
 }
@@ -932,6 +935,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for llbc::Statement {
                     tab
                 )
             }
+            RawStatement::Error(s) => format!("{tab}@ERROR({})", s),
         }
     }
 }

diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs
@@ -201,7 +201,7 @@ impl<'a> MutAstVisitor for Visitor<'a> {
                 self.visit_transform_place(false, p);
             }
             Assign(..) | SetDiscriminant(..) | Drop(..) | Assert(..) | Call(..) | Panic
-            | Return | Break(..) | Continue(..) | Nop | Switch(..) | Loop(..) => {
+            | Return | Break(..) | Continue(..) | Nop | Switch(..) | Loop(..) | Error(..) => {
                 // Explore
                 self.default_visit_raw_statement(st)
             }

diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs
@@ -1543,6 +1543,7 @@ fn translate_statement(st: &src::Statement) -> Option<tgt::Statement> {
             // We translate a deinit as a drop
             tgt::RawStatement::Drop(place.clone())
         }
+        src::RawStatement::Error(s) => tgt::RawStatement::Error(s.clone()),
     };
     Some(tgt::Statement::new(src_span, st))
 }
@@ -1755,7 +1756,8 @@ fn is_terminal_explore(num_loops: usize, st: &tgt::Statement) -> bool {
         | tgt::RawStatement::Drop(_)
         | tgt::RawStatement::Assert(_)
         | tgt::RawStatement::Call(_)
-        | tgt::RawStatement::Nop => false,
+        | tgt::RawStatement::Nop
+        | tgt::RawStatement::Error(_) => false,
         tgt::RawStatement::Panic | tgt::RawStatement::Return => true,
         tgt::RawStatement::Break(index) => *index >= num_loops,
         tgt::RawStatement::Continue(_index) => true,