Config: Fix issue with abstract booleans in configuration

lib/json/sail_config.c

@@ -87,7 +87,12 @@ sail_config_json sail_config_get(size_t n, const char *key[])
     if (cJSON_IsObject(json)) {
       json = cJSON_GetObjectItemCaseSensitive(json, key[i]);
     } else {
-      sail_assert(false, "Failed to access config item");
+      fprintf(stderr, "Failed to access configuration item: '");
+      for (int j = 0; j < n; j++) {
+        fprintf(stderr, ".%s", key[i]);
+      }
+      fprintf(stderr, "'\n");
+      exit(EXIT_FAILURE);
     }
   }
 

lib/json/sail_config.h

@@ -67,7 +67,7 @@ void sail_config_set_file(const char *path);
 void sail_config_cleanup(void);
 
 /*
- * Get the JSON corresponding to some key
+ * Get the JSON corresponding to some key.
  */
 sail_config_json sail_config_get(const size_t n, const_sail_string key[]);
 

src/lib/anf.ml

@@ -840,7 +840,8 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
       wrap (mk_aexp (AE_val (AV_record (record, typ_of exp))))
   | E_typ (typ, exp) -> mk_aexp (AE_typ (anf exp, typ))
   | E_internal_assume (_nc, exp) -> anf exp
-  | E_sizeof (Nexp_aux (Nexp_id id, _)) -> mk_aexp (AE_val (AV_abstract (id, typ_of exp)))
+  | E_sizeof (Nexp_aux (Nexp_id id, _)) | E_constraint (NC_aux (NC_id id, _)) ->
+      mk_aexp (AE_val (AV_abstract (id, typ_of exp)))
   | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ ->
       (* Should be re-written by type checker *)
       Reporting.unreachable l __POS__ "encountered raw vector operation when converting to ANF" [@coverage off]

src/lib/type_check.ml

@@ -3500,9 +3500,12 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
       | Nexp_aux (Nexp_id id, _) when Env.is_abstract_typ id env -> annot_exp (E_sizeof nexp) (atom_typ nexp)
       | _ -> crule check_exp env (rewrite_sizeof l env (Env.expand_nexp_synonyms env nexp)) (atom_typ nexp)
     end
-  | E_constraint nc ->
+  | E_constraint nc -> begin
       Env.wf_constraint ~at:l env nc;
-      crule check_exp env (rewrite_nc env (Env.expand_constraint_synonyms env nc)) (atom_bool_typ nc)
+      match nc with
+      | NC_aux (NC_id id, _) when Env.is_abstract_typ id env -> annot_exp (E_constraint nc) (atom_bool_typ nc)
+      | _ -> crule check_exp env (rewrite_nc env (Env.expand_constraint_synonyms env nc)) (atom_bool_typ nc)
+    end
   | E_field (exp, field) -> begin
       let inferred_exp = irule infer_exp env exp in
       match Env.expand_synonyms env (typ_of inferred_exp) with

test/c/config_abstract_bool.expect

@@ -0,0 +1 @@
+R = 0xF

test/c/config_abstract_bool.json

@@ -0,0 +1,5 @@
+{
+    "have" : {
+        "ext" : true
+    }
+}

test/c/config_abstract_bool.sail

@@ -0,0 +1,29 @@
+default Order dec
+
+$include <prelude.sail>
+
+$option --abstract-types
+
+$iftarget c
+$c_in_main sail_config_set_file("config_abstract_bool.json");
+$c_in_main sail_set_abstract_have_ext();
+$c_in_main_post sail_config_cleanup();
+$else
+$option --config ../c/config_abstract_bool.json
+$endif
+
+type have_ext : Bool = config have.ext
+
+type bits_conf = bits(if have_ext then 4 else 5)
+
+register R : bits_conf
+
+val main : unit -> unit
+
+function main() = {
+  let x = R;
+  if length(x) == 4 then {
+    R = 0xF;
+    print_bits("R = ", R)
+  }
+}

test/lean/run_tests.py

@@ -65,6 +65,7 @@
     'constructor247',
     'config_vec_list',
     'deep_poly_nest',
+    'config_abstract_bool', # Register type unsupported in state.ml
 }
 
 print("Sail is {}".format(sail))