Merge pull request #154 from project-everest/_nik_misc_fixes

A few miscellaneous fixes to 3D

src/3d/Ast.fst

@@ -1108,17 +1108,21 @@ let print_bitfield (bf:option field_bitwidth_t) =
      (print_typ a.bitfield_type)
      a.bitfield_from a.bitfield_to
 
-let rec print_field (f:field) : ML string =
+let rec print_field' (f:field) (with_comments:bool) : ML string =
   let field = 
     match f.v with
     | AtomicField f -> print_atomic_field f
     | RecordField f i -> Printf.sprintf "%s %s" (print_record f) i.v.name
     | SwitchCaseField f i -> Printf.sprintf "%s %s" (print_switch_case f) i.v. name
   in
-  match f.comments with 
-  | [] -> field
-  | comms -> Printf.sprintf "//%s\n%s" (String.concat "; " comms) field
-
+  if with_comments then 
+    match f.comments with 
+    | [] -> field
+    | comms -> Printf.sprintf "//%s\n%s" (String.concat "; " comms) field
+  else field
+
+and print_field f : ML string = print_field' f true 
+
 and print_record (f:record) : ML string = 
   List.map print_field f |>
   String.concat ";\n"

src/3d/BitFields.fst

@@ -168,7 +168,7 @@ let eliminate_one_decl (env:B.global_env) (d:decl) : ML decl =
   match d.d_decl.v with
   | Record names params where fields ->
     let i = with_dummy_range (to_ident' "_") in
-    let { v = RecordField fields _ } = rewrite_field env (with_dummy_range (RecordField fields i)) in
+    let { v = RecordField fields _ } = rewrite_field env (with_range (RecordField fields i) d.d_decl.range) in
     List.iter (fun f ->
       Options.debug_print_string
             (Printf.sprintf "Bitfields: Field %s has comments <%s>\n"

src/3d/Simplify.fst

@@ -119,6 +119,7 @@ let simplify_atomic_field (env:T.env_t) (f:atomic_field)
     let ft = simplify_typ env sf.field_type in
     let fa = simplify_field_array env sf.field_array_opt in
     let fc = sf.field_constraint |> map_opt (simplify_expr env) in
+    let fp = sf.field_probe |> map_opt (fun fp -> { fp with probe_length=simplify_expr env fp.probe_length } ) in
     let fact =
       match sf.field_action with
       | None -> None
@@ -127,7 +128,8 @@ let simplify_atomic_field (env:T.env_t) (f:atomic_field)
     let sf = { sf with field_type = ft;
                        field_array_opt = fa; 
                        field_constraint = fc;
-                       field_action = fact } in
+                       field_action = fact;
+                       field_probe = fp } in
     { f with v = sf }
 
 let rec simplify_field (env:T.env_t) (f:field)

src/3d/TranslateForInterpreter.fst

@@ -269,9 +269,7 @@ let dep_pair_with_action_parser p1 (a:T.lam T.action) (p2:A.ident & T.parser) =
 let extend_fieldname fieldname e = Printf.sprintf "%s.%s" fieldname e
 let ite_parser typename fieldname (e:T.expr) (then_:T.parser) (else_:T.parser) : ML T.parser =      
     let k, p1, p2 =
-      if T.parser_kind_eq then_.p_kind else_.p_kind
-      then then_.p_kind, then_, else_
-      else let k = pk_glb then_.p_kind else_.p_kind in
+      let k = pk_glb then_.p_kind else_.p_kind in
            k,
            mk_parser k then_.p_typ typename (extend_fieldname fieldname "case_left") (T.Parse_weaken_right then_ else_.p_kind),
            mk_parser k else_.p_typ typename (extend_fieldname fieldname "case_right") (T.Parse_weaken_left else_ then_.p_kind)

src/3d/TypeSizes.fst

@@ -300,7 +300,7 @@ let rec size_and_alignment_of_field (env:env_t)
         : ML (size & alignment & list field)
         = let field, field_size, field_alignment = size_and_alignment_of_field env should_align diag_enclosing_type_name f in
           let pad_size, padding_field =
-            let msg = Printf.sprintf "(preceding field %s)" (print_field field) in
+            let msg = Printf.sprintf "(preceding field %s)" (print_field' field false) in
             alignment_padding env should_align diag_enclosing_type_name msg offset field_alignment
           in
           let offset =
@@ -390,7 +390,7 @@ let rec size_and_alignment_of_field (env:env_t)
         if all_cases_fixed
         && not (Fixed? size)
         then error
-              "With the --align option, \
+              "With the 'aligned' qualifier, \
                all cases of a union with a fixed size \
                must have the same size; \
                union padding is not yet supported"

src/3d/tests/BoolSwitch.3d

@@ -8,4 +8,16 @@ casetype _T (Bool b)
       case false:
          UINT32 integer;
    }
-} T;
+} T;
+
+entrypoint
+casetype _S (Bool b)
+{
+   switch (b)
+   {
+      case true:
+         UINT32 f;
+      default:
+         UINT32 g;
+   }
+} S;