Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 22 insertions, 14 deletions

diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index d35cd5d8..ccc870dc 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -1,10 +1,10 @@
-open Identifiers
 open Names
 open Types
 open Values
 open Expressions
-
+open Identifiers
 module FunDeclId = IdGen ()
+module GlobalDeclId = IdGen ()
 
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
@@ -36,6 +36,9 @@ type assumed_fun_id =
 type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
 [@@deriving show, ord]
 
+type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
+[@@deriving show]
+
 type assertion = { cond : operand; expected : bool } [@@deriving show]
 
 type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
@@ -77,20 +80,16 @@ class ['self] iter_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
-    method visit_place : 'env -> place -> unit = fun _ _ -> ()
+    method visit_global_assignment : 'env -> global_assignment -> unit =
+      fun _ _ -> ()
 
+    method visit_place : 'env -> place -> unit = fun _ _ -> ()
     method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
-
     method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
-
     method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
-
     method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
-
     method visit_call : 'env -> call -> unit = fun _ _ -> ()
-
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-
     method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
   end
 
@@ -99,16 +98,15 @@ class ['self] map_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
-    method visit_place : 'env -> place -> place = fun _ x -> x
+    method visit_global_assignment
+        : 'env -> global_assignment -> global_assignment =
+      fun _ x -> x
 
+    method visit_place : 'env -> place -> place = fun _ x -> x
     method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
-
     method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
-
     method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
-
     method visit_operand : 'env -> operand -> operand = fun _ x -> x
-
     method visit_call : 'env -> call -> call = fun _ x -> x
 
     method visit_integer_type : 'env -> integer_type -> integer_type =
@@ -120,6 +118,7 @@ class ['self] map_statement_base =
 
 type statement =
   | Assign of place * rvalue
+  | AssignGlobal of global_assignment
   | FakeRead of place
   | SetDiscriminant of place * VariantId.id
   | Drop of place
@@ -178,5 +177,14 @@ type fun_decl = {
   name : fun_name;
   signature : fun_sig;
   body : fun_body option;
+  is_global_decl_body : bool;
+}
+[@@deriving show]
+
+type global_decl = {
+  def_id : GlobalDeclId.id;
+  body_id : FunDeclId.id;
+  name : global_name;
+  ty : ety;
 }
 [@@deriving show]