CN: support enum constants in CN syntax

Enumerated constants are already "normal" identifiers in the Cerberus pipeline,
and were thus already parsed in CN annotations, but they were then treated like
local variables with nonsensical results. Instead, a fiddly mechanism inserted
via a state hook converts their value to a CN counterpart, permitting all enum
constants (which can be converted) to be used in expression positions in CN.

backend/cn/compile.ml

@@ -47,14 +47,14 @@ type env = {
   tagDefs: Mu.mu_tag_definitions;
 }
 
-let empty tagDefs =
+let init_env tagDefs =
   { computationals = SymMap.empty;
     logicals= SymMap.empty; 
     predicates= SymMap.empty;
     functions = SymMap.empty; 
     datatypes = SymMap.empty; 
     datatype_constrs = SymMap.empty;
-    tagDefs; 
+    tagDefs;
   }
 
 
@@ -350,6 +350,33 @@ let add_datatype_infos env dts =
   ListM.fold_leftM add_datatype_info env dts
 
 
+exception Convert_enum_failed of string
+
+let str_ail_const c = Pp.plain (CF.Pp_ail_ast.pp_constant c)
+let str_ail_expr_constr e =
+  Pp.plain (CF.Pp_ast.doc_tree_toplevel
+    (CF.Pp_ail_ast.dtree_of_expression (fun _ -> (!^ "()")) e))
+
+(* TODO: handle more kinds of constant expression *)
+let convert_enum_expr_to_cn =
+  let open CF.AilSyntax in
+  let conv_const loc = function
+    | ConstantInteger (IConstant (z, _, _)) -> CNExpr (loc, CNExpr_const (CNConst_integer z))
+    | c -> raise (Convert_enum_failed ("unhandled constant: " ^ str_ail_const c))
+  in
+  let rec conv_expr_ e1 loc = function
+    | AilEconst const -> conv_const loc const
+    | AilEannot (cty, expr) -> conv_expr expr
+    | e -> raise (Convert_enum_failed ("unhandled expression: " ^ str_ail_expr_constr e1))
+  and conv_expr e = match e with
+    | AnnotatedExpression (_, _, loc, expr) -> conv_expr_ e loc expr
+  in
+  fun expr -> try
+    Either.Left (conv_expr expr)
+  with
+    | Convert_enum_failed s -> Either.Right s
+
+
 module E = struct
 
   type evaluation_scope = string

backend/cn/core_to_mucore.ml

@@ -53,6 +53,10 @@ let do_ail_desugar_rdonly desugar_state f =
   let@ (x, _) = do_ail_desugar_op desugar_state f in
   return x
 
+let add_enum_hook desugar_state =
+  CAE.{ desugar_state with cn_state =
+    Cn_desugaring.{ desugar_state.cn_state with cn_enum_hook = C.convert_enum_expr_to_cn } }
+
 let register_new_cn_local id d_st =
   do_ail_desugar_op d_st (CA.register_additional_cn_var id)
 
@@ -1026,7 +1030,9 @@ let make_fun_with_spec_args f_i loc env args requires =
 let desugar_access d_st global_types (loc, id) =
   let@ (s, var_kind) = do_ail_desugar_rdonly d_st (CAE.resolve_cn_ident CN_vars id) in
   let@ () = match var_kind with
-    | Var_kind_c -> return ()
+    | Var_kind_c C_kind_var -> return ()
+    | Var_kind_c C_kind_enum ->
+       fail {loc; msg = Generic (!^"accesses: expected global, not enum constant")}
     | Var_kind_cn ->
        let msg = 
          !^"The name" ^^^ squotes (Id.pp id) 
@@ -1172,9 +1178,9 @@ let normalise_fun_map_decl
          Sym.equal fname ail_prog.function_definitions in
      (* let ail_env = Pmap.find ail_marker ail_prog.markers_env in *)
      (* let d_st = CAE.set_cn_c_identifier_env ail_env d_st in *)
-     let d_st = 
-       CAE.{ inner = Pmap.find ail_marker markers_env;
-                            markers_env = markers_env }
+     let d_st =
+       CAE.{ inner = add_enum_hook (Pmap.find ail_marker markers_env);
+               markers_env = markers_env }
      in
      let@ trusted, accesses, requires, ensures, mk_functions = Parse.parse_function_spec attrs in
      Print.debug 6 (lazy (Print.string "parsed spec attrs"));
@@ -1308,15 +1314,15 @@ let normalise_fun_map
 
 
 
-let normalise_globs tagDefs sym g =
+let normalise_globs env sym g =
   let loc = Loc.unknown in
   match g with
   | GlobalDef ((bt, ct), e) -> 
      assert (BT.equal BT.Loc (convert_bt loc bt));
      (* this may have to change *)
      let@ e = 
        n_expr loc 
-         ((C.empty tagDefs, (C.LocalState.init_st).old_states), 
+         ((env, (C.LocalState.init_st).old_states),
           (Pmap.empty Int.compare, 
            CF.Cn_desugaring.initial_cn_desugaring_state [])) 
          ([], Pmap.empty Int.compare)
@@ -1328,9 +1334,9 @@ let normalise_globs tagDefs sym g =
      return (M_GlobalDecl (convert_ct loc ct))
 
 
-let normalise_globs_list tagDefs gs = 
+let normalise_globs_list env gs =
    ListM.mapM (fun (sym,g) -> 
-       let@ g = normalise_globs tagDefs sym g in
+       let@ g = normalise_globs env sym g in
        return (sym, g)
      ) gs
 
@@ -1410,7 +1416,7 @@ let normalise_file (markers_env, ail_prog) file =
 
   let tagDefs = normalise_tag_definitions file.mi_tagDefs in
 
-  let env = C.empty tagDefs in
+  let env = C.init_env tagDefs in
   let@ env = C.add_datatype_infos env ail_prog.cn_datatypes in
   let@ env = C.register_cn_functions env ail_prog.cn_functions in
   let@ lfuns = ListM.mapM (C.translate_cn_function env) ail_prog.cn_functions in
@@ -1426,7 +1432,7 @@ let normalise_file (markers_env, ail_prog) file =
       ) file.mi_globs
   in
 
-  let@ globs = normalise_globs_list tagDefs file.mi_globs in
+  let@ globs = normalise_globs_list env file.mi_globs in
 
   let env = List.fold_left register_glob env globs in
 

frontend/model/cabs_to_ail.lem

@@ -4154,7 +4154,12 @@ let rec desugar_cn_expr (CNExpr loc expr_) =
         E.resolve_cn_ident CN_vars ident >>= fun (sym, kind) ->
         match kind with
         | Var_kind_cn -> E.return (CNExpr_var sym)
-        | Var_kind_c -> E.return (CNExpr_value_of_c_variable sym)
+        | Var_kind_c C_kind_var -> E.return (CNExpr_value_of_c_variable sym)
+        | Var_kind_c C_kind_enum ->
+            E.resolve_enum_constant sym >>= fun expr_ ->
+            let expr = A.AnnotatedExpression () [] loc expr_ in
+            E.convert_enum_expr loc expr >>= fun (CNExpr _ expr_) ->
+            E.return expr_
         end
     | CNExpr_list es ->
         CNExpr_list <$> E.mapM desugar_cn_expr es

frontend/model/cabs_to_ail_effect.lem

@@ -989,18 +989,25 @@ let resolve_cn_ident_opt ns ident =
   get_inner >>= fun inner ->
   let st = inner.cn_state in
 
+  let c_var_kind (kind : identifier_kind) = match kind with
+     | Kind_ordinary OK_enum_constant -> Cn.Var_kind_c Cn.C_kind_enum
+     | Kind_ordinary _ -> Cn.Var_kind_c Cn.C_kind_var
+     | _ -> error "resolve_cn_ident_opt: not Kind_ordinary"
+     end
+  in
+
   (* based on earlier Cabs_to_ail_effect code  *)
   let lookup_in_c_desugaring_state () =
      match Scope_table.resolve (ident, Namespace_ordinary) inner.registered_identifiers with
      | Nothing -> 
         Nothing
-     | Just (_, Internal sym _kind _linkage) -> 
-        Just (sym, Cn.Var_kind_c)
+     | Just (_, Internal sym kind _linkage) ->
+        Just (sym, c_var_kind kind)
      | Just (_, External) ->
         match Map.lookup (ident, Namespace_ordinary) inner.registered_external_identifiers with
         | Nothing -> Nothing
-        | Just (_scope, (sym, _identifier_kind, _linkage)) ->
-           Just (sym, Cn.Var_kind_c)
+        | Just (_scope, (sym, kind, _linkage)) ->
+           Just (sym, c_var_kind kind)
         end
      end
   in
@@ -1018,7 +1025,7 @@ let resolve_cn_ident_opt ns ident =
           end
     end
   in
-  
+
   let result = match ns with
     | Cn.CN_vars ->
        match lookup_in_c_desugaring_state () with
@@ -1252,6 +1259,15 @@ let register_cn_datatype ident mk_cases =
         fail (Loc.locOf ident) (Errors.Desugar_CN (Cn.CNErr_redeclaration Cn.CN_datatype_nm))
   end
 
+let convert_enum_expr loc expr =
+  get_inner >>= fun st ->
+  match st.cn_state.Cn_desugaring.cn_enum_hook expr with
+    | Left res -> return res
+    | Right msg ->
+        fail loc (Errors.Desugar_CN
+            (Cn.CNErr_general ("error converting enum: " ^ msg)))
+  end
+
 
 (* END CN *)
 

frontend/model/cn.lem

@@ -2,14 +2,17 @@ open import Pervasives
 import Symbol Ctype
 
 (* for desugaring *)
+type cn_c_kind =
+  | C_kind_var
+  | C_kind_enum
 
 type cn_var_kind =
-  | Var_kind_c
+  | Var_kind_c of cn_c_kind
   | Var_kind_cn
 
 let ensure_not_c_variable = function
   | (sym, Var_kind_cn) -> sym
-  | (sym, Var_kind_c) -> Assert_extra.failwith "unexpected c variable"
+  | (sym, Var_kind_c _) -> Assert_extra.failwith "unexpected c variable"
 end
 
 

frontend/model/cn_desugaring.lem

@@ -15,6 +15,7 @@ type cn_desugaring_state = <|
   cn_lemmata: list (Symbol.identifier * (Symbol.sym * cn_lemma Symbol.sym Ctype.ctype));
   cn_fun_specs: list (nat * cn_fun_spec Symbol.sym Ctype.ctype);
   cn_type_synonyms: map Symbol.identifier (cn_base_type Symbol.sym);
+  cn_enum_hook: AilSyntax.expression unit -> either (Cn.cn_expr Symbol.sym Ctype.ctype) string;
 |>
 
 let initial_cn_desugaring_state cn_initial_function_identifiers = 
@@ -35,6 +36,7 @@ let initial_cn_desugaring_state cn_initial_function_identifiers =
   cn_lemmata= [];
   cn_fun_specs= [];
   cn_type_synonyms= Map.empty;
+  cn_enum_hook= (fun _ -> Right "enum conversion not installed");
   (* cn_c_identifier_env= Map.empty; *)
 |>
 

ocaml_frontend/cn_ocaml.ml

@@ -97,6 +97,10 @@ module MakePp (Conf: PP_CN) = struct
     | CN_and -> P.ampersand ^^ P.ampersand
     | CN_map_get -> P.string "CN_map_get"
 
+  let pp_cn_c_kind = function
+    | C_kind_var -> !^ "c_var"
+    | C_kind_enum -> !^ "c_enum_constant"
+
 
 
   let rec dtree_of_cn_pattern (CNPat (_, pat_)) = 
@@ -202,7 +206,8 @@ module MakePp (Conf: PP_CN) = struct
       | CNExpr_deref e ->
           Dnode (pp_ctor "CNExpr_deref", [dtree_of_cn_expr e])
       | CNExpr_value_of_c_variable ident ->
-          Dleaf (pp_ctor "CNExpr_value_of_c_variable" ^^^ Conf.pp_ident ident)
+          Dnode (pp_ctor "CNExpr_value_of_c_variable"
+               , [Dleaf (Conf.pp_ident ident)])
       | CNExpr_unchanged e ->
           Dnode (pp_ctor "CNExpr_unchanged", [dtree_of_cn_expr e])
       | CNExpr_at_env (e, env_name) ->

ocaml_frontend/pprinters/pp_ast.ml

@@ -10,6 +10,11 @@ type doc_tree =
   | Dnode of P.document * doc_tree list
   | Dnode_attrs of P.document * Annot.attributes * doc_tree list
 
+let doc_tree_toplevel = function
+  | Dleaf p -> p
+  | Dleaf_attrs (p, _) -> p
+  | Dnode (p, _) -> p
+  | Dnode_attrs (p, _, _) -> p
 
 let add_dtree_of_attributes (Annot.Attrs xs) dtrees =
   let open Annot in