From d2d144d166fbce51c2324d224670b4d96edd1969 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 12 Aug 2022 23:18:23 +0000 Subject: [PATCH 01/12] basic support for #if/#else in expressions --- src/3d/Ast.fst | 7 +++- src/3d/Binding.fst | 6 +++ src/3d/Deps.fst | 1 + src/3d/Desugar.fst | 67 +++++++++++++++++++++++++++--- src/3d/InlineSingletonRecords.fst | 3 +- src/3d/Simplify.fst | 3 ++ src/3d/Target.fst | 4 +- src/3d/Target.fsti | 1 + src/3d/TranslateForInterpreter.fst | 22 ++++++---- src/3d/TypeSizes.fst | 3 +- src/3d/ocaml/lexer.mll | 3 ++ src/3d/ocaml/parser.mly | 15 +++++++ 12 files changed, 119 insertions(+), 16 deletions(-) diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst index 3e4457486..8af115880 100644 --- a/src/3d/Ast.fst +++ b/src/3d/Ast.fst @@ -243,6 +243,7 @@ type op = | LE of option integer_type | GE of option integer_type | IfThenElse + | HashIfThenElse | BitFieldOf of int //BitFieldOf_n(i, from, to); the integer is the size of i in bits | SizeOf | Cast : from:option integer_type -> to:integer_type -> op @@ -526,6 +527,7 @@ type decl' = | OutputType : out_typ -> decl' | ExternType : typedef_names -> decl' | ExternFn : ident -> typ -> list param -> decl' + | CompileTimeFlag : ident -> decl' [@@ PpxDerivingYoJson ] noeq @@ -738,7 +740,8 @@ let subst_decl' (s:subst) (d:decl') : ML decl' = CaseType names (subst_params s params) (subst_switch_case s cases) | OutputType _ | ExternType _ - | ExternFn _ _ _ -> d + | ExternFn _ _ _ + | CompileTimeFlag _ -> d let subst_decl (s:subst) (d:decl) : ML decl = decl_with_v d (subst_decl' s d.d_decl.v) (*** Printing the source AST; for debugging only **) @@ -790,6 +793,7 @@ let print_op = function | LE _ -> "<=" | GE _ -> ">=" | IfThenElse -> "ifthenelse" + | HashIfThenElse -> "#ifthenelse" | BitFieldOf i -> Printf.sprintf "bitfield_of(%d)" i | SizeOf -> "sizeof" | Cast _ t -> "(" ^ print_integer_type t ^ ")" @@ -993,6 +997,7 @@ let print_decl' (d:decl') : ML string = | OutputType out_t -> "Printing for output types is TBD" | ExternType _ -> "Printing for extern types is TBD" | ExternFn _ _ _ -> "Printing for extern functions is TBD" + | CompileTimeFlag i -> Printf.sprintf "[@@IfDef]val %s : bool" i.v.name let print_decl (d:decl) : ML string = match d.d_decl.comments with diff --git a/src/3d/Binding.fst b/src/3d/Binding.fst index cb3b907f2..7935fe7c1 100644 --- a/src/3d/Binding.fst +++ b/src/3d/Binding.fst @@ -69,6 +69,7 @@ let params_of_decl (d:decl) : list param = | OutputType _ -> [] | ExternType _ -> [] | ExternFn _ _ ps -> ps + | CompileTimeFlag _ -> [] let check_shadow (e:H.t ident' 'a) (i:ident) (r:range) = match H.try_find e i.v with @@ -1567,6 +1568,11 @@ let bind_decl (e:global_env) (d:decl) : ML decl = add_extern_fn e f d; d + | CompileTimeFlag i -> + let ms = nullary_macro tbool None in + add_global e i d (Inr ms); + d + let bind_decls (g:global_env) (p:list decl) : ML (list decl & global_env) = List.map (bind_decl g) p, g diff --git a/src/3d/Deps.fst b/src/3d/Deps.fst index 0aa7df84f..748096944 100644 --- a/src/3d/Deps.fst +++ b/src/3d/Deps.fst @@ -186,6 +186,7 @@ let scan_deps (fn:string) : ML scan_deps_t = | OutputType _ | ExternType _ | ExternFn _ _ _ -> [] //AR: no dependencies from the output/extern types yet + | CompileTimeFlag _ -> [] in let has_output_types (ds:list decl) : bool = diff --git a/src/3d/Desugar.fst b/src/3d/Desugar.fst index b9509920d..f94316937 100644 --- a/src/3d/Desugar.fst +++ b/src/3d/Desugar.fst @@ -31,8 +31,15 @@ module H = Hashtable abbreviations * Set the kind (Spec/Output/Extern) in the type nodes + + * Find variables in HashIfThenElse and hoist them as assumptions + and rewrite HashIfThenElse to IfThenElse *) +#push-options "--warn_error -272" //intentional top-level effect +let auxiliary_decls : ref (list decl) = FStar.ST.alloc [] +#pop-options + let check_desugared_enum_cases (cases:list enum_case) : ML (list ident) = List.map (function @@ -187,14 +194,61 @@ let resolve_ident (env:qenv) (i:ident) : ML ident = | Some m -> { i with v = { i.v with modul_name = Some m } })) -let rec resolve_expr' (env:qenv) (e:expr') : ML expr' = +let rec collect_ifdef_guards (env:qenv) (e:expr) + : ML unit + = match e.v with + | This -> error "'this' is not allowed in the guard of an #if" e.range + | Constant _ -> () + | Identifier i -> + if List.mem i.v.name env.local_names //it's a local name (e.g. a parameter name) + then error (Printf.sprintf "Identifier %s is not a compile-time macro but is used in a #if" i.v.name) e.range + else ( + //declare ident, if not already declared + let aux = !auxiliary_decls in + match List.tryFind + (fun d -> + match d.d_decl.v with + | CompileTimeFlag j -> i.v.name = j.v.name + | _ -> false) + aux + with + | None -> + IO.print_string (Printf.sprintf "Adding declaration of %s\n" i.v.name); + let d = mk_decl (CompileTimeFlag i) e.range [] false in + auxiliary_decls := d :: aux + | Some _ -> () //already declared + + ) + | App op args -> + begin + match op with + | And + | Or + | Not -> List.iter (collect_ifdef_guards env) args + | _ -> error "Only boolean expressions over identifiers are supported in #if guards" e.range + end + +let rec resolve_expr' (env:qenv) (e:expr') r : ML expr' = match e with | Constant _ -> e | Identifier i -> Identifier (resolve_ident env i) | This -> e - | App op args -> App op (List.map (resolve_expr env) args) - -and resolve_expr (env:qenv) (e:expr) : ML expr = { e with v = resolve_expr' env e.v } + | App op args -> + let args = List.map (resolve_expr env) args in + match op with + | HashIfThenElse -> + begin + match args with + | [guard; br1; br2] -> + collect_ifdef_guards env guard;//mark any variables as top-level IfDef symbols + App IfThenElse args //rewrite away the HashIfThenElse + | _ -> error "Unexpected arguments to a #if/#else" r + end + + | _ -> + App op args + +and resolve_expr (env:qenv) (e:expr) : ML expr = { e with v = resolve_expr' env e.v e.range } let resolve_typ_param (env:qenv) (p:typ_param) : ML typ_param = match p with @@ -366,10 +420,12 @@ let resolve_decl' (env:qenv) (d:decl') : ML decl' = let ret = resolve_typ env ret in let params, _ = resolve_params env params in ExternFn id ret params + | CompileTimeFlag i -> d let resolve_decl (env:qenv) (d:decl) : ML decl = decl_with_v d (resolve_decl' env d.d_decl.v) let desugar (genv:GlobalEnv.global_env) (mname:string) (p:prog) : ML prog = + auxiliary_decls := []; let decls, refinement = p in let decls = List.collect desugar_one_enum decls in let env = { @@ -382,7 +438,8 @@ let desugar (genv:GlobalEnv.global_env) (mname:string) (p:prog) : ML prog = } in H.insert env.extern_types (Ast.to_ident' "void") (); let decls = List.map (resolve_decl env) decls in - decls, + let aux = List.rev (!auxiliary_decls) in + aux@decls, (match refinement with | None -> None | Some tr -> diff --git a/src/3d/InlineSingletonRecords.fst b/src/3d/InlineSingletonRecords.fst index 8433fa23a..b8cc9fd5d 100644 --- a/src/3d/InlineSingletonRecords.fst +++ b/src/3d/InlineSingletonRecords.fst @@ -185,7 +185,8 @@ let simplify_decl (env:env) (d:decl) : ML decl = | OutputType _ | ExternType _ - | ExternFn _ _ _ -> d + | ExternFn _ _ _ + | CompileTimeFlag _ -> d let simplify_prog (p:list decl) = let env = H.create 10 in diff --git a/src/3d/Simplify.fst b/src/3d/Simplify.fst index e07033097..e2b1597d6 100644 --- a/src/3d/Simplify.fst +++ b/src/3d/Simplify.fst @@ -175,5 +175,8 @@ let simplify_decl (env:T.env_t) (d:decl) : ML decl = let params = List.map (fun (t, i, q) -> simplify_typ env t, i, q) params in decl_with_v d (ExternFn f ret params) + | CompileTimeFlag i -> d + + let simplify_prog benv senv (p:list decl) = List.map (simplify_decl (B.mk_env benv, senv)) p diff --git a/src/3d/Target.fst b/src/3d/Target.fst index c8d497a93..39e528f57 100644 --- a/src/3d/Target.fst +++ b/src/3d/Target.fst @@ -57,6 +57,7 @@ let rec parser_kind_eq k k' = let default_attrs = { is_hoisted = false; + is_if_def = false; is_exported = false; should_inline = false; comments = [] @@ -804,7 +805,8 @@ let print_definition (mname:string) (d:decl { Definition? (fst d)} ) : ML string let print_assumption (mname:string) (d:decl { Assumption? (fst d) } ) : ML string = match fst d with | Assumption (x, t) -> - Printf.sprintf "assume\nval %s : %s\n\n" + Printf.sprintf "%sassume\nval %s : %s\n\n" + (if (snd d).is_if_def then "[@@ CIfDef ]\n" else "") (print_ident x) (print_typ mname t) diff --git a/src/3d/Target.fsti b/src/3d/Target.fsti index 7ca2f6077..15ee4195a 100644 --- a/src/3d/Target.fsti +++ b/src/3d/Target.fsti @@ -359,6 +359,7 @@ let assumption = A.ident * typ type decl_attributes = { is_hoisted: bool; is_exported: bool; + is_if_def: bool; should_inline: bool; comments: list string; } diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index 2314e7456..6eb337a0d 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -274,9 +274,11 @@ let translate_op : A.op -> ML T.op = | Cast (Some from) to -> T.Cast from to | Ext s -> T.Ext s | Cast None _ + | HashIfThenElse | SizeOf -> failwith (Printf.sprintf "Operator `%s` should have been eliminated already" (Ast.print_op op)) + let rec translate_expr (e:A.expr) : ML T.expr = (match e.v with | Constant c -> T.Constant c @@ -321,9 +323,11 @@ and translate_out_expr (oe:out_expr) : ML T.output_expr = let output_types_attributes = { T.is_hoisted = false; + T.is_if_def = false; T.is_exported = false; T.should_inline = false; - T.comments = [] } + T.comments = [] +} (* * An output expression type parameter is translated to @@ -1098,13 +1102,13 @@ let rec free_vars_expr (genv:global_env) | Record _ fields -> List.fold_left (fun out (_, e) -> free_vars_expr genv env out e) out fields -let with_attrs (d:T.decl') (h:bool) (e:bool) (i:bool) (c:list string) +let with_attrs (d:T.decl') (h:bool) (ifdef:bool) (e:bool) (i:bool) (c:list string) : T.decl - = d, T.({ is_hoisted = h; is_exported = e; should_inline = i; comments = c } ) + = d, T.({ is_hoisted = h; is_if_def = ifdef; is_exported = e; should_inline = i; comments = c } ) let with_comments (d:T.decl') (e:bool) (c:list string) : T.decl - = d, T.({ is_hoisted = false; is_exported = e; should_inline = false; comments = c } ) + = d, T.({ is_hoisted = false; is_if_def=false; is_exported = e; should_inline = false; comments = c } ) let rec hoist_typ (fn:string) @@ -1138,7 +1142,7 @@ let rec hoist_typ in let d = Definition def in let t = T_refine t1 (None, app) in - ds@[with_attrs d true false true []], //hoisted, not exported, inlineable + ds@[with_attrs d true false false true []], //hoisted, not exported, inlineable t | T_refine t1 (None, e) -> @@ -1227,7 +1231,7 @@ let hoist_one_type_definition (should_inline:bool) decl_is_enum = false } in let td = Type_decl td in - with_attrs td true false should_inline [comment], //hoisted, not exported, should_inline + with_attrs td true false false should_inline [comment], //hoisted, not exported, should_inline tdef let hoist_field (genv:global_env) (env:env_t) (tdn:T.typedef_name) (f:T.field) @@ -1403,7 +1407,11 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = let params, ds = List.fold_left (fun (params, ds) (t, i, _) -> let t, ds_t = translate_typ t in params@[i, t],ds@ds_t) ([], ds) params in - [with_comments (T.Extern_fn f ret params) false []] + ds @ [with_comments (T.Extern_fn f ret params) false []] + + | CompileTimeFlag i -> + let t, ds_t = translate_typ tbool in + ds_t @ [with_attrs (T.Assumption (i, t)) false true false false []] noeq type translate_env = { diff --git a/src/3d/TypeSizes.fst b/src/3d/TypeSizes.fst index d5f21a552..0f2703622 100644 --- a/src/3d/TypeSizes.fst +++ b/src/3d/TypeSizes.fst @@ -392,7 +392,8 @@ let decl_size_with_alignment (env:env_t) (d:decl) d | OutputType _ | ExternType _ - | ExternFn _ _ _ -> d + | ExternFn _ _ _ + | CompileTimeFlag _ -> d let size_of_decls (genv:B.global_env) (senv:size_env) (ds:list decl) = let env = diff --git a/src/3d/ocaml/lexer.mll b/src/3d/ocaml/lexer.mll index cd64e7aab..265c1b005 100644 --- a/src/3d/ocaml/lexer.mll +++ b/src/3d/ocaml/lexer.mll @@ -107,6 +107,9 @@ rule token = | line_comment as c { Ast.comments_buffer.push (locate_pos lexbuf c); token lexbuf } | "/*++" { block_comment ("", Lexing.lexeme_start_p lexbuf) lexbuf } | "/*" { multi_line_comment lexbuf } + | "#if" { locate lexbuf HASH_IF } + | "#else" { locate lexbuf HASH_ELSE } + | "#endif" { locate lexbuf HASH_ENDIF } | "(" { locate lexbuf LPAREN } | ")" { locate lexbuf RPAREN } | "<<" { locate lexbuf SHIFT_LEFT } diff --git a/src/3d/ocaml/parser.mly b/src/3d/ocaml/parser.mly index e87693652..5de2a4636 100644 --- a/src/3d/ocaml/parser.mly +++ b/src/3d/ocaml/parser.mly @@ -59,6 +59,7 @@ %token REM SHIFT_LEFT SHIFT_RIGHT BITWISE_AND BITWISE_OR BITWISE_XOR BITWISE_NOT AS %token MODULE EXPORT OUTPUT UNION EXTERN %token ENTRYPOINT REFINING ALIGNED +%token HASH_IF HASH_ELSE HASH_ENDIF (* LBRACE_ONERROR CHECK *) %start prog %start expr_top @@ -108,6 +109,10 @@ else_opt: | { None } | ELSE LBRACE e=expr RBRACE { Some e } +hash_else_opt: + | { None } + | HASH_ELSE e=expr { Some e } + atomic_expr: | i=qident { Identifier i } | THIS { This } @@ -178,6 +183,16 @@ expr_no_range: in App(IfThenElse, [e;e1;e2]) } + | HASH_IF e=atomic_or_paren_expr e1=expr e2=hash_else_opt HASH_ENDIF + { + let e2 = + match e2 with + | None -> with_range (Constant (Bool true)) $startpos + | Some e2 -> e2 + in + App(HashIfThenElse, [e;e1;e2]) + } + | i=IDENT LPAREN es=arguments RPAREN { App(Ext i.v.name, es) From 40431f513791f1857426306cd226a9da7993a4f5 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 12 Aug 2022 23:21:11 +0000 Subject: [PATCH 02/12] boolean expressions in #if --- src/3d/tests/CompileTimeIf.3d | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 src/3d/tests/CompileTimeIf.3d diff --git a/src/3d/tests/CompileTimeIf.3d b/src/3d/tests/CompileTimeIf.3d new file mode 100644 index 000000000..82120563a --- /dev/null +++ b/src/3d/tests/CompileTimeIf.3d @@ -0,0 +1,12 @@ +entrypoint +typedef struct _PointConditional { + UINT32 x; + UINT32 y + { + #if (ABOVE_DIAGONAL && SOMETHING_ELSE) + x <= y + #else + y <= x + #endif + }; +} PointConditional; From 4ae7cb9219f3619160e5879a3d77f662b574e347 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 16 Aug 2022 05:54:26 +0000 Subject: [PATCH 03/12] code complete on anonymous structs and case types, arbitrarily nested --- src/3d/Ast.fst | 61 +++-- src/3d/Binding.fst | 346 +++++++++++++++++++---------- src/3d/BitFields.fst | 117 ++++++---- src/3d/Deps.fst | 32 +-- src/3d/Desugar.fst | 16 +- src/3d/InlineSingletonRecords.fst | 47 ++-- src/3d/Simplify.fst | 32 ++- src/3d/TranslateForInterpreter.fst | 262 +++++++++++----------- src/3d/TypeSizes.fst | 116 ++++++---- src/3d/ocaml/parser.mly | 3 +- 10 files changed, 636 insertions(+), 396 deletions(-) diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst index 8af115880..1d2c0d2c4 100644 --- a/src/3d/Ast.fst +++ b/src/3d/Ast.fst @@ -438,7 +438,7 @@ type field_array_t = [@@ PpxDerivingYoJson ] noeq -type struct_field = { +type atomic_field' = { field_dependence:bool; //computed; whether or not the rest of the struct depends on this field field_ident:ident; //name of the field field_type:typ; //type of the field @@ -448,17 +448,23 @@ type struct_field = { field_action:option (action & bool); //boo indicates if the action depends on the field value } -[@@ PpxDerivingYoJson ] -let field = with_meta_t struct_field +and atomic_field = with_meta_t atomic_field' -[@@ PpxDerivingYoJson ] -noeq -type case = +and field' = + | AtomicField of atomic_field + | RecordField of record + | SwitchCaseField of switch_case + +and field = with_meta_t field' + +and record = list field + +and case = | Case : expr -> field -> case | DefaultCase : field -> case -[@@ PpxDerivingYoJson ] -let switch_case = expr & list case +and switch_case = expr & list case + [@@ PpxDerivingYoJson ] type attribute = @@ -521,7 +527,7 @@ type decl' = | Define: ident -> option typ -> constant -> decl' | TypeAbbrev: typ -> ident -> decl' | Enum: typ -> ident -> list enum_case -> decl' - | Record: names:typedef_names -> params:list param -> where:option expr -> fields:list field -> decl' + | Record: names:typedef_names -> params:list param -> where:option expr -> fields:record -> decl' | CaseType: typedef_names -> list param -> switch_case -> decl' | OutputType : out_typ -> decl' @@ -704,7 +710,12 @@ let subst_field_array (s:subst) (f:field_array_t) : ML field_array_t = | FieldScalar -> f | FieldArrayQualified (e, q) -> FieldArrayQualified (subst_expr s e, q) | FieldString sz -> FieldString (map_opt (subst_expr s) sz) -let subst_field (s:subst) (f:field) : ML field = +let rec subst_field (s:subst) (ff:field) : ML field = + match ff.v with + | AtomicField f -> {ff with v = AtomicField (subst_atomic_field s f)} + | RecordField f -> {ff with v = RecordField (subst_record s f)} + | SwitchCaseField f -> {ff with v = SwitchCaseField (subst_switch_case s f)} +and subst_atomic_field (s:subst) (f:atomic_field) : ML atomic_field = let sf = f.v in let a = match sf.field_action with @@ -718,12 +729,14 @@ let subst_field (s:subst) (f:field) : ML field = field_constraint = map_opt (subst_expr s) sf.field_constraint; field_action = a } in - { f with v = sf } -let subst_case (s:subst) (c:case) : ML case = + { f with v = sf } +and subst_record (s:subst) (f:record) : ML record + = List.map (subst_field s) f +and subst_case (s:subst) (c:case) : ML case = match c with | Case e f -> Case (subst_expr s e) (subst_field s f) | DefaultCase f -> DefaultCase (subst_field s f) -let subst_switch_case (s:subst) (sc:switch_case) : ML switch_case = +and subst_switch_case (s:subst) (sc:switch_case) : ML switch_case = subst_expr s (fst sc), List.map (subst_case s) (snd sc) let subst_params (s:subst) (p:list param) : ML (list param) = List.map (fun (t, i, q) -> subst_typ s t, i, q) p @@ -912,7 +925,17 @@ let print_bitfield (bf:option field_bitwidth_t) = (print_typ a.bitfield_type) a.bitfield_from a.bitfield_to -let print_field (f:field) : ML string = +let rec print_field (f:field) : ML string = + match f.v with + | AtomicField f -> print_atomic_field f + | RecordField f -> print_record f + | SwitchCaseField f -> print_switch_case f + +and print_record (f:record) : ML string = + List.map print_field f |> + String.concat ";\n" + +and print_atomic_field (f:atomic_field) : ML string = let print_array eq : Tot string = match eq with | FieldScalar -> "" @@ -935,7 +958,7 @@ let print_field (f:field) : ML string = (print_array sf.field_array_opt) (print_opt sf.field_constraint (fun e -> Printf.sprintf "{%s}" (print_expr e))) -let print_switch_case (s:switch_case) : ML string = +and print_switch_case (s:switch_case) : ML string = let head, cases = s in let print_case (c:case) : ML string = match c with @@ -1025,3 +1048,11 @@ let weak_kind_glb (w1 w2: weak_kind) : Tot weak_kind = if w1 = w2 then w1 else WeakKindWeak + + +let field_tag_equal (f0 f1:field) = + match f0.v, f1.v with + | AtomicField _, AtomicField _ + | RecordField _, RecordField _ + | SwitchCaseField _, SwitchCaseField _ -> true + | _ -> false diff --git a/src/3d/Binding.fst b/src/3d/Binding.fst index 7935fe7c1..f364f9c88 100644 --- a/src/3d/Binding.fst +++ b/src/3d/Binding.fst @@ -51,6 +51,15 @@ let mk_env (g:global_env) = locals = H.create 10; globals = g } +let copy_env (e:env) = + let locals = H.create 10 in + H.iter (fun k v -> H.insert locals k v) e.locals; + { + this = e.this; + globals = e.globals; + locals = locals + } + let env_of_global_env : global_env -> env = let locals = H.create 1 in @@ -908,7 +917,7 @@ and check_typ_param (env:env) (p:typ_param) : ML (typ_param & typ) = #pop-options #push-options "--z3rlimit_factor 3" -let rec check_field_action (env:env) (f:field) (a:action) +let rec check_field_action (env:env) (f:atomic_field) (a:action) : ML (action & typ) = let check_atomic_action env (r:range) (a:atomic_action) : ML (atomic_action & typ) @@ -1046,8 +1055,8 @@ let rec check_field_action (env:env) (f:field) (a:action) #pop-options #push-options "--z3rlimit_factor 4" -let check_field (env:env) (extend_scope: bool) (f:field) - : ML field +let check_atomic_field (env:env) (extend_scope: bool) (f:atomic_field) + : ML atomic_field = let sf = f.v in let sf_field_type = check_typ false env sf.field_type in let check_annot (e: expr) : ML expr = @@ -1096,23 +1105,65 @@ let check_field (env:env) (extend_scope: bool) (f:field) let is_strong_prefix_field_array (a: field_array_t) : Tot bool = not (FieldScalar? a) -let weak_kind_of_field (env: env) (f: field) : ML weak_kind = +let weak_kind_of_atomic_field (env: env) (f: atomic_field) : ML weak_kind = if is_strong_prefix_field_array f.v.field_array_opt then WeakKindStrongPrefix else match typ_weak_kind env f.v.field_type with | Some e -> e | None -> failwith (Printf.sprintf "cannot find the weak kind of field %s : %s" (print_ident f.v.field_ident) (print_typ f.v.field_type)) -let weak_kind_of_case (env: env) (c: case) : ML weak_kind = +let weak_kind_of_list (wa:'a -> ML weak_kind) (xs:list 'a) : ML weak_kind = + let k = + List.fold_left + (fun out f -> + let fk = wa f in + match out with + | None -> Some fk + | Some o -> Some (weak_kind_glb o fk)) + None + xs + in + match k with + | None -> WeakKindWeak + | Some k -> k + +let rec weak_kind_of_field (env: env) (f: field) : ML weak_kind = + match f.v with + | AtomicField f -> weak_kind_of_atomic_field env f + | RecordField f -> weak_kind_of_record env f + | SwitchCaseField f -> weak_kind_of_switch_case env f + +and weak_kind_of_record env (fs:record) : ML weak_kind = + match fs with + | [] -> WeakKindStrongPrefix + | [a] -> weak_kind_of_field env a + | a :: q -> + let wk = weak_kind_of_field env a in + if wk <> WeakKindStrongPrefix + then failwith + (Printf.sprintf "weak_kind_of_fields: \ + field %s should be of strong kind \ + instead of %s" + (print_field a) + (print_weak_kind wk)) + else weak_kind_of_record env q + +and weak_kind_of_switch_case env (s:switch_case) : ML weak_kind = + let _, cases = s in + weak_kind_of_list (weak_kind_of_case env) cases + +and weak_kind_of_case (env: env) (c: case) : ML weak_kind = match c with | DefaultCase f | Case _ f -> weak_kind_of_field env f #pop-options +let check_field_t = env -> field -> ML field + #push-options "--z3rlimit_factor 8" -let check_switch (env:env) (s:switch_case) - : ML (switch_case & decl_attributes) +let check_switch (check_field:check_field_t) (env:env) (s:switch_case) + : ML switch_case = let head, cases = s in let head, scrutinee_t = check_expr env head in let fail_non_equality_type (#a:Type) () : ML (option a) = @@ -1139,7 +1190,7 @@ let check_switch (env:env) (s:switch_case) let check_case (c:case{Case? c}) : ML case = let Case pat f = c in let pat, pat_t = check_expr env pat in - let f = check_field env false f in + let f = check_field env f in let pat = //check type of patterns match tags_t_opt with | None -> @@ -1181,7 +1232,7 @@ let check_switch (env:env) (s:switch_case) in let check_default_case (c:case{DefaultCase? c}) : ML case = let DefaultCase f = c in - let f = check_field env false f in + let f = check_field env f in DefaultCase f in let cases = @@ -1194,28 +1245,78 @@ let check_switch (env:env) (s:switch_case) | DefaultCase f -> if default_ok then false else raise (error "default is only allowed in the last case" - f.v.field_ident.range)) + f.range)) cases true in - let wk = match cases with - | [] -> failwith "no cases in switch" - | c :: cases' -> - List.fold_left - (fun wk case -> weak_kind_glb wk (weak_kind_of_case env case)) - (weak_kind_of_case env c) - cases' - in - let attrs = { - may_fail = false; - integral = None; - has_reader = false; - parser_weak_kind = wk; - parser_kind_nz = None - } in - (head, cases), attrs + (head, cases) #pop-options +let rec check_record (check_field:check_field_t) (env:env) (fs:record) + : ML record + = let env = copy_env env in //locals of a record do not escape the record + + (* Elaborate and check each field in order; + Checking each field extends the local environment with the name of that field *) + let fields = + List.map + (fun f -> + match f.v with + | AtomicField af -> + let af = check_atomic_field env true af in + { f with v = AtomicField af } + + | RecordField fs -> + let fs = check_record check_field env fs in + { f with v = RecordField fs } + + | SwitchCaseField swc -> + let swc = check_switch check_field env swc in + { f with v = SwitchCaseField swc }) + fs + in + + (* Infer which of the fields are dependent by seeing which of them are used in refinements *) + let nfields = List.length fields in + let fields = fields |> List.mapi (fun i f -> + match f.v with + | RecordField _ + | SwitchCaseField _ -> f + | AtomicField af -> + let sf = af.v in + let used = is_used env sf.field_ident in + let last_field = i = (nfields - 1) in + let dependent = used || (Some? sf.field_constraint && not last_field) in + let af = + with_range_and_comments + ({ sf with field_dependence = dependent }) + af.range + af.comments + in + let has_reader = typ_has_reader env af.v.field_type in + let is_enum = is_enum env af.v.field_type in + if af.v.field_dependence + && not has_reader + && not is_enum //if it's an enum, it can be inlined later to allow dependence + then error "The type of this field does not have a reader, \ + either because its values are too large \ + or because reading it may incur a double fetch; \ + subsequent fields cannot depend on it" af.range + else { f with v = AtomicField af }) + in + fields + +let rec check_field (env:env) (f:field) + : ML field + = match f.v with + | AtomicField af -> + { f with v = AtomicField (check_atomic_field env false af) } + + | RecordField fs -> + { f with v = RecordField (check_record check_field env fs) } + + | SwitchCaseField swc -> + { f with v = SwitchCaseField (check_switch check_field env swc) } (** Computes a layout for bit fields, decorating each field with a bitfield index @@ -1226,7 +1327,11 @@ let check_switch (env:env) (s:switch_case) *) let elaborate_bit_fields env (fields:list field) : ML (list field) - = let new_bit_field index sf bw r : ML (field & option (typ & int & int)) = + = let bf_index : ref int = ST.alloc 0 in + let get_bf_index () = !bf_index in + let next_bf_index () = bf_index := !bf_index + 1 in + let new_bit_field (sf:atomic_field') bw r : ML (atomic_field & option (typ & int & int)) = + let index = get_bf_index () in let size = size_of_integral_typ env sf.field_type r in let bit_size = 8 * size in let remaining_size = bit_size - bw.v in @@ -1243,63 +1348,103 @@ let elaborate_bit_fields env (fields:list field) with_range sf r, Some (sf.field_type, to, remaining_size) in - let rec aux bf_index open_bit_field fields + let rec aux open_bit_field fields : ML (list field) = match fields with | [] -> [] | hd::tl -> - let sf = hd.v in - match sf.field_bitwidth, open_bit_field with - | None, None -> - hd :: aux bf_index open_bit_field tl - - | None, Some _ -> //end the bit field - hd :: aux (bf_index + 1) None tl - - | Some (Inr _), _ -> - failwith "Bitfield is already elaborated" - - | Some (Inl bw), None -> - let hd, open_bit_field = new_bit_field bf_index sf bw hd.range in - let tl = aux bf_index open_bit_field tl in - hd :: tl - - | Some (Inl bw), Some (bit_field_typ, pos, remaining_size) -> - Options.debug_print_string - (Printf.sprintf - "Field type = %s; bit_field_type = %s\n" - (print_typ sf.field_type) - (print_typ bit_field_typ)); - - if remaining_size < bw.v //not enough space in this bit field, start a new one - then let next_index = bf_index + 1 in - let hd, open_bit_field = new_bit_field next_index sf bw hd.range in - let tl = aux next_index open_bit_field tl in - hd :: tl - else //extend this bit field - begin + begin + match hd.v with + | RecordField fs -> + next_bf_index(); + let fs = aux None fs in + let hd = { hd with v = RecordField fs } in + next_bf_index(); + hd :: aux None tl + + | SwitchCaseField (e, cases) -> + next_bf_index(); + let cases = + List.map + (function + | Case p f -> + let fs = aux None [f] in + begin + match fs with + | [f] -> Case p f + | _ -> Case p (with_range_and_comments (RecordField fs) f.range f.comments) + end + + | DefaultCase f -> + let fs = aux None [f] in + begin + match fs with + | [f] -> DefaultCase f + | _ -> DefaultCase (with_range_and_comments (RecordField fs) f.range f.comments) + end) + cases + in + next_bf_index(); + let hd = { hd with v = SwitchCaseField (e, cases) } in + hd :: aux None tl + + | AtomicField af -> + let sf = af.v in + match sf.field_bitwidth, open_bit_field with + | None, None -> + hd :: aux open_bit_field tl + + | None, Some _ -> //end the bit field + next_bf_index(); + hd :: aux None tl + + | Some (Inr _), _ -> + failwith "Bitfield is already elaborated" + + | Some (Inl bw), None -> + let af, open_bit_field = new_bit_field sf bw hd.range in + let tl = aux open_bit_field tl in + { hd with v = AtomicField af } :: tl + + | Some (Inl bw), Some (bit_field_typ, pos, remaining_size) -> + Options.debug_print_string + (Printf.sprintf + "Field type = %s; bit_field_type = %s\n" + (print_typ sf.field_type) + (print_typ bit_field_typ)); + + if remaining_size < bw.v //not enough space in this bit field, start a new one + then let _ = next_bf_index () in + let af, open_bit_field = new_bit_field sf bw hd.range in + let tl = aux open_bit_field tl in + { hd with v = AtomicField af } :: tl + else //extend this bit field + begin if not (eq_typ env sf.field_type bit_field_typ) then raise (error "Packing fields of different types into the same bit field is not yet supported" hd.range); let remaining_size = remaining_size - bw.v in let from = pos in let to = pos + bw.v in + let index = get_bf_index() in let bf_attr = { bitfield_width = bw.v; - bitfield_identifier = bf_index; + bitfield_identifier = index; bitfield_type = bit_field_typ; bitfield_from = from; bitfield_to = to } in let sf = { sf with field_bitwidth = Some (Inr (with_range bf_attr bw.range)) } in - let hd = { hd with v = sf } in + let af = { af with v = sf } in + let hd = { hd with v = AtomicField af } in let open_bit_field = Some (bit_field_typ, to, remaining_size) in - let tl = aux bf_index open_bit_field tl in + let tl = aux open_bit_field tl in hd :: tl end + end in - aux 0 None fields + aux None fields let allowed_base_types_as_output_types = [ @@ -1357,30 +1502,15 @@ let check_params (env:env) (ps:list param) : ML unit = else ignore (check_typ true env t); add_local env p t) -let rec weak_kind_of_fields (e: env) (l: list field) : ML weak_kind = - match l with - | [] -> WeakKindStrongPrefix - | [a] -> weak_kind_of_field e a - | a :: q -> - let wk = weak_kind_of_field e a in - if wk <> WeakKindStrongPrefix - then failwith - (Printf.sprintf "weak_kind_of_fields: \ - field %s : %s should be of strong kind \ - instead of %s" - (print_ident a.v.field_ident) - (print_typ a.v.field_type) - (print_weak_kind wk)) - else weak_kind_of_fields e q - -let elaborate_record (e:global_env) - (tdnames:Ast.typedef_names) - (params:list param) - (where:option expr) - (fields:list field) - (range:range) - (comments:comments) - (is_exported:bool) + +let elaborate_record_decl (e:global_env) + (tdnames:Ast.typedef_names) + (params:list param) + (where:option expr) + (fields:list field) + (range:range) + (comments:comments) + (is_exported:bool) : ML decl = let env = { mk_env e with this=Some tdnames.typedef_name } in @@ -1410,37 +1540,13 @@ let elaborate_record (e:global_env) field_action = None } in - w, [with_range field e.range] + let af = with_range (AtomicField (with_range field e.range)) e.range in + w, [af] in (* Elaborate and check each field in order; Checking each field extends the local environment with the name of that field *) - let fields = fields |> List.map (check_field env true) in - - (* Infer which of the fields are dependent by seeing which of them are used in refinements *) - let nfields = List.length fields in - let fields = fields |> List.mapi (fun i f -> - let sf = f.v in - let used = is_used env sf.field_ident in - let last_field = i = (nfields - 1) in - let dependent = used || (Some? sf.field_constraint && not last_field) in - let f = - with_range_and_comments - ({ sf with field_dependence = dependent }) - f.range - f.comments - in - let has_reader = typ_has_reader env f.v.field_type in - let is_enum = is_enum env f.v.field_type in - if f.v.field_dependence - && not has_reader - && not is_enum //if it's an enum, it can be inlined later to allow dependence - then error "The type of this field does not have a reader, \ - either because its values are too large \ - or because reading it may incur a double fetch; \ - subsequent fields cannot depend on it" f.range - else f) - in + let fields = check_record check_field env fields in let fields = maybe_unit_field@fields in @@ -1452,7 +1558,7 @@ let elaborate_record (e:global_env) may_fail = false; //only its fields may fail; not the struct itself integral = None; has_reader = false; - parser_weak_kind = weak_kind_of_fields env fields; + parser_weak_kind = weak_kind_of_record env fields; parser_kind_nz = None } in @@ -1541,12 +1647,20 @@ let bind_decl (e:global_env) (d:decl) : ML decl = d | Record tdnames params where fields -> - elaborate_record e tdnames params where fields d.d_decl.range d.d_decl.comments d.d_exported + elaborate_record_decl e tdnames params where fields d.d_decl.range d.d_decl.comments d.d_exported | CaseType tdnames params switch -> let env = { mk_env e with this=Some tdnames.typedef_name } in check_params env params; - let switch, attrs = check_switch env switch in + let switch = check_switch check_field env switch in + let wk = weak_kind_of_switch_case env switch in + let attrs = { + may_fail = false; + integral = None; + has_reader = false; + parser_weak_kind = wk; + parser_kind_nz = None + } in let d = mk_decl (CaseType tdnames params switch) d.d_decl.range d.d_decl.comments d.d_exported in add_global e tdnames.typedef_name d (Inl attrs); d diff --git a/src/3d/BitFields.fst b/src/3d/BitFields.fst index 7ea3c2056..38edd2f11 100644 --- a/src/3d/BitFields.fst +++ b/src/3d/BitFields.fst @@ -28,34 +28,43 @@ module H = Hashtable *) -let bitfield_group = int & typ & list field +let bitfield_group = int & typ & list atomic_field let grouped_fields = either field bitfield_group -let group_bit_fields (fields: list field) +let group_bit_fields (rewrite_composite_field: field -> ML field) + (fields: list field) : ML (list grouped_fields) = List.fold_right (fun field out -> - match field.v.field_bitwidth with - | None -> - Inl field :: out - - | Some (Inl _) -> - failwith "Bit fields should have been elaborated already" - - | Some (Inr bf) -> - match out with - | Inr (index, typ, fields)::tl -> - if index = bf.v.bitfield_identifier - then Inr(index, typ, field::fields) :: tl //extend this bitfield group - else Inr(bf.v.bitfield_identifier, bf.v.bitfield_type, [field]) :: out //new bitfield group - - | _ -> Inr (bf.v.bitfield_identifier, bf.v.bitfield_type, [field]) :: out //new bitfield group + match field.v with + | RecordField _ + | SwitchCaseField _ -> + Inl (rewrite_composite_field field) :: out + + | AtomicField af -> + match af.v.field_bitwidth with + | None -> + Inl field :: out + + | Some (Inl _) -> + failwith "Bit fields should have been elaborated already" + + | Some (Inr bf) -> + match out with + | Inr (index, typ, atomic_fields)::tl -> + if index = bf.v.bitfield_identifier + then Inr(index, typ, af :: atomic_fields) :: tl //extend this bitfield group + else Inr(bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group + + | _ -> Inr (bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group ) fields [] +let subst' = list (ident & expr) + let coalesce_grouped_bit_field env (f:bitfield_group) - : ML (field & list (ident & expr)) + : ML (field & subst') = let id, typ, fields = f in let size = B.size_of_integral_typ env typ typ.range in let bitsize = 8 * size in @@ -114,45 +123,61 @@ let coalesce_grouped_bit_field env (f:bitfield_group) field_bitwidth = None; field_action = field_action; } in - with_dummy_range struct_field, + let af = with_dummy_range struct_field in + with_dummy_range (AtomicField af), subst - -let coalesce_fields (env:B.global_env) (fields:list field) - : ML (list field & list (ident & expr)) - = let fs = group_bit_fields fields in - let fs, subst = - List.fold_right - (fun f (fields, subst) -> - match f with - | Inl f -> (f::fields, subst) - | Inr gf -> - let f, subst' = coalesce_grouped_bit_field (B.mk_env env) gf in - f::fields, subst'@subst) - fs - ([], []) - in - fs, - subst - + +let rec rewrite_field (env:B.global_env) (f:field) + : ML (f':field {field_tag_equal f f'}) + = match f.v with + | AtomicField _ -> f + + | RecordField fs -> + let gfs = group_bit_fields (rewrite_field env) fs in + let fs, subst = + List.fold_right + (fun f (fields, subst) -> + match f with + | Inl f -> (f::fields, subst) + | Inr gf -> + let f, subst' = coalesce_grouped_bit_field (B.mk_env env) gf in + f::fields, subst'@subst) + gfs + ([], []) + in + let fs = List.map (subst_field (mk_subst subst)) fs in + { f with v = RecordField fs } + + | SwitchCaseField (e, cases) -> + let cases = + List.map + (function + | Case p f -> + Case p (rewrite_field env f) + + | DefaultCase f -> + DefaultCase (rewrite_field env f)) + cases + in + { f with v = SwitchCaseField (e, cases) } + + let eliminate_one_decl (env:B.global_env) (d:decl) : ML decl = match d.d_decl.v with | Record names params where fields -> - let fields, subst = coalesce_fields env fields in + let { v = RecordField fields } = rewrite_field env (with_dummy_range (RecordField fields)) in List.iter (fun f -> Options.debug_print_string (Printf.sprintf "Bitfields: Field %s has comments <%s>\n" - (print_ident f.v.field_ident) + (print_field f) (String.concat "\n" f.comments))) fields; - List.iter (fun (i, e) -> - Options.debug_print_string (Printf.sprintf "subst(%s -> %s)\n" (ident_to_string i) (print_expr e))) - subst; - let fields = List.map (subst_field (mk_subst subst)) fields in let fields = match fields with - | [f] -> //just one field, it need no longer be dependent - let sf = { f.v with field_dependence = false } in - [{ f with v = sf }] + | [{v=AtomicField af; range; comments}] -> //just one field, it need no longer be dependent + let af' = { af.v with field_dependence = false } in + let af' = { af with v = af' } in + [{v=AtomicField af; range; comments}] | _ -> fields in decl_with_v d (Record names params where fields) diff --git a/src/3d/Deps.fst b/src/3d/Deps.fst index 748096944..74a97b602 100644 --- a/src/3d/Deps.fst +++ b/src/3d/Deps.fst @@ -146,19 +146,25 @@ let scan_deps (fn:string) : ML scan_deps_t = | FieldArrayQualified (e, _) -> deps_of_expr e | FieldString eopt -> deps_of_opt deps_of_expr eopt in - let deps_of_struct_field (sf:struct_field) : ML (list string) = - (deps_of_typ sf.field_type)@ - (deps_of_field_array_t sf.field_array_opt)@ - (deps_of_opt deps_of_expr sf.field_constraint)@ - (deps_of_opt deps_of_field_bitwidth_t sf.field_bitwidth)@ - (deps_of_opt (fun (a, _) -> deps_of_action a) sf.field_action) in - - let deps_of_case (c:case) : ML (list string) = + let deps_of_atomic_field (af:atomic_field) : ML (list string) = + let af = af.v in + (deps_of_typ af.field_type)@ + (deps_of_field_array_t af.field_array_opt)@ + (deps_of_opt deps_of_expr af.field_constraint)@ + (deps_of_opt deps_of_field_bitwidth_t af.field_bitwidth)@ + (deps_of_opt (fun (a, _) -> deps_of_action a) af.field_action) in + + let rec deps_of_field (f:field) : ML (list string) = + match f.v with + | AtomicField af -> deps_of_atomic_field af + | RecordField fs -> List.collect deps_of_field fs + | SwitchCaseField swc -> deps_of_switch_case swc + and deps_of_case (c:case) : ML (list string) = match c with - | Case e f -> (deps_of_expr e)@(deps_of_struct_field f.v) - | DefaultCase f -> deps_of_struct_field f.v in - - let deps_of_switch_case (sc:switch_case) : ML (list string) = + | Case e f -> (deps_of_expr e)@(deps_of_field f) + | DefaultCase f -> deps_of_field f + + and deps_of_switch_case (sc:switch_case) : ML (list string) = let e, l = sc in (deps_of_expr e)@(List.collect deps_of_case l) in @@ -179,7 +185,7 @@ let scan_deps (fn:string) : ML scan_deps_t = | Record _ params wopt flds -> (deps_of_params params)@ (deps_of_opt deps_of_expr wopt)@ - (List.collect (fun f -> deps_of_struct_field f.v) flds) + (List.collect deps_of_field flds) | CaseType _ params sc -> (deps_of_params params)@ (deps_of_switch_case sc) diff --git a/src/3d/Desugar.fst b/src/3d/Desugar.fst index f94316937..a091ecbda 100644 --- a/src/3d/Desugar.fst +++ b/src/3d/Desugar.fst @@ -337,8 +337,14 @@ let resolve_field_array_t (env:qenv) (farr:field_array_t) : ML field_array_t = | FieldString None -> farr | FieldString (Some e) -> FieldString (Some (resolve_expr env e)) -let resolve_field (env:qenv) (f:field) : ML (field & qenv) = - let resolve_struct_field (env:qenv) (sf:struct_field) : ML struct_field = +let rec resolve_field (env:qenv) (ff:field) : ML (field & qenv) = + match ff.v with + | AtomicField f -> let f, e = resolve_atomic_field env f in {ff with v = AtomicField f}, e + | RecordField f -> let fs, _ = resolve_fields env f in {ff with v = RecordField fs}, env //record fields are not in scope outside the record + | SwitchCaseField f -> let f = resolve_switch_case env f in {ff with v = SwitchCaseField f}, env + +and resolve_atomic_field (env:qenv) (f:atomic_field) : ML (atomic_field & qenv) = + let resolve_atomic_field' (env:qenv) (sf:atomic_field') : ML atomic_field' = { sf with field_type = resolve_typ env sf.field_type; field_array_opt = resolve_field_array_t env sf.field_array_opt; @@ -347,14 +353,14 @@ let resolve_field (env:qenv) (f:field) : ML (field & qenv) = field_action = map_opt (fun (a, b) -> resolve_action env a, b) sf.field_action } in let env = push_name env f.v.field_ident.v.name in - { f with v = resolve_struct_field env f.v }, env + { f with v = resolve_atomic_field' env f.v }, env -let resolve_fields (env:qenv) (flds:list field) : ML (list field & qenv) = +and resolve_fields (env:qenv) (flds:list field) : ML (list field & qenv) = List.fold_left (fun (flds, env) f -> let f, env = resolve_field env f in flds@[f], env) ([], env) flds -let resolve_switch_case (env:qenv) (sc:switch_case) : ML switch_case = +and resolve_switch_case (env:qenv) (sc:switch_case) : ML switch_case = //case fields do not escape their scope let resolve_case (env:qenv) (c:case) : ML case = match c with | Case e f -> Case (resolve_expr env e) (fst (resolve_field env f)) diff --git a/src/3d/InlineSingletonRecords.fst b/src/3d/InlineSingletonRecords.fst index b8cc9fd5d..73ed2eb23 100644 --- a/src/3d/InlineSingletonRecords.fst +++ b/src/3d/InlineSingletonRecords.fst @@ -17,7 +17,7 @@ module InlineSingletonRecords open Ast open FStar.All module H = Hashtable -type singleton_record = list param & field +type singleton_record = list param & atomic_field let env = H.t ident' singleton_record (* @@ -36,8 +36,8 @@ let choose_one (a b:option 'a) : ML (option 'a) = | _, Some fc -> Some fc | _ -> None -let simplify_field (env:env) (f:field) - : ML field +let simplify_atomic_field (env:env) (f:atomic_field) + : ML atomic_field = let field = f.v in let field = match field.field_type.v with @@ -63,7 +63,7 @@ let simplify_field (env:env) (f:field) params args in let subst = (inlined_field.v.field_ident, with_dummy_range (Identifier field.field_ident)) :: subst in - let inlined_field = subst_field (mk_subst subst) inlined_field in + let inlined_field = subst_atomic_field (mk_subst subst) inlined_field in let error msg = let msg = Printf.sprintf "Other types depend on the value of this field, but this field cannot be read because %s" @@ -106,6 +106,25 @@ let simplify_field (env:env) (f:field) in { f with v = field } +let rec simplify_field (env:env) (f:field) + : ML field + = match f.v with + | AtomicField f -> { f with v = AtomicField (simplify_atomic_field env f) } + | RecordField fs -> { f with v = RecordField (List.map (simplify_field env) fs) } + | SwitchCaseField swc -> { f with v = SwitchCaseField (simplify_switch_case env swc) } + +and simplify_switch_case (env:env) (swc:switch_case) + : ML switch_case + = let e, cases = swc in + let cases = + List.map + (function Case p f -> Case p (simplify_field env f) + | DefaultCase f -> DefaultCase (simplify_field env f)) + cases + in + e, cases + + let simplify_decl (env:env) (d:decl) : ML decl = match d.d_decl.v with | ModuleAbbrev _ _ -> @@ -151,15 +170,15 @@ let simplify_decl (env:env) (d:decl) : ML decl = field_bitwidth = None; field_action = None } in - let field = with_dummy_range field in + let af = with_dummy_range field in Options.debug_print_string (Printf.sprintf "For Enum %s, inserting field = %s\n" i.v.name - (print_field field)); - H.insert env i.v ([], field); + (print_atomic_field af)); + H.insert env i.v ([], af); d - | Record tdnames params None [field] -> //singleton + | Record tdnames params None [{v = AtomicField field; range; comments}] -> //singleton begin match field.v with | { field_array_opt = FieldArrayQualified _ } @@ -167,21 +186,19 @@ let simplify_decl (env:env) (d:decl) : ML decl = | { field_bitwidth = Some _ } -> d | _ -> - let field = simplify_field env field in + let af = simplify_atomic_field env field in H.insert env tdnames.typedef_name.v (params, field); + let field = with_range_and_comments (AtomicField af) range comments in decl_with_v d (Record tdnames params None [field]) end - + | Record tdnames params wopt fields -> let fields = List.map (simplify_field env) fields in decl_with_v d (Record tdnames params wopt fields) | CaseType tdnames params switch -> - let hd, cases = switch in - let cases = List.map (function Case e f -> Case e (simplify_field env f) - | DefaultCase f -> DefaultCase (simplify_field env f)) - cases in - decl_with_v d (CaseType tdnames params (hd, cases)) + let switch = simplify_switch_case env switch in + decl_with_v d (CaseType tdnames params switch) | OutputType _ | ExternType _ diff --git a/src/3d/Simplify.fst b/src/3d/Simplify.fst index e2b1597d6..edaf7a075 100644 --- a/src/3d/Simplify.fst +++ b/src/3d/Simplify.fst @@ -112,8 +112,8 @@ let simplify_field_array (env:T.env_t) (f:field_array_t) : ML field_array_t = | FieldArrayQualified (e, b) -> FieldArrayQualified (simplify_expr env e, b) | FieldString sz -> FieldString (map_opt (simplify_expr env) sz) -let simplify_field (env:T.env_t) (f:field) - : ML field +let simplify_atomic_field (env:T.env_t) (f:atomic_field) + : ML atomic_field = let sf = f.v in let ft = simplify_typ env sf.field_type in let fa = simplify_field_array env sf.field_array_opt in @@ -129,6 +129,26 @@ let simplify_field (env:T.env_t) (f:field) field_action = fact } in { f with v = sf } +let rec simplify_field (env:T.env_t) (f:field) + : ML field + = match f.v with + | AtomicField af -> { f with v = AtomicField (simplify_atomic_field env af) } + | RecordField fs -> { f with v = RecordField (List.map (simplify_field env) fs) } + | SwitchCaseField swc -> { f with v = SwitchCaseField (simplify_switch_case env swc) } + +and simplify_switch_case (env:T.env_t) (c:switch_case) + : ML switch_case = + let (e, cases) = c in + let e = simplify_expr env e in + let cases = + List.map + (function Case e f -> Case (simplify_expr env e) (simplify_field env f) + | DefaultCase f -> DefaultCase (simplify_field env f)) + cases + in + e, cases + + let rec simplify_out_fields (env:T.env_t) (flds:list out_field) : ML (list out_field) = List.map (fun fld -> match fld with | Out_field_named id t n -> Out_field_named id (simplify_typ env t) n @@ -158,12 +178,8 @@ let simplify_decl (env:T.env_t) (d:decl) : ML decl = | CaseType tdnames params switch -> let params = List.map (fun (t, i, q) -> simplify_typ env t, i, q) params in - let hd, cases = switch in - let hd = simplify_expr env hd in - let cases = List.map (function Case e f -> Case (simplify_expr env e) (simplify_field env f) - | DefaultCase f -> DefaultCase (simplify_field env f)) - cases in - decl_with_v d (CaseType tdnames params (hd, cases)) + let switch = simplify_switch_case env switch in + decl_with_v d (CaseType tdnames params switch) | OutputType out_t -> decl_with_v d (OutputType ({out_t with out_typ_fields=simplify_out_fields env out_t.out_typ_fields})) diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index 6eb337a0d..cbbb16cea 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -240,6 +240,19 @@ let dep_pair_with_action_parser p1 (a:T.lam T.action) (p2:A.ident & T.parser) = t_id "none" (Parse_dep_pair_with_action p1 a (Some (fst p2), snd p2)) +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 + 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) + in + let t = T.T_if_else e then_.p_typ else_.p_typ in + mk_parser k t typename fieldname (T.Parse_if_else e p1 p2) + let translate_op : A.op -> ML T.op = let force_topt (o:option A.integer_type) : ML integer_type @@ -490,15 +503,7 @@ let rec parse_typ (env:global_env) | T.T_if_else e t1 t2 -> let p1 = parse_typ env typename fieldname t1 in let p2 = parse_typ env typename fieldname t2 in - let k, p1, p2 = - if parser_kind_eq p1.p_kind p2.p_kind - then p1.p_kind, p1, p2 - else let k = pk_glb p1.p_kind p2.p_kind in - k, - mk_parser k t1 typename (extend_fieldname "case_left") (Parse_weaken_right p1 p2.p_kind), - mk_parser k t2 typename (extend_fieldname "case_right") (Parse_weaken_left p2 p1.p_kind) - in - mk_parser k t typename fieldname (Parse_if_else e p1 p2) + ite_parser typename fieldname e p1 p2 | T.T_dep_pair t1 (x, t2) -> dep_pair_parser typename (parse_typ env typename (extend_fieldname "first") t1) @@ -856,7 +861,7 @@ let make_zero (r: range) (t: typ) : ML T.expr = (T.Constant (Int it 0), r) #push-options "--z3rlimit_factor 4" -let translate_field (f:A.field) : ML (T.struct_field & T.decls) = +let translate_atomic_field (f:A.atomic_field) : ML (T.struct_field & T.decls) = let sf = f.v in let t, ds1 = translate_typ sf.field_type in let t = @@ -917,54 +922,13 @@ let translate_field (f:A.field) : ML (T.struct_field & T.decls) = sf_typ=t}), ds1@ds2 #pop-options -let nondep_group = list T.field -let grouped_fields = list (either T.field nondep_group) -let print_grouped_fields (gfs:grouped_fields) : ML string = - Printf.sprintf "[%s]" - (let s = - List.Tot.map - (fun (f:either T.field nondep_group) -> - match f with - | Inl f -> ident_to_string f.T.sf_ident - | Inr l -> - Printf.sprintf "[%s]" - (let s = List.Tot.map (fun f -> ident_to_string f.T.sf_ident) l in - String.concat "; " s)) - gfs - in - String.concat "; " s) -let make_grouped_fields (fs:list T.field) : ML grouped_fields = - let open T in - let add_run (out, run) : grouped_fields = - match run with - | [] -> out - | _ -> Inr run :: out - in - let extend_run sf (run:nondep_group) : nondep_group = - sf::run - in - let group_non_dependent_fields - (sf:struct_field) - (out, run) - : grouped_fields & nondep_group - = match out, run with - | [], [] -> - //last field is always non-dependent - //even though its sf_dependence flag may be sets - //e.g., because it a field result from coalescing multiple bitfield - //which may themselves be dependent - //See BitFields0.3d for a test case - out, extend_run sf run - | _ -> - if sf.sf_dependence - then Inl sf::add_run (out, run), [] - else out, extend_run sf run - in - let gfs : grouped_fields = - add_run (List.fold_right group_non_dependent_fields fs ([], [])) - in - gfs - +noeq +type grouped_fields = + | Empty_grouped_field + | DependentField : hd:T.field -> tl:grouped_fields -> grouped_fields + | NonDependentField : hd:T.field -> tl:grouped_fields -> grouped_fields + | ITEGroup : e:T.expr -> then_:grouped_fields -> else_:grouped_fields -> grouped_fields + | GroupThen : struct:grouped_fields -> rest:grouped_fields -> grouped_fields let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields) : ML T.parser @@ -972,10 +936,10 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields let parse_typ (fieldname:A.ident) = parse_typ env typename Ast.(fieldname.v.name) in let rec aux (gfs:grouped_fields) : ML parser = match gfs with - | [] -> + | Empty_grouped_field -> failwith "Unexpected empty list of fields" - | Inl sf::gfs -> + | DependentField sf gfs -> //This a dependent pair, gfs cannot be empty let get_action = function | Inl a -> (Some sf.sf_ident, a) @@ -1017,46 +981,38 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields (sf.sf_ident, aux gfs) end - | [Inr gf] -> - let rec aux (gf:nondep_group) - : ML T.parser - = match gf with - | [] -> - failwith "Unexpected empty non-dep group" - | [sf] -> - parse_typ sf.sf_ident sf.sf_typ - | sf::sfs -> - pair_parser - sf.sf_ident - (parse_typ sf.sf_ident sf.sf_typ) - (aux sfs) - in - aux gf - - | Inr gf::gfs -> - List.fold_right - (fun (sf:struct_field) (p_tl:parser) -> - pair_parser - sf.sf_ident - (parse_typ sf.sf_ident sf.sf_typ) - p_tl) - gf - (aux gfs) + | NonDependentField sf rest -> ( + match rest with + | Empty_grouped_field -> + parse_typ sf.sf_ident sf.sf_typ + + | _ -> + pair_parser sf.sf_ident + (parse_typ sf.sf_ident sf.sf_typ) + (aux rest) + ) + + | ITEGroup e then_ else_ -> + let id = gen_ident None in + let then_ = aux then_ in + let else_ = aux else_ in + ite_parser typename id.v.name e then_ else_ + + | GroupThen gfs rest -> ( + match rest with + | Empty_grouped_field -> + aux gfs + + | _ -> + let id = gen_ident None in + pair_parser id + (aux gfs) + (aux rest) + ) + in aux gfs -let parse_fields (env:global_env) (tdn:T.typedef_name) (fs:list T.field) - : ML T.parser = - let open T in - let td_name, td_params = tdn.td_name, tdn.td_params in - let gfs = make_grouped_fields fs in - // FStar.IO.print_string - // (FStar.Printf.sprintf "parse_fields (tdn = %s), fields=[%s], grouped_fields=%s\n" - // tdn.td_name.v - // (List.map (fun x -> x.sf_ident.v) fs |> String.concat ", ") - // (print_grouped_fields gfs)); - let p = parse_grouped_fields env tdn.td_name gfs in - p let make_tdn (i:A.ident) = { @@ -1275,39 +1231,74 @@ let hoist_refinements (genv:global_env) (tdn:T.typedef_name) (fields:list T.fiel in decls, List.rev fields -let translate_switch_case_type (genv:global_env) (tdn:T.typedef_name) (sw:Ast.switch_case) - : ML (T.typ & list T.decl) = - let sc, cases = sw in - let sc = translate_expr sc in - let env = List.rev tdn.T.td_params in - let translate_one_case f : ML _ = - let sf, ds = translate_field f in - ds, sf - in - let rest, default_t, decls = - if List.length cases > 0 - then - let rest, last = List.splitAt (List.length cases - 1) cases in - match last with - | [DefaultCase f] -> - let decls, sf = translate_one_case f in - rest, sf.T.sf_typ, decls - | _ -> - cases, T.T_false, [] - else - cases, T.T_false, [] - in - List.fold_right - (fun case (t_else, decls) -> - match case with - | DefaultCase _ -> failwith "Impossible" - | Case e f -> - let decls', sf = translate_one_case f in - let guard = T.mk_expr (T.App T.Eq [sc; translate_expr e]) in - let t = T.T_if_else guard sf.T.sf_typ t_else in - t, decls@decls') - rest - (default_t, decls) +let type_of_grouped_fields (gfs:grouped_fields) : T.typ = admit() + +let rec field_as_grouped_fields (f:A.field) + : ML (grouped_fields & T.decls) + = match f.v with + | AtomicField af -> + let sf, ds = translate_atomic_field af in + NonDependentField sf Empty_grouped_field, ds + + | RecordField fs -> + List.fold_right + (fun f (gfs, ds_out) -> + match f.v with + | AtomicField af -> + let sf, ds = translate_atomic_field af in + if sf.sf_dependence + then DependentField sf gfs, ds@ds_out + else NonDependentField sf gfs, ds@ds_out + + | RecordField _ + | SwitchCaseField _ -> + let gf, ds = field_as_grouped_fields f in + GroupThen gf gfs, ds@ds_out) + fs + (Empty_grouped_field, []) + + | SwitchCaseField swc -> + let sc, cases = swc in + let sc = translate_expr sc in + let false_field = + NonDependentField + T.( { sf_typ = T.T_false; + sf_ident = gen_ident None; + sf_dependence = false } ) + Empty_grouped_field + in + let rest, default_group, decls = + if List.length cases > 0 + then + let rest, last = List.splitAt (List.length cases - 1) cases in + match last with + | [DefaultCase f] -> + let gfs, ds = field_as_grouped_fields f in + rest, gfs, ds + + | _ -> + cases, false_field, [] + else + cases, false_field, [] + in + List.fold_right + (fun case (else_group, decls') -> + match case with + | DefaultCase _ -> failwith "Impossible" + | Case p f -> + let gfs, decls = field_as_grouped_fields f in + let guard = T.mk_expr (T.App T.Eq [sc; translate_expr p]) in + ITEGroup guard gfs else_group, decls@decls') + rest + (default_group, decls) + +let parse_field (env:global_env) + (typename:A.ident) + (f:A.field) + : ML (T.parser & T.decls) + = let gfs, decls = field_as_grouped_fields f in + parse_grouped_fields env typename gfs, decls + let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = match d.d_decl.v with @@ -1361,10 +1352,7 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = | Record tdn params _ ast_fields -> let tdn, ds1 = translate_typedef_name tdn params in - let fields, ds2 = - let fields, ds2 = ast_fields |> List.map translate_field |> List.split in - fields, List.flatten ds2 in - let p = parse_fields env tdn fields in + let p, ds2 = parse_field env tdn.td_name (with_dummy_range (RecordField ast_fields)) in let open T in add_parser_kind_nz env tdn.td_name p.p_kind.pk_nz p.p_kind.pk_weak_kind; add_parser_kind_is_constant_size env tdn.td_name (parser_is_constant_size_without_actions env p); @@ -1382,11 +1370,13 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = | CaseType tdn0 params switch_case -> let tdn, ds1 = translate_typedef_name tdn0 params in - let t, ds2 = translate_switch_case_type env tdn switch_case in - let p = parse_typ env tdn0.typedef_name "" t in + let p, ds2 = parse_field env tdn.td_name (with_dummy_range (SwitchCaseField switch_case)) in + // let t, ds2 = translate_switch_case_type env tdn switch_case in + // let p = parse_typ env tdn0.typedef_name "" t in let open T in add_parser_kind_nz env tdn.td_name p.p_kind.pk_nz p.p_kind.pk_weak_kind; add_parser_kind_is_constant_size env tdn.td_name (parser_is_constant_size_without_actions env p); + let t = p.p_typ in let reader = maybe_add_reader env tdn t in let td = { decl_name = tdn; diff --git a/src/3d/TypeSizes.fst b/src/3d/TypeSizes.fst index 0f2703622..b20a642ac 100644 --- a/src/3d/TypeSizes.fst +++ b/src/3d/TypeSizes.fst @@ -158,7 +158,7 @@ let rec value_of_const_expr (env:env_t) (e:expr) end | _ -> None -let size_and_alignment_of_field (env:env_t) (f:field) +let size_and_alignment_of_atomic_field (env:env_t) (f:atomic_field) : ML (size & alignment) = let base_size, align = size_and_alignment_of_typ env f.v.field_type in let size = @@ -207,7 +207,7 @@ let gen_alignment_ident dummy_range #pop-options -let padding_field (env:env_t) (enclosing_struct:ident) (padding_msg:string) (n:int) +let padding_field (env:env_t) (diag_enclosing_type_name:ident (* for diagnostics only *)) (padding_msg:string) (n:int) : ML (list field) = if n <= 0 @@ -215,9 +215,10 @@ let padding_field (env:env_t) (enclosing_struct:ident) (padding_msg:string) (n:i else ( let field_name = gen_alignment_ident() in let n_expr = with_range (Constant (Int UInt32 n)) dummy_range in + let nm = ident_to_string diag_enclosing_type_name in FStar.IO.print_string (Printf.sprintf "Adding padding field in %s for %d bytes at %s\n" - (ident_to_string enclosing_struct) + nm n padding_msg); let sf = { @@ -229,16 +230,22 @@ let padding_field (env:env_t) (enclosing_struct:ident) (padding_msg:string) (n:i field_bitwidth=None; field_action=None } in - [with_dummy_range sf] + let af = with_dummy_range sf in + let f = with_dummy_range (AtomicField af) in + [f] ) let should_align (td:typedef_names) : bool = List.Tot.Base.mem Aligned td.typedef_attributes -let alignment_padding env (enclosing_name:typedef_names) (msg:string) (offset:size) (a:alignment) +let alignment_padding env (should_align:bool) + (diag_enclosing_type_name:ident (* for diagnostics only *)) + (msg:string) + (offset:size) + (a:alignment) : ML (int & list field) - = if not (should_align enclosing_name) + = if not should_align then 0, [] else ( let pad_size = @@ -256,7 +263,7 @@ let alignment_padding env (enclosing_name:typedef_names) (msg:string) (offset:si 0 in pad_size, - padding_field env enclosing_name.typedef_name msg pad_size + padding_field env diag_enclosing_type_name msg pad_size ) let sum_size (n : size) (m:size) @@ -269,29 +276,29 @@ let sum_size (n : size) (m:size) | WithVariableSuffix m -> WithVariableSuffix (n + m) | Variable -> WithVariableSuffix n -let decl_size_with_alignment (env:env_t) (d:decl) - : ML decl - = match d.d_decl.v with - | ModuleAbbrev _ _ -> d - | Define _ _ _ -> d +open FStar.List.Tot - | TypeAbbrev t i - | Enum t i _ -> - let s, a = size_and_alignment_of_typ env t in - extend_with_size_of_ident env i s a; - d +let rec size_and_alignment_of_field (env:env_t) + (should_align:bool) + (diag_enclosing_type_name:ident) + (f:field) + : ML (res:(field & size & alignment) { let f', _, _ = res in field_tag_equal f f' }) + = match f.v with + | AtomicField af -> + let s, a = size_and_alignment_of_atomic_field env af in + f, s, a - | Record names params where fields -> + | RecordField fields -> let aligned_field_size (offset:size) (max_align:alignment) (fields:list field) (f:field) : ML (size & alignment & list field) - = let field_size, field_alignment = size_and_alignment_of_field env f in + = 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)" (ident_to_string f.v.field_ident) in - alignment_padding env names msg offset field_alignment + let msg = Printf.sprintf "(preceding field %s)" (print_field field) in + alignment_padding env should_align diag_enclosing_type_name msg offset field_alignment in let offset = (offset `sum_size` (Fixed pad_size)) `sum_size` @@ -317,23 +324,29 @@ let decl_size_with_alignment (env:env_t) (d:decl) fields in let pad_size, end_padding = - alignment_padding env names "(end padding)" size max_align + alignment_padding env should_align diag_enclosing_type_name "(end padding)" size max_align in let size = size `sum_size` (Fixed pad_size) in let fields_rev = end_padding @ fields_rev in let fields = List.rev fields_rev in - extend_with_size_of_typedef_names env names size max_align; - decl_with_v d (Record names params where fields) + { f with v = RecordField fields }, + size, + max_align - | CaseType names params cases -> + | SwitchCaseField swc -> let case_sizes = List.map (function - | Case _ f + | Case p f -> + let f, s, a = size_and_alignment_of_field env should_align diag_enclosing_type_name f in + Case p f, (s, a) + | DefaultCase f -> - size_and_alignment_of_field env f) - (snd cases) + let f, s, a = size_and_alignment_of_field env should_align diag_enclosing_type_name f in + DefaultCase f, (s, a)) + (snd swc) in + let cases, size_and_alignments = List.unzip case_sizes in let combine_size_and_alignment (accum_size, accum_align) (f_size, f_align) @@ -358,7 +371,7 @@ let decl_size_with_alignment (env:env_t) (d:decl) List.fold_left combine_size_and_alignment (None, None) - case_sizes + size_and_alignments in let size = match size with @@ -366,18 +379,10 @@ let decl_size_with_alignment (env:env_t) (d:decl) | Some s -> s in let alignment = if Fixed? size then alignment else None in - let all_fixed = - List.for_all - (fun (size, _) -> - match size with - | Fixed _ -> true - | _ -> false) - case_sizes - in - if should_align names + if should_align then ( let all_cases_fixed = - List.for_all (function (Fixed _, _) -> true | _ -> false) case_sizes + List.for_all (function (Fixed _, _) -> true | _ -> false) size_and_alignments in if all_cases_fixed && not (Fixed? size) @@ -386,10 +391,39 @@ let decl_size_with_alignment (env:env_t) (d:decl) all cases of a union with a fixed size \ must have the same size; \ union padding is not yet supported" - d.d_decl.range + f.range ); - extend_with_size_of_typedef_names env names size alignment; + let swc = fst swc, cases in + let f = { f with v = SwitchCaseField swc } in + f, size, alignment + + +let decl_size_with_alignment (env:env_t) (d:decl) + : ML decl + = match d.d_decl.v with + | ModuleAbbrev _ _ -> d + | Define _ _ _ -> d + + | TypeAbbrev t i + | Enum t i _ -> + let s, a = size_and_alignment_of_typ env t in + extend_with_size_of_ident env i s a; d + + | Record names params where fields -> + let { v = RecordField fields }, size, max_align = + size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (RecordField fields)) + in + extend_with_size_of_typedef_names env names size max_align; + decl_with_v d (Record names params where fields) + + | CaseType names params cases -> + let { v = SwitchCaseField cases }, size, alignment = + size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (SwitchCaseField cases)) + in + extend_with_size_of_typedef_names env names size alignment; + decl_with_v d (CaseType names params cases) + | OutputType _ | ExternType _ | ExternFn _ _ _ diff --git a/src/3d/ocaml/parser.mly b/src/3d/ocaml/parser.mly index 5de2a4636..64d99b4e2 100644 --- a/src/3d/ocaml/parser.mly +++ b/src/3d/ocaml/parser.mly @@ -274,7 +274,8 @@ field: { let comms = Ast.comments_buffer.flush () in let range = (mk_pos $startpos, mk_pos $startpos) in - with_range_and_comments f range comms + let af' = with_range_and_comments f range comms in + with_range_and_comments (AtomicField af') range comms } From 6bd1150b28df2cc968154518dbd0aa5343ac67fd Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 16 Aug 2022 20:02:54 +0000 Subject: [PATCH 04/12] support for anonymous structs, case types, and #if fields --- src/3d/Ast.fst | 22 +++---- src/3d/Binding.fst | 81 ++++++++++++++++---------- src/3d/BitFields.fst | 15 ++--- src/3d/Deps.fst | 5 +- src/3d/Desugar.fst | 27 ++++----- src/3d/InlineSingletonRecords.fst | 4 +- src/3d/Simplify.fst | 4 +- src/3d/TranslateForInterpreter.fst | 93 +++++++++++++++++------------- src/3d/TypeSizes.fst | 18 +++--- src/3d/ocaml/parser.mly | 68 ++++++++++++++++++++-- src/3d/tests/AnonNestedStruct.3d | 39 +++++++++++++ 11 files changed, 253 insertions(+), 123 deletions(-) create mode 100644 src/3d/tests/AnonNestedStruct.3d diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst index 1d2c0d2c4..32de28d41 100644 --- a/src/3d/Ast.fst +++ b/src/3d/Ast.fst @@ -243,7 +243,6 @@ type op = | LE of option integer_type | GE of option integer_type | IfThenElse - | HashIfThenElse | BitFieldOf of int //BitFieldOf_n(i, from, to); the integer is the size of i in bits | SizeOf | Cast : from:option integer_type -> to:integer_type -> op @@ -259,6 +258,7 @@ noeq type expr' = | Constant of constant | Identifier of ident + | Static of expr //the guard of a #if; must be made from compile-time constants only | This | App : op -> list expr -> expr' @@ -452,8 +452,8 @@ and atomic_field = with_meta_t atomic_field' and field' = | AtomicField of atomic_field - | RecordField of record - | SwitchCaseField of switch_case + | RecordField : record -> ident -> field' + | SwitchCaseField : switch_case -> ident -> field' and field = with_meta_t field' @@ -676,6 +676,7 @@ let rec subst_expr (s:subst) (e:expr) : ML expr = | Constant _ | This -> e | Identifier i -> apply s i + | Static e -> { e with v = Static (subst_expr s e) } | App op es -> {e with v = App op (List.map (subst_expr s) es)} let subst_atomic_action (s:subst) (aa:atomic_action) : ML atomic_action = match aa with @@ -713,8 +714,8 @@ let subst_field_array (s:subst) (f:field_array_t) : ML field_array_t = let rec subst_field (s:subst) (ff:field) : ML field = match ff.v with | AtomicField f -> {ff with v = AtomicField (subst_atomic_field s f)} - | RecordField f -> {ff with v = RecordField (subst_record s f)} - | SwitchCaseField f -> {ff with v = SwitchCaseField (subst_switch_case s f)} + | RecordField f i -> {ff with v = RecordField (subst_record s f) i} + | SwitchCaseField f i -> {ff with v = SwitchCaseField (subst_switch_case s f) i} and subst_atomic_field (s:subst) (f:atomic_field) : ML atomic_field = let sf = f.v in let a = @@ -806,7 +807,6 @@ let print_op = function | LE _ -> "<=" | GE _ -> ">=" | IfThenElse -> "ifthenelse" - | HashIfThenElse -> "#ifthenelse" | BitFieldOf i -> Printf.sprintf "bitfield_of(%d)" i | SizeOf -> "sizeof" | Cast _ t -> "(" ^ print_integer_type t ^ ")" @@ -820,6 +820,8 @@ let rec print_expr (e:expr) : Tot string = print_ident i | This -> "this" + | Static e -> + Printf.sprintf "static(%s)" (print_expr e) | App Eq [e1; e2] -> Printf.sprintf "(%s = %s)" (print_expr e1) (print_expr e2) | App And [e1; e2] -> @@ -928,8 +930,8 @@ let print_bitfield (bf:option field_bitwidth_t) = let rec print_field (f:field) : ML string = match f.v with | AtomicField f -> print_atomic_field f - | RecordField f -> print_record f - | SwitchCaseField f -> print_switch_case 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 and print_record (f:record) : ML string = List.map print_field f |> @@ -1053,6 +1055,6 @@ let weak_kind_glb (w1 w2: weak_kind) : Tot weak_kind = let field_tag_equal (f0 f1:field) = match f0.v, f1.v with | AtomicField _, AtomicField _ - | RecordField _, RecordField _ - | SwitchCaseField _, SwitchCaseField _ -> true + | RecordField _ _, RecordField _ _ + | SwitchCaseField _ _, SwitchCaseField _ _ -> true | _ -> false diff --git a/src/3d/Binding.fst b/src/3d/Binding.fst index f364f9c88..64be1f82f 100644 --- a/src/3d/Binding.fst +++ b/src/3d/Binding.fst @@ -667,6 +667,9 @@ and check_expr (env:env) (e:expr) let t = lookup_expr_name env i in e, t + | Static _ -> + failwith "Static expressions should have been desugared already" + | This -> error "`this` is not a valid expression" e.range @@ -1130,8 +1133,8 @@ let weak_kind_of_list (wa:'a -> ML weak_kind) (xs:list 'a) : ML weak_kind = let rec weak_kind_of_field (env: env) (f: field) : ML weak_kind = match f.v with | AtomicField f -> weak_kind_of_atomic_field env f - | RecordField f -> weak_kind_of_record env f - | SwitchCaseField f -> weak_kind_of_switch_case env f + | RecordField f _ -> weak_kind_of_record env f + | SwitchCaseField f _ -> weak_kind_of_switch_case env f and weak_kind_of_record env (fs:record) : ML weak_kind = match fs with @@ -1252,6 +1255,11 @@ let check_switch (check_field:check_field_t) (env:env) (s:switch_case) (head, cases) #pop-options +let is_bound_locally (env:env) (i:ident) = + match H.try_find env.locals i.v with + | None -> false + | Some _ -> true + let rec check_record (check_field:check_field_t) (env:env) (fs:record) : ML record = let env = copy_env env in //locals of a record do not escape the record @@ -1266,13 +1274,13 @@ let rec check_record (check_field:check_field_t) (env:env) (fs:record) let af = check_atomic_field env true af in { f with v = AtomicField af } - | RecordField fs -> + | RecordField fs i -> let fs = check_record check_field env fs in - { f with v = RecordField fs } + {f with v = RecordField fs i } - | SwitchCaseField swc -> + | SwitchCaseField swc i -> let swc = check_switch check_field env swc in - { f with v = SwitchCaseField swc }) + { f with v = SwitchCaseField swc i}) fs in @@ -1280,8 +1288,8 @@ let rec check_record (check_field:check_field_t) (env:env) (fs:record) let nfields = List.length fields in let fields = fields |> List.mapi (fun i f -> match f.v with - | RecordField _ - | SwitchCaseField _ -> f + | RecordField _ _ + | SwitchCaseField _ _ -> f | AtomicField af -> let sf = af.v in let used = is_used env sf.field_ident in @@ -1306,18 +1314,37 @@ let rec check_record (check_field:check_field_t) (env:env) (fs:record) in fields + +let name_of_field (f:field) : ident = + match f.v with + | AtomicField af -> af.v.field_ident + | RecordField _ i + | SwitchCaseField _ i -> i + +let check_field_names_unique (f:list field) + : ML unit + = match f with + | [] + | [_] -> () + | hd::tl -> + let i = name_of_field hd in + if List.for_all (fun f' -> not (eq_idents (name_of_field f') i)) tl + then () + else error (Printf.sprintf "Field name %s is not unique" i.v.name) i.range + let rec check_field (env:env) (f:field) : ML field = match f.v with | AtomicField af -> { f with v = AtomicField (check_atomic_field env false af) } - | RecordField fs -> - { f with v = RecordField (check_record check_field env fs) } - - | SwitchCaseField swc -> - { f with v = SwitchCaseField (check_switch check_field env swc) } + | RecordField fs i -> + check_field_names_unique fs; + { f with v = RecordField (check_record check_field env fs) i } + | SwitchCaseField swc i -> + { f with v = SwitchCaseField (check_switch check_field env swc) i } + (** Computes a layout for bit fields, decorating each field with a bitfield index and a bit range within that bitfield to store the given field. @@ -1326,7 +1353,7 @@ let rec check_field (env:env) (f:field) separate phase, see BitFields.fst *) let elaborate_bit_fields env (fields:list field) - : ML (list field) + : ML (out:list field { List.length out == List.length fields }) = let bf_index : ref int = ST.alloc 0 in let get_bf_index () = !bf_index in let next_bf_index () = bf_index := !bf_index + 1 in @@ -1349,7 +1376,7 @@ let elaborate_bit_fields env (fields:list field) Some (sf.field_type, to, remaining_size) in let rec aux open_bit_field fields - : ML (list field) + : ML (out:list field { List.length out == List.length fields } ) = match fields with | [] -> [] @@ -1357,37 +1384,29 @@ let elaborate_bit_fields env (fields:list field) | hd::tl -> begin match hd.v with - | RecordField fs -> + | RecordField fs hd_fieldname -> next_bf_index(); let fs = aux None fs in - let hd = { hd with v = RecordField fs } in + let hd = { hd with v = RecordField fs hd_fieldname } in next_bf_index(); hd :: aux None tl - | SwitchCaseField (e, cases) -> + | SwitchCaseField (e, cases) hd_fieldname -> next_bf_index(); let cases = List.map (function | Case p f -> - let fs = aux None [f] in - begin - match fs with - | [f] -> Case p f - | _ -> Case p (with_range_and_comments (RecordField fs) f.range f.comments) - end + let [f] = aux None [f] in + Case p f | DefaultCase f -> - let fs = aux None [f] in - begin - match fs with - | [f] -> DefaultCase f - | _ -> DefaultCase (with_range_and_comments (RecordField fs) f.range f.comments) - end) + let [f] = aux None [f] in + DefaultCase f) cases in next_bf_index(); - let hd = { hd with v = SwitchCaseField (e, cases) } in + let hd = { hd with v = SwitchCaseField (e, cases) hd_fieldname } in hd :: aux None tl | AtomicField af -> diff --git a/src/3d/BitFields.fst b/src/3d/BitFields.fst index 38edd2f11..109c4d0f6 100644 --- a/src/3d/BitFields.fst +++ b/src/3d/BitFields.fst @@ -37,8 +37,8 @@ let group_bit_fields (rewrite_composite_field: field -> ML field) = List.fold_right (fun field out -> match field.v with - | RecordField _ - | SwitchCaseField _ -> + | RecordField _ _ + | SwitchCaseField _ _ -> Inl (rewrite_composite_field field) :: out | AtomicField af -> @@ -132,7 +132,7 @@ let rec rewrite_field (env:B.global_env) (f:field) = match f.v with | AtomicField _ -> f - | RecordField fs -> + | RecordField fs field_name -> let gfs = group_bit_fields (rewrite_field env) fs in let fs, subst = List.fold_right @@ -146,9 +146,9 @@ let rec rewrite_field (env:B.global_env) (f:field) ([], []) in let fs = List.map (subst_field (mk_subst subst)) fs in - { f with v = RecordField fs } + { f with v = RecordField fs field_name } - | SwitchCaseField (e, cases) -> + | SwitchCaseField (e, cases) field_name -> let cases = List.map (function @@ -159,13 +159,14 @@ let rec rewrite_field (env:B.global_env) (f:field) DefaultCase (rewrite_field env f)) cases in - { f with v = SwitchCaseField (e, cases) } + { f with v = SwitchCaseField (e, cases) field_name } let eliminate_one_decl (env:B.global_env) (d:decl) : ML decl = match d.d_decl.v with | Record names params where fields -> - let { v = RecordField fields } = rewrite_field env (with_dummy_range (RecordField fields)) in + let i = with_dummy_range (to_ident' "_") in + let { v = RecordField fields _ } = rewrite_field env (with_dummy_range (RecordField fields i)) in List.iter (fun f -> Options.debug_print_string (Printf.sprintf "Bitfields: Field %s has comments <%s>\n" diff --git a/src/3d/Deps.fst b/src/3d/Deps.fst index 74a97b602..3aaae610a 100644 --- a/src/3d/Deps.fst +++ b/src/3d/Deps.fst @@ -97,6 +97,7 @@ let scan_deps (fn:string) : ML scan_deps_t = | Constant _ -> [] | Identifier i -> maybe_dep i | This -> [] + | Static e -> deps_of_expr e | App _op args -> List.collect deps_of_expr args in let deps_of_typ_param (p:typ_param) : ML (list string) = @@ -157,8 +158,8 @@ let scan_deps (fn:string) : ML scan_deps_t = let rec deps_of_field (f:field) : ML (list string) = match f.v with | AtomicField af -> deps_of_atomic_field af - | RecordField fs -> List.collect deps_of_field fs - | SwitchCaseField swc -> deps_of_switch_case swc + | RecordField fs _ -> List.collect deps_of_field fs + | SwitchCaseField swc _ -> deps_of_switch_case swc and deps_of_case (c:case) : ML (list string) = match c with | Case e f -> (deps_of_expr e)@(deps_of_field f) diff --git a/src/3d/Desugar.fst b/src/3d/Desugar.fst index a091ecbda..48440790a 100644 --- a/src/3d/Desugar.fst +++ b/src/3d/Desugar.fst @@ -32,8 +32,8 @@ module H = Hashtable * Set the kind (Spec/Output/Extern) in the type nodes - * Find variables in HashIfThenElse and hoist them as assumptions - and rewrite HashIfThenElse to IfThenElse + * Finds variables in Static expressions and hoists them as assumptions + and removes the Static *) #push-options "--warn_error -272" //intentional top-level effect @@ -198,6 +198,7 @@ let rec collect_ifdef_guards (env:qenv) (e:expr) : ML unit = match e.v with | This -> error "'this' is not allowed in the guard of an #if" e.range + | Static _ -> failwith "static should have been eliminated already" | Constant _ -> () | Identifier i -> if List.mem i.v.name env.local_names //it's a local name (e.g. a parameter name) @@ -233,20 +234,14 @@ let rec resolve_expr' (env:qenv) (e:expr') r : ML expr' = | Constant _ -> e | Identifier i -> Identifier (resolve_ident env i) | This -> e + | Static e' -> + let e' = resolve_expr env e' in + collect_ifdef_guards env e';//mark any variables as top-level IfDef symbols + e'.v + | App op args -> let args = List.map (resolve_expr env) args in - match op with - | HashIfThenElse -> - begin - match args with - | [guard; br1; br2] -> - collect_ifdef_guards env guard;//mark any variables as top-level IfDef symbols - App IfThenElse args //rewrite away the HashIfThenElse - | _ -> error "Unexpected arguments to a #if/#else" r - end - - | _ -> - App op args + App op args and resolve_expr (env:qenv) (e:expr) : ML expr = { e with v = resolve_expr' env e.v e.range } @@ -340,8 +335,8 @@ let resolve_field_array_t (env:qenv) (farr:field_array_t) : ML field_array_t = let rec resolve_field (env:qenv) (ff:field) : ML (field & qenv) = match ff.v with | AtomicField f -> let f, e = resolve_atomic_field env f in {ff with v = AtomicField f}, e - | RecordField f -> let fs, _ = resolve_fields env f in {ff with v = RecordField fs}, env //record fields are not in scope outside the record - | SwitchCaseField f -> let f = resolve_switch_case env f in {ff with v = SwitchCaseField f}, env + | RecordField f i -> let fs, _ = resolve_fields env f in {ff with v = RecordField fs i}, env //record fields are not in scope outside the record + | SwitchCaseField f i -> let f = resolve_switch_case env f in {ff with v = SwitchCaseField f i}, env and resolve_atomic_field (env:qenv) (f:atomic_field) : ML (atomic_field & qenv) = let resolve_atomic_field' (env:qenv) (sf:atomic_field') : ML atomic_field' = diff --git a/src/3d/InlineSingletonRecords.fst b/src/3d/InlineSingletonRecords.fst index 73ed2eb23..f2a93d92d 100644 --- a/src/3d/InlineSingletonRecords.fst +++ b/src/3d/InlineSingletonRecords.fst @@ -110,8 +110,8 @@ let rec simplify_field (env:env) (f:field) : ML field = match f.v with | AtomicField f -> { f with v = AtomicField (simplify_atomic_field env f) } - | RecordField fs -> { f with v = RecordField (List.map (simplify_field env) fs) } - | SwitchCaseField swc -> { f with v = SwitchCaseField (simplify_switch_case env swc) } + | RecordField fs i -> { f with v = RecordField (List.map (simplify_field env) fs) i } + | SwitchCaseField swc i -> { f with v = SwitchCaseField (simplify_switch_case env swc) i } and simplify_switch_case (env:env) (swc:switch_case) : ML switch_case diff --git a/src/3d/Simplify.fst b/src/3d/Simplify.fst index edaf7a075..ab3a1f73d 100644 --- a/src/3d/Simplify.fst +++ b/src/3d/Simplify.fst @@ -133,8 +133,8 @@ let rec simplify_field (env:T.env_t) (f:field) : ML field = match f.v with | AtomicField af -> { f with v = AtomicField (simplify_atomic_field env af) } - | RecordField fs -> { f with v = RecordField (List.map (simplify_field env) fs) } - | SwitchCaseField swc -> { f with v = SwitchCaseField (simplify_switch_case env swc) } + | RecordField fs i -> { f with v = RecordField (List.map (simplify_field env) fs) i } + | SwitchCaseField swc i -> { f with v = SwitchCaseField (simplify_switch_case env swc) i } and simplify_switch_case (env:T.env_t) (c:switch_case) : ML switch_case = diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index cbbb16cea..f6ad4ca2a 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -287,7 +287,6 @@ let translate_op : A.op -> ML T.op = | Cast (Some from) to -> T.Cast from to | Ext s -> T.Ext s | Cast None _ - | HashIfThenElse | SizeOf -> failwith (Printf.sprintf "Operator `%s` should have been eliminated already" (Ast.print_op op)) @@ -297,6 +296,7 @@ let rec translate_expr (e:A.expr) : ML T.expr = | Constant c -> T.Constant c | Identifier i -> T.Identifier i | App op exprs -> T.App (translate_op op) (List.map translate_expr exprs) + | Static _ -> failwith "`static` should have been eliminated already" | This -> failwith "`this` should have been eliminated already"), e.A.range @@ -928,7 +928,7 @@ type grouped_fields = | DependentField : hd:T.field -> tl:grouped_fields -> grouped_fields | NonDependentField : hd:T.field -> tl:grouped_fields -> grouped_fields | ITEGroup : e:T.expr -> then_:grouped_fields -> else_:grouped_fields -> grouped_fields - | GroupThen : struct:grouped_fields -> rest:grouped_fields -> grouped_fields + | GroupThen : id:A.ident -> struct:grouped_fields -> rest:grouped_fields -> grouped_fields let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields) : ML T.parser @@ -998,13 +998,12 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields let else_ = aux else_ in ite_parser typename id.v.name e then_ else_ - | GroupThen gfs rest -> ( + | GroupThen id gfs rest -> ( match rest with | Empty_grouped_field -> aux gfs | _ -> - let id = gen_ident None in pair_parser id (aux gfs) (aux rest) @@ -1231,33 +1230,34 @@ let hoist_refinements (genv:global_env) (tdn:T.typedef_name) (fields:list T.fiel in decls, List.rev fields -let type_of_grouped_fields (gfs:grouped_fields) : T.typ = admit() - let rec field_as_grouped_fields (f:A.field) - : ML (grouped_fields & T.decls) + : ML (A.ident & grouped_fields & T.decls) = match f.v with | AtomicField af -> let sf, ds = translate_atomic_field af in - NonDependentField sf Empty_grouped_field, ds - - | RecordField fs -> - List.fold_right - (fun f (gfs, ds_out) -> - match f.v with - | AtomicField af -> - let sf, ds = translate_atomic_field af in - if sf.sf_dependence - then DependentField sf gfs, ds@ds_out - else NonDependentField sf gfs, ds@ds_out - - | RecordField _ - | SwitchCaseField _ -> - let gf, ds = field_as_grouped_fields f in - GroupThen gf gfs, ds@ds_out) - fs - (Empty_grouped_field, []) - - | SwitchCaseField swc -> + sf.sf_ident, NonDependentField sf Empty_grouped_field, ds + + | RecordField fs field_name -> + let gfs, ds = + List.fold_right + (fun f (gfs, ds_out) -> + match f.v with + | AtomicField af -> + let sf, ds = translate_atomic_field af in + if sf.sf_dependence + then DependentField sf gfs, ds@ds_out + else NonDependentField sf gfs, ds@ds_out + + | RecordField _ _ + | SwitchCaseField _ _ -> + let id, gf, ds = field_as_grouped_fields f in + GroupThen id gf gfs, ds@ds_out) + fs + (Empty_grouped_field, []) + in + field_name, gfs, ds + + | SwitchCaseField swc field_name -> let sc, cases = swc in let sc = translate_expr sc in let false_field = @@ -1273,7 +1273,7 @@ let rec field_as_grouped_fields (f:A.field) let rest, last = List.splitAt (List.length cases - 1) cases in match last with | [DefaultCase f] -> - let gfs, ds = field_as_grouped_fields f in + let _, gfs, ds = field_as_grouped_fields f in rest, gfs, ds | _ -> @@ -1281,22 +1281,31 @@ let rec field_as_grouped_fields (f:A.field) else cases, false_field, [] in - List.fold_right - (fun case (else_group, decls') -> - match case with - | DefaultCase _ -> failwith "Impossible" - | Case p f -> - let gfs, decls = field_as_grouped_fields f in - let guard = T.mk_expr (T.App T.Eq [sc; translate_expr p]) in - ITEGroup guard gfs else_group, decls@decls') - rest - (default_group, decls) + let gfs, ds = + List.fold_right + (fun case (else_group, decls') -> + match case with + | DefaultCase _ -> failwith "Impossible" + | Case p f -> + let _, gfs, decls = field_as_grouped_fields f in + let guard = + match p.v with + | Constant (Bool true) -> + // simplify (sc == true) to just (sc) + sc + | _ -> T.mk_expr (T.App T.Eq [sc; translate_expr p]) + in + ITEGroup guard gfs else_group, decls@decls') + rest + (default_group, decls) + in + field_name, gfs, ds let parse_field (env:global_env) (typename:A.ident) (f:A.field) : ML (T.parser & T.decls) - = let gfs, decls = field_as_grouped_fields f in + = let _, gfs, decls = field_as_grouped_fields f in parse_grouped_fields env typename gfs, decls @@ -1352,7 +1361,8 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = | Record tdn params _ ast_fields -> let tdn, ds1 = translate_typedef_name tdn params in - let p, ds2 = parse_field env tdn.td_name (with_dummy_range (RecordField ast_fields)) in + let dummy_ident = with_dummy_range (to_ident' "_") in + let p, ds2 = parse_field env tdn.td_name (with_dummy_range (RecordField ast_fields dummy_ident)) in let open T in add_parser_kind_nz env tdn.td_name p.p_kind.pk_nz p.p_kind.pk_weak_kind; add_parser_kind_is_constant_size env tdn.td_name (parser_is_constant_size_without_actions env p); @@ -1370,7 +1380,8 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = | CaseType tdn0 params switch_case -> let tdn, ds1 = translate_typedef_name tdn0 params in - let p, ds2 = parse_field env tdn.td_name (with_dummy_range (SwitchCaseField switch_case)) in + let dummy_ident = with_dummy_range (to_ident' "_") in + let p, ds2 = parse_field env tdn.td_name (with_dummy_range (SwitchCaseField switch_case dummy_ident)) in // let t, ds2 = translate_switch_case_type env tdn switch_case in // let p = parse_typ env tdn0.typedef_name "" t in let open T in diff --git a/src/3d/TypeSizes.fst b/src/3d/TypeSizes.fst index b20a642ac..515a53b22 100644 --- a/src/3d/TypeSizes.fst +++ b/src/3d/TypeSizes.fst @@ -288,7 +288,7 @@ let rec size_and_alignment_of_field (env:env_t) let s, a = size_and_alignment_of_atomic_field env af in f, s, a - | RecordField fields -> + | RecordField fields field_name -> let aligned_field_size (offset:size) (max_align:alignment) @@ -329,11 +329,11 @@ let rec size_and_alignment_of_field (env:env_t) let size = size `sum_size` (Fixed pad_size) in let fields_rev = end_padding @ fields_rev in let fields = List.rev fields_rev in - { f with v = RecordField fields }, + { f with v = RecordField fields field_name }, size, max_align - | SwitchCaseField swc -> + | SwitchCaseField swc field_name -> let case_sizes = List.map (function @@ -394,7 +394,7 @@ let rec size_and_alignment_of_field (env:env_t) f.range ); let swc = fst swc, cases in - let f = { f with v = SwitchCaseField swc } in + let f = { f with v = SwitchCaseField swc field_name } in f, size, alignment @@ -411,15 +411,17 @@ let decl_size_with_alignment (env:env_t) (d:decl) d | Record names params where fields -> - let { v = RecordField fields }, size, max_align = - size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (RecordField fields)) + let dummy_ident = with_dummy_range (to_ident' "_") in + let { v = RecordField fields _ }, size, max_align = + size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (RecordField fields dummy_ident)) in extend_with_size_of_typedef_names env names size max_align; decl_with_v d (Record names params where fields) | CaseType names params cases -> - let { v = SwitchCaseField cases }, size, alignment = - size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (SwitchCaseField cases)) + let dummy_ident = with_dummy_range (to_ident' "_") in + let { v = SwitchCaseField cases _ }, size, alignment = + size_and_alignment_of_field env (should_align names) names.typedef_name (with_dummy_range (SwitchCaseField cases dummy_ident)) in extend_with_size_of_typedef_names env names size alignment; decl_with_v d (CaseType names params cases) diff --git a/src/3d/ocaml/parser.mly b/src/3d/ocaml/parser.mly index 64d99b4e2..8a0fef52f 100644 --- a/src/3d/ocaml/parser.mly +++ b/src/3d/ocaml/parser.mly @@ -190,7 +190,8 @@ expr_no_range: | None -> with_range (Constant (Bool true)) $startpos | Some e2 -> e2 in - App(HashIfThenElse, [e;e1;e2]) + let e = with_range (Static e) ($startpos(e)) in + App(IfThenElse, [e;e1;e2]) } | i=IDENT LPAREN es=arguments RPAREN @@ -255,7 +256,7 @@ field_action: | LBRACE_CHECK a=action RBRACE { a, false } | LBRACE_ACT a=action RBRACE { with_range (Action_act a) $startpos(a), false } -struct_field: +atomic_field: | t=typ fn=IDENT bopt=option_of(bitwidth) aopt=array_annot c=option_of(refinement) a=option_of(field_action) { { @@ -269,15 +270,73 @@ struct_field: } } +anonymous_struct_field: + | STRUCT LBRACE fields=right_flexible_nonempty_list(SEMICOLON, field) RBRACE fn=IDENT + { + RecordField(fields, fn) + } + +anonymous_casetype_field: + | SWITCH LPAREN i=IDENT RPAREN LBRACE cs=cases RBRACE fn=IDENT + { + let e = with_range (Identifier i) ($startpos(i)) in + SwitchCaseField((e, cs), fn) + } + +static_conditional_field: + | HASH_IF e=atomic_or_paren_expr f_then=fields HASH_ELSE f_else=fields HASH_ENDIF + { + let tt = with_range (Constant (Bool true)) ($startpos(e)) in + let dummy_identifier = with_range (to_ident' "_") ($startpos(e)) in + let f_then = + match f_then with + | [f] -> f + | _ -> with_range (RecordField(f_then, dummy_identifier)) ($startpos(f_then)) + in + let f_else = + match f_else with + | [f] -> f + | _ -> with_range (RecordField(f_else, dummy_identifier)) ($startpos(f_else)) + in + let case_then = Case (tt, f_then) in + let case_else = DefaultCase f_else in + let e = with_range (Static e) ($startpos(e)) in + SwitchCaseField ((e, [case_then; case_else]), dummy_identifier) + } + field: - | f = struct_field + | f = atomic_field { let comms = Ast.comments_buffer.flush () in let range = (mk_pos $startpos, mk_pos $startpos) in let af' = with_range_and_comments f range comms in with_range_and_comments (AtomicField af') range comms } + + | rf = anonymous_struct_field + { + let comms = Ast.comments_buffer.flush () in + let range = (mk_pos $startpos, mk_pos $startpos) in + with_range_and_comments rf range comms + } + | cf = anonymous_casetype_field + { + let comms = Ast.comments_buffer.flush () in + let range = (mk_pos $startpos, mk_pos $startpos) in + with_range_and_comments cf range comms + } + + | cf = static_conditional_field + { + let comms = Ast.comments_buffer.flush () in + let range = (mk_pos $startpos, mk_pos $startpos) in + with_range_and_comments cf range comms + } + +fields: + | fields=right_flexible_nonempty_list(SEMICOLON, field) + { fields } immutable_parameter: | t=typ i=IDENT { (t, i, Immutable) } @@ -399,7 +458,7 @@ decl_no_range: | b=attributes TYPEDEF t=typ i=IDENT SEMICOLON { TypeAbbrev (t, i) } | b=attributes TYPEDEF STRUCT i=IDENT ps=parameters w=where_opt - LBRACE fields=right_flexible_nonempty_list(SEMICOLON, field) + LBRACE fields=fields RBRACE j=IDENT p=typedef_pointer_name_opt SEMICOLON { let k = pointer_name j p in Record(mk_td b i j k, ps, w, fields) @@ -463,6 +522,7 @@ type_refinement: } } + prog: | d=decl r=option_of(type_refinement) EOF { [d], r } diff --git a/src/3d/tests/AnonNestedStruct.3d b/src/3d/tests/AnonNestedStruct.3d new file mode 100644 index 000000000..d926e15f6 --- /dev/null +++ b/src/3d/tests/AnonNestedStruct.3d @@ -0,0 +1,39 @@ +entrypoint +typedef struct _Point3D { + struct { + UINT32 a; + UINT32 b; + } point2d; + UINT32 z; +} Point3D; + +entrypoint +typedef struct _TaggedPoint { + UINT8 dim_2; + switch (dim_2) { + case 0: + struct { + UINT32 x; + UINT32 y; + } p2; + + default: + struct { + UINT32 x; + UINT32 y; + UINT32 z; + } p3; + } payload; +} TaggedPoint; + +entrypoint +typedef struct _StaticConditionalPoint { + #if DIM2 + UINT32 x; + UINT32 y; + #else + UINT32 x; + UINT32 y; + UINT32 z; + #endif +} StaticConditionalPoint; From 2c458ddba3b75c2a8a1c9b04002f21c02e448018 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 16 Aug 2022 22:41:28 +0000 Subject: [PATCH 05/12] support for #elif --- src/3d/ocaml/lexer.mll | 1 + src/3d/ocaml/parser.mly | 89 +++++++++++++++++++++----------- src/3d/tests/AnonNestedStruct.3d | 26 +++++++--- src/3d/tests/CompileTimeIf.3d | 8 +-- 4 files changed, 85 insertions(+), 39 deletions(-) diff --git a/src/3d/ocaml/lexer.mll b/src/3d/ocaml/lexer.mll index 265c1b005..a5fca2df9 100644 --- a/src/3d/ocaml/lexer.mll +++ b/src/3d/ocaml/lexer.mll @@ -108,6 +108,7 @@ rule token = | "/*++" { block_comment ("", Lexing.lexeme_start_p lexbuf) lexbuf } | "/*" { multi_line_comment lexbuf } | "#if" { locate lexbuf HASH_IF } + | "#elif" { locate lexbuf HASH_ELIF } | "#else" { locate lexbuf HASH_ELSE } | "#endif" { locate lexbuf HASH_ENDIF } | "(" { locate lexbuf LPAREN } diff --git a/src/3d/ocaml/parser.mly b/src/3d/ocaml/parser.mly index 8a0fef52f..773a4c764 100644 --- a/src/3d/ocaml/parser.mly +++ b/src/3d/ocaml/parser.mly @@ -44,6 +44,19 @@ out_expr_meta = None } + let unit_atomic_field' rng = + let dummy_identifier = with_range (to_ident' "_empty_") rng in + { + field_dependence=false; + field_ident=dummy_identifier; + field_type=tunit; + field_array_opt=FieldScalar; + field_constraint=None; + field_bitwidth=None; + field_action=None + } + + %} %token INT XINT STRING @@ -59,7 +72,7 @@ %token REM SHIFT_LEFT SHIFT_RIGHT BITWISE_AND BITWISE_OR BITWISE_XOR BITWISE_NOT AS %token MODULE EXPORT OUTPUT UNION EXTERN %token ENTRYPOINT REFINING ALIGNED -%token HASH_IF HASH_ELSE HASH_ENDIF +%token HASH_IF HASH_ELSE HASH_ENDIF HASH_ELIF (* LBRACE_ONERROR CHECK *) %start prog %start expr_top @@ -110,8 +123,9 @@ else_opt: | ELSE LBRACE e=expr RBRACE { Some e } hash_else_opt: - | { None } - | HASH_ELSE e=expr { Some e } + | HASH_ENDIF { None } + | HASH_ELSE e=expr HASH_ENDIF { Some e } + | HASH_ELIF e=hash_if_body { Some (with_range e ($startpos)) } atomic_expr: | i=qident { Identifier i } @@ -127,6 +141,18 @@ castable_expr: | e=atomic_expr { Some e } | LPAREN e=expr RPAREN { Some e.v } +hash_if_body: + | e=atomic_or_paren_expr e1=expr e2=hash_else_opt + { + let e2 = + match e2 with + | None -> with_range (Constant (Bool true)) $startpos + | Some e2 -> e2 + in + let e = with_range (Static e) ($startpos(e)) in + App(IfThenElse, [e;e1;e2]) + } + expr_no_range: | e=atomic_expr { e } | LPAREN e=expr RPAREN eopt=castable_expr { @@ -183,16 +209,8 @@ expr_no_range: in App(IfThenElse, [e;e1;e2]) } - | HASH_IF e=atomic_or_paren_expr e1=expr e2=hash_else_opt HASH_ENDIF - { - let e2 = - match e2 with - | None -> with_range (Constant (Bool true)) $startpos - | Some e2 -> e2 - in - let e = with_range (Static e) ($startpos(e)) in - App(IfThenElse, [e;e1;e2]) - } + | HASH_IF e=hash_if_body + { e } | i=IDENT LPAREN es=arguments RPAREN { @@ -271,7 +289,7 @@ atomic_field: } anonymous_struct_field: - | STRUCT LBRACE fields=right_flexible_nonempty_list(SEMICOLON, field) RBRACE fn=IDENT + | STRUCT LBRACE fields=fields RBRACE fn=IDENT { RecordField(fields, fn) } @@ -283,29 +301,42 @@ anonymous_casetype_field: SwitchCaseField((e, cs), fn) } -static_conditional_field: - | HASH_IF e=atomic_or_paren_expr f_then=fields HASH_ELSE f_else=fields HASH_ENDIF +maybe_hash_else_fields: + | HASH_ENDIF { None } + | HASH_ELSE f_else=option_of(fields) HASH_ENDIF { f_else } + | HASH_ELIF f=static_conditional_body { Some [with_range f ($startpos)] } + +static_conditional_body: + | e=atomic_or_paren_expr f_then=option_of(fields) f_else=maybe_hash_else_fields { let tt = with_range (Constant (Bool true)) ($startpos(e)) in let dummy_identifier = with_range (to_ident' "_") ($startpos(e)) in - let f_then = - match f_then with + let as_field fopt rng = + let unit_atomic_field = AtomicField (with_range (unit_atomic_field' rng) rng) in + let unit_field = with_range unit_atomic_field rng in + let fields = + match fopt with + | None -> [unit_field] + | Some fs -> fs + in + match fields with | [f] -> f - | _ -> with_range (RecordField(f_then, dummy_identifier)) ($startpos(f_then)) - in - let f_else = - match f_else with - | [f] -> f - | _ -> with_range (RecordField(f_else, dummy_identifier)) ($startpos(f_else)) + | _ -> with_range (RecordField(fields, dummy_identifier)) rng in + let f_then = as_field f_then ($startpos(f_then)) in + let f_else = as_field f_else ($startpos(f_else)) in let case_then = Case (tt, f_then) in let case_else = DefaultCase f_else in let e = with_range (Static e) ($startpos(e)) in SwitchCaseField ((e, [case_then; case_else]), dummy_identifier) } + +static_conditional_field: + | HASH_IF f=static_conditional_body + { f } field: - | f = atomic_field + | f = atomic_field SEMICOLON { let comms = Ast.comments_buffer.flush () in let range = (mk_pos $startpos, mk_pos $startpos) in @@ -313,14 +344,14 @@ field: with_range_and_comments (AtomicField af') range comms } - | rf = anonymous_struct_field + | rf = anonymous_struct_field SEMICOLON { let comms = Ast.comments_buffer.flush () in let range = (mk_pos $startpos, mk_pos $startpos) in with_range_and_comments rf range comms } - | cf = anonymous_casetype_field + | cf = anonymous_casetype_field SEMICOLON { let comms = Ast.comments_buffer.flush () in let range = (mk_pos $startpos, mk_pos $startpos) in @@ -335,7 +366,7 @@ field: } fields: - | fields=right_flexible_nonempty_list(SEMICOLON, field) + | fields=nonempty_list(field) { fields } immutable_parameter: @@ -361,7 +392,7 @@ case: | DEFAULT COLON f=field { DefaultCase f } cases: - | cs=right_flexible_nonempty_list(SEMICOLON, case) { cs } + | cs=nonempty_list(case) { cs } attribute: | ENTRYPOINT { Entrypoint } diff --git a/src/3d/tests/AnonNestedStruct.3d b/src/3d/tests/AnonNestedStruct.3d index d926e15f6..f0d64f0dc 100644 --- a/src/3d/tests/AnonNestedStruct.3d +++ b/src/3d/tests/AnonNestedStruct.3d @@ -28,12 +28,24 @@ typedef struct _TaggedPoint { entrypoint typedef struct _StaticConditionalPoint { - #if DIM2 - UINT32 x; - UINT32 y; - #else - UINT32 x; - UINT32 y; - UINT32 z; + UINT32 d1; + UINT32 d2; + #if (DIM3 || DIM4) + UINT32 d3; + #endif + #if DIM4 + UINT32 d4; #endif } StaticConditionalPoint; + +entrypoint +typedef struct _StaticConditionalPointAlt { + UINT32 d1; + UINT32 d2; + #if DIM3 + UINT32 d3; + #elif DIM4 + UINT32 d3; + UINT32 d4 { d3 <= d4 }; + #endif +} StaticConditionalPointAlt; diff --git a/src/3d/tests/CompileTimeIf.3d b/src/3d/tests/CompileTimeIf.3d index 82120563a..5704182a9 100644 --- a/src/3d/tests/CompileTimeIf.3d +++ b/src/3d/tests/CompileTimeIf.3d @@ -3,10 +3,12 @@ typedef struct _PointConditional { UINT32 x; UINT32 y { - #if (ABOVE_DIAGONAL && SOMETHING_ELSE) + #if (ABOVE_DIAGONAL && STRICT) + x < y + #elif ABOVE_DIAGONAL x <= y - #else - y <= x + #else + true #endif }; } PointConditional; From 5b282185369181ecf228982fa91f2d45c2493486 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 4 Oct 2022 00:21:42 +0000 Subject: [PATCH 06/12] parsing a JSON-formatted config file --- src/3d/Config.fst | 12 ++++++++++++ src/3d/Deps.fst | 23 +++++++++++++++++++++++ src/3d/Deps.fsti | 2 ++ src/3d/JSON.fsti | 2 ++ src/3d/Main.fst | 1 + src/3d/OS.fsti | 2 ++ src/3d/Options.fst | 4 ++++ src/3d/Options.fsti | 2 ++ src/3d/ocaml/JSON.ml | 13 +++++++++++++ src/3d/ocaml/OS.ml | 7 +++++++ 10 files changed, 68 insertions(+) create mode 100644 src/3d/Config.fst diff --git a/src/3d/Config.fst b/src/3d/Config.fst new file mode 100644 index 000000000..63638805c --- /dev/null +++ b/src/3d/Config.fst @@ -0,0 +1,12 @@ +module Config + +[@@ PpxDerivingYoJson] +type compile_time_flags = { + flags : list string; + include_file : string; +} + +[@@ PpxDerivingYoJson] +type config = { + compile_time_flags : compile_time_flags +} diff --git a/src/3d/Deps.fst b/src/3d/Deps.fst index 3aaae610a..d981002e2 100644 --- a/src/3d/Deps.fst +++ b/src/3d/Deps.fst @@ -291,3 +291,26 @@ let has_extern_types g m = List.Tot.mem m g.modules_with_extern_types let has_extern_functions g m = List.Tot.mem m g.modules_with_extern_functions +let get_config () = + match Options.get_config_file () with + | None -> None + | Some fn -> + if not (OS.file_exists fn) + then raise (Error ("Unable to file configuration file: " ^ fn)) + else + let s = + try OS.file_contents fn + with + | _ -> raise (Error ("Unable to read configuration file: "^fn)) + in + match JSON.config_of_json s with + | Pervasives.Inl c -> Some c + | Pervasives.Inr err -> + let msg = + Printf.sprintf "Unable to parse configuration: %s\n\ + A sample configuration is shown below:\n\ + %s" + err + (JSON.config_to_json { compile_time_flags = { flags = ["FLAG1"; "FLAG2"; "FLAG3"]; + include_file = "flags.h" }}) in + raise (Error msg) diff --git a/src/3d/Deps.fsti b/src/3d/Deps.fsti index 6a6e2c1aa..9991f7727 100644 --- a/src/3d/Deps.fsti +++ b/src/3d/Deps.fsti @@ -22,3 +22,5 @@ val has_output_types (g:dep_graph) (modul:string) : bool val has_extern_types (g:dep_graph) (modul:string) : bool val has_extern_functions (g:dep_graph) (modul:string) : bool + +val get_config (_:unit) : ML (option Config.config) diff --git a/src/3d/JSON.fsti b/src/3d/JSON.fsti index 75e25ec44..fe78af1b5 100644 --- a/src/3d/JSON.fsti +++ b/src/3d/JSON.fsti @@ -1,2 +1,4 @@ module JSON val prog_to_json (d:Ast.prog) : string +val config_to_json (c:Config.config) : string +val config_of_json (s:string) : either Config.config string diff --git a/src/3d/Main.fst b/src/3d/Main.fst index f3b47b7b3..f4e426405 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -398,6 +398,7 @@ let produce_and_postprocess_c let go () : ML unit = (* Parse command-line options. This action is only accumulating values into globals, without any further action (other than --help and --version, which interrupt the execution.) *) let cmd_line_files = Options.parse_cmd_line() in + let c = Deps.get_config () in (* Special mode: --check_inplace_hashes *) let inplace_hashes = Options.get_check_inplace_hashes () in if Cons? inplace_hashes diff --git a/src/3d/OS.fsti b/src/3d/OS.fsti index e7678df87..ef69db549 100644 --- a/src/3d/OS.fsti +++ b/src/3d/OS.fsti @@ -18,3 +18,5 @@ val extension: string -> Tot string val file_exists: string -> FStar.All.ML bool + +val file_contents: string -> FStar.All.ML string diff --git a/src/3d/Options.fst b/src/3d/Options.fst index a07e63da5..6d1cf5e39 100644 --- a/src/3d/Options.fst +++ b/src/3d/Options.fst @@ -25,6 +25,7 @@ let batch : ref bool = alloc false let clang_format : ref bool = alloc false let clang_format_executable : ref (option vstring) = alloc None let cleanup : ref bool = alloc false +let config_file : ref (option vstring) = alloc None let debug : ref bool = alloc false let inplace_hashes : ref (list vstring) = alloc [] let input_file : ref (list string) = alloc [] @@ -300,6 +301,7 @@ let (display_usage_2, compute_options_2, fstar_options) = CmdOption "clang_format" (OptBool clang_format) "Call clang-format on extracted .c/.h files (--batch only)" ["batch"]; CmdOption "clang_format_executable" (OptStringOption "clang-format full path" always_valid clang_format_executable) "Set the path to clang-format if not reachable through PATH" ["batch"; "clang_format"]; CmdOption "cleanup" (OptBool cleanup) "Remove *.fst*, *.krml and krml-args.rsp (--batch only)" []; + CmdOption "config" (OptStringOption "config file" always_valid config_file) "The name of a JSON formatted file containing configuration options" []; CmdOption "emit_output_types_defs" (OptBool emit_output_types_defs) "Emit definitions of output types in a .h file" []; CmdOption "input_stream" (OptStringOption "buffer|extern|static" valid_input_stream_binding input_stream_binding) "Input stream binding (default buffer)" []; CmdOption "input_stream_include" (OptStringOption ".h file" always_valid input_stream_include) "Include file defining the EverParseInputStreamBase type (only for --input_stream extern or static)" []; @@ -447,3 +449,5 @@ let get_input_stream_binding _ = InputStreamStatic (get_include ()) let get_emit_output_types_defs () = !emit_output_types_defs + +let get_config_file () = !config_file diff --git a/src/3d/Options.fsti b/src/3d/Options.fsti index fd97ca3b0..575070c32 100644 --- a/src/3d/Options.fsti +++ b/src/3d/Options.fsti @@ -53,3 +53,5 @@ val get_json : unit -> ML bool val get_input_stream_binding : unit -> ML input_stream_binding_t val get_emit_output_types_defs : unit -> ML bool + +val get_config_file : unit -> ML (option string) diff --git a/src/3d/ocaml/JSON.ml b/src/3d/ocaml/JSON.ml index ade571066..47aeb96b8 100644 --- a/src/3d/ocaml/JSON.ml +++ b/src/3d/ocaml/JSON.ml @@ -3,3 +3,16 @@ let prog_to_json (p:prog) : string = let yj = Ast.prog_to_yojson p in Yojson.Safe.to_string yj + +let config_to_json (c:Config.config) + : string + = let yj = Config.config_to_yojson c in + Yojson.Safe.to_string yj + +let config_of_json (s:string) + : (Config.config, string) FStar_Pervasives.either + = try + match Config.config_of_yojson (Yojson.Safe.from_string s) with + | Result.Ok c -> FStar_Pervasives.Inl c + | Result.Error s -> FStar_Pervasives.Inr s + with Yojson.Json_error msg -> FStar_Pervasives.Inr msg diff --git a/src/3d/ocaml/OS.ml b/src/3d/ocaml/OS.ml index 5095dc8eb..df8c396ac 100644 --- a/src/3d/ocaml/OS.ml +++ b/src/3d/ocaml/OS.ml @@ -113,3 +113,10 @@ let rename ol ne = let file_exists s = Sys.file_exists s + +let file_contents f = + let ic = open_in_bin f in + let l = in_channel_length ic in + let s = really_input_string ic l in + close_in ic; + s From b6235c10b289f22f02be549e2b9d86d6094ef537 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 4 Oct 2022 21:51:20 +0000 Subject: [PATCH 07/12] support for compile-time flags specified in a separate config file, with both makefile and batch mode support --- src/3d/Ast.fst | 5 +- src/3d/Binding.fst | 20 ++-- src/3d/Config.fst | 11 ++- src/3d/Deps.fst | 22 ++++- src/3d/Deps.fsti | 2 +- src/3d/Desugar.fst | 51 +++++----- src/3d/GenMakefile.fst | 74 +++++++++++---- src/3d/GlobalEnv.fst | 1 + src/3d/HashingOptions.fst | 3 +- src/3d/InlineSingletonRecords.fst | 3 +- src/3d/Main.fst | 25 ++++- src/3d/Options.fst | 48 ++++++++-- src/3d/Options.fsti | 2 + src/3d/Simplify.fst | 2 - src/3d/TranslateForInterpreter.fst | 4 - src/3d/TypeSizes.fst | 3 +- src/3d/ocaml/Batch.ml | 40 ++++++-- src/3d/tests/Makefile | 5 +- src/3d/tests/ifdefs/.gitignore | 1 + src/3d/tests/ifdefs/Makefile | 94 +++++++++++++++++++ .../src/AnonNestedStructIfDefs.3d} | 0 .../tests/{ => ifdefs/src}/CompileTimeIf.3d | 0 .../ifdefs/src/CompileTimeIfFlags.3d.config | 6 ++ src/3d/tests/ifdefs/src/compile_time_flags.h | 8 ++ 24 files changed, 337 insertions(+), 93 deletions(-) create mode 100644 src/3d/tests/ifdefs/.gitignore create mode 100644 src/3d/tests/ifdefs/Makefile rename src/3d/tests/{AnonNestedStruct.3d => ifdefs/src/AnonNestedStructIfDefs.3d} (100%) rename src/3d/tests/{ => ifdefs/src}/CompileTimeIf.3d (100%) create mode 100644 src/3d/tests/ifdefs/src/CompileTimeIfFlags.3d.config create mode 100644 src/3d/tests/ifdefs/src/compile_time_flags.h diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst index 32de28d41..f68d5d62b 100644 --- a/src/3d/Ast.fst +++ b/src/3d/Ast.fst @@ -533,7 +533,6 @@ type decl' = | OutputType : out_typ -> decl' | ExternType : typedef_names -> decl' | ExternFn : ident -> typ -> list param -> decl' - | CompileTimeFlag : ident -> decl' [@@ PpxDerivingYoJson ] noeq @@ -754,8 +753,7 @@ let subst_decl' (s:subst) (d:decl') : ML decl' = CaseType names (subst_params s params) (subst_switch_case s cases) | OutputType _ | ExternType _ - | ExternFn _ _ _ - | CompileTimeFlag _ -> d + | ExternFn _ _ _ -> d let subst_decl (s:subst) (d:decl) : ML decl = decl_with_v d (subst_decl' s d.d_decl.v) (*** Printing the source AST; for debugging only **) @@ -1022,7 +1020,6 @@ let print_decl' (d:decl') : ML string = | OutputType out_t -> "Printing for output types is TBD" | ExternType _ -> "Printing for extern types is TBD" | ExternFn _ _ _ -> "Printing for extern functions is TBD" - | CompileTimeFlag i -> Printf.sprintf "[@@IfDef]val %s : bool" i.v.name let print_decl (d:decl) : ML string = match d.d_decl.comments with diff --git a/src/3d/Binding.fst b/src/3d/Binding.fst index 64be1f82f..008e3223c 100644 --- a/src/3d/Binding.fst +++ b/src/3d/Binding.fst @@ -78,7 +78,6 @@ let params_of_decl (d:decl) : list param = | OutputType _ -> [] | ExternType _ -> [] | ExternFn _ _ ps -> ps - | CompileTimeFlag _ -> [] let check_shadow (e:H.t ident' 'a) (i:ident) (r:range) = match H.try_find e i.v with @@ -1701,20 +1700,17 @@ let bind_decl (e:global_env) (d:decl) : ML decl = add_extern_fn e f d; d - | CompileTimeFlag i -> - let ms = nullary_macro tbool None in - add_global e i d (Inr ms); - d - let bind_decls (g:global_env) (p:list decl) : ML (list decl & global_env) = List.map (bind_decl g) p, g let initial_global_env () = + let cfg = Deps.get_config () in let e = { ge_h = H.create 10; ge_out_t = H.create 10; ge_extern_t = H.create 10; ge_extern_fn = H.create 10; + ge_cfg = cfg } in let nullary_decl i = @@ -1760,6 +1756,18 @@ let initial_global_env () = typedef_attributes = [] })) dummy_range [] false) in + let _ = + match cfg with + | None -> () + | Some (cfg, module_name) -> + List.iter + (fun flag -> + let ms = nullary_macro tbool None in + let i = with_dummy_range { to_ident' flag with modul_name = Some module_name } in + let d = mk_decl (ExternFn i tbool []) dummy_range [] false in + add_global e i d (Inr ms)) + cfg.compile_time_flags.flags + in e let get_exported_decls ge mname = diff --git a/src/3d/Config.fst b/src/3d/Config.fst index 63638805c..dbb98e883 100644 --- a/src/3d/Config.fst +++ b/src/3d/Config.fst @@ -1,5 +1,5 @@ module Config - +module O = Options [@@ PpxDerivingYoJson] type compile_time_flags = { flags : list string; @@ -10,3 +10,12 @@ type compile_time_flags = { type config = { compile_time_flags : compile_time_flags } + +let emit_config_as_fstar_module (module_name:string) (c:config) = + let flags = + List.map + (Printf.sprintf "[@@ CIfDef]\nassume\nval ___%s : bool" ) + c.compile_time_flags.flags + in + let assumes = String.concat "\n\n" flags in + Printf.sprintf "module %s\n%s\n" module_name assumes diff --git a/src/3d/Deps.fst b/src/3d/Deps.fst index d981002e2..491088e0a 100644 --- a/src/3d/Deps.fst +++ b/src/3d/Deps.fst @@ -193,7 +193,6 @@ let scan_deps (fn:string) : ML scan_deps_t = | OutputType _ | ExternType _ | ExternFn _ _ _ -> [] //AR: no dependencies from the output/extern types yet - | CompileTimeFlag _ -> [] in let has_output_types (ds:list decl) : bool = @@ -291,11 +290,18 @@ let has_extern_types g m = List.Tot.mem m g.modules_with_extern_types let has_extern_functions g m = List.Tot.mem m g.modules_with_extern_functions -let get_config () = + +#push-options "--warn_error -272" +let parsed_config : ref (option (Config.config & string)) = ST.alloc None +#pop-options + +let parse_config () = match Options.get_config_file () with | None -> None | Some fn -> - if not (OS.file_exists fn) + let module_name = Options.config_module_name () in + if None? module_name then failwith "Impossible" + else if not (OS.file_exists fn) then raise (Error ("Unable to file configuration file: " ^ fn)) else let s = @@ -304,7 +310,7 @@ let get_config () = | _ -> raise (Error ("Unable to read configuration file: "^fn)) in match JSON.config_of_json s with - | Pervasives.Inl c -> Some c + | Pervasives.Inl c -> Some (c, Some?.v module_name) | Pervasives.Inr err -> let msg = Printf.sprintf "Unable to parse configuration: %s\n\ @@ -314,3 +320,11 @@ let get_config () = (JSON.config_to_json { compile_time_flags = { flags = ["FLAG1"; "FLAG2"; "FLAG3"]; include_file = "flags.h" }}) in raise (Error msg) + +let get_config () = + match !parsed_config with + | Some c -> Some c + | None -> + let copt = parse_config () in + parsed_config := copt; + copt diff --git a/src/3d/Deps.fsti b/src/3d/Deps.fsti index 9991f7727..249d091f2 100644 --- a/src/3d/Deps.fsti +++ b/src/3d/Deps.fsti @@ -23,4 +23,4 @@ val has_extern_types (g:dep_graph) (modul:string) : bool val has_extern_functions (g:dep_graph) (modul:string) : bool -val get_config (_:unit) : ML (option Config.config) +val get_config (_:unit) : ML (option (Config.config & string)) diff --git a/src/3d/Desugar.fst b/src/3d/Desugar.fst index 48440790a..760a70424 100644 --- a/src/3d/Desugar.fst +++ b/src/3d/Desugar.fst @@ -36,10 +36,6 @@ module H = Hashtable and removes the Static *) -#push-options "--warn_error -272" //intentional top-level effect -let auxiliary_decls : ref (list decl) = FStar.ST.alloc [] -#pop-options - let check_desugared_enum_cases (cases:list enum_case) : ML (list ident) = List.map (function @@ -176,6 +172,18 @@ let prim_consts = [ "void" ] let resolve_ident (env:qenv) (i:ident) : ML ident = + let resolve_to_current_module i = + { i with v = { i.v with modul_name = Some env.mname } } + in + let maybe_resolve_as_ifdef i + : ML ident + = match env.global_env.ge_cfg with + | None -> resolve_to_current_module i + | Some (cfg, cfg_module_name) -> + if List.mem i.v.name cfg.compile_time_flags.flags + then { i with v = { i.v with modul_name = Some cfg_module_name } } + else resolve_to_current_module i + in if List.mem i.v.name prim_consts //it's a primitive constant, e.g. UINT8, leave as is then i else if List.mem i.v.name env.local_names //it's a local name (e.g. a parameter name) @@ -187,7 +195,7 @@ let resolve_ident (env:qenv) (i:ident) : ML ident = i.range else i) //return the local name as is else (match i.v.modul_name with //it's a top-level name - | None -> { i with v = { i.v with modul_name = Some env.mname } } //if unqualified, add current module + | None -> maybe_resolve_as_ifdef i | Some m -> //if already qualified, check if it is an abbreviation (match H.try_find env.module_abbrevs m with | None -> i @@ -196,30 +204,20 @@ let resolve_ident (env:qenv) (i:ident) : ML ident = let rec collect_ifdef_guards (env:qenv) (e:expr) : ML unit - = match e.v with + = let check_resolved_to_ifdef i = + match env.global_env.ge_cfg with + | None -> false + | Some (cfg, cfg_module_name) -> + List.mem i.v.name cfg.compile_time_flags.flags + && i.v.modul_name = Some cfg_module_name + in + match e.v with | This -> error "'this' is not allowed in the guard of an #if" e.range | Static _ -> failwith "static should have been eliminated already" | Constant _ -> () | Identifier i -> - if List.mem i.v.name env.local_names //it's a local name (e.g. a parameter name) + if not (check_resolved_to_ifdef i) then error (Printf.sprintf "Identifier %s is not a compile-time macro but is used in a #if" i.v.name) e.range - else ( - //declare ident, if not already declared - let aux = !auxiliary_decls in - match List.tryFind - (fun d -> - match d.d_decl.v with - | CompileTimeFlag j -> i.v.name = j.v.name - | _ -> false) - aux - with - | None -> - IO.print_string (Printf.sprintf "Adding declaration of %s\n" i.v.name); - let d = mk_decl (CompileTimeFlag i) e.range [] false in - auxiliary_decls := d :: aux - | Some _ -> () //already declared - - ) | App op args -> begin match op with @@ -421,12 +419,10 @@ let resolve_decl' (env:qenv) (d:decl') : ML decl' = let ret = resolve_typ env ret in let params, _ = resolve_params env params in ExternFn id ret params - | CompileTimeFlag i -> d let resolve_decl (env:qenv) (d:decl) : ML decl = decl_with_v d (resolve_decl' env d.d_decl.v) let desugar (genv:GlobalEnv.global_env) (mname:string) (p:prog) : ML prog = - auxiliary_decls := []; let decls, refinement = p in let decls = List.collect desugar_one_enum decls in let env = { @@ -439,8 +435,7 @@ let desugar (genv:GlobalEnv.global_env) (mname:string) (p:prog) : ML prog = } in H.insert env.extern_types (Ast.to_ident' "void") (); let decls = List.map (resolve_decl env) decls in - let aux = List.rev (!auxiliary_decls) in - aux@decls, + decls, (match refinement with | None -> None | Some tr -> diff --git a/src/3d/GenMakefile.fst b/src/3d/GenMakefile.fst index f6c009e9b..17cac416a 100644 --- a/src/3d/GenMakefile.fst +++ b/src/3d/GenMakefile.fst @@ -47,6 +47,41 @@ let mk_filename : Tot string = output_dir `OS.concat` (Printf.sprintf "%s.%s" modul ext) +let add_cfg_file_dep ext deps + : FStar.All.ML (list string) + = match Options.config_module_name () with + | None -> deps + | Some module_name -> deps `List.Tot.append` [mk_filename module_name ext] + +let produce_config_fst_file_rule () +: FStar.All.ML (list rule_t) += match Options.config_module_name (), Options.get_config_file() with + | Some module_name, Some cfg_file_name -> + let fst_file_name = mk_filename module_name "fst" in + let checked_file_name = mk_filename module_name "fst.checked" in + let krml_file_name = mk_filename module_name "krml" in + let fst_rule = { + ty = EverParse; + from = [cfg_file_name]; + to = fst_file_name; + args = "--__micro_step emit_config" + } in + let fst_checked_rule = { + ty = EverParse; + from = [fst_file_name]; + to = checked_file_name; + args = Printf.sprintf "--__micro_step verify %s" fst_file_name; + } in + let krml_rule = { + ty = EverParse; + from = [checked_file_name]; + to = krml_file_name; + args = Printf.sprintf "--__micro_step extract %s" fst_file_name; + } in + [fst_rule; fst_checked_rule; krml_rule] + | _ -> [] + + let produce_external_api_fsti_checked_rule (g: Deps.dep_graph) (modul: string) @@ -78,11 +113,11 @@ let produce_fsti_checked_rule let produce_fst_checked_rule (g: Deps.dep_graph) (modul: string) -: Tot rule_t +: FStar.All.ML rule_t = let fst = mk_filename modul "fst" in { ty = EverParse; - from = fst :: mk_filename modul "fsti.checked" :: List.Tot.map (fun m -> mk_filename m "fsti.checked") (Deps.dependencies g modul); + from = add_cfg_file_dep "fst.checked" (fst :: mk_filename modul "fsti.checked" :: List.Tot.map (fun m -> mk_filename m "fsti.checked") (Deps.dependencies g modul)); to = mk_filename modul "fst.checked"; args = Printf.sprintf "--__micro_step verify %s" fst; } @@ -106,11 +141,13 @@ let produce_external_api_krml_rule let produce_krml_rule (g: Deps.dep_graph) (modul: string) -: Tot rule_t +: FStar.All.ML rule_t = { ty = EverParse; - from = mk_filename modul "fst.checked" :: List.Tot.map (fun m -> mk_filename m "fst.checked") (Deps.dependencies g modul); + from = add_cfg_file_dep "fst.checked" + (mk_filename modul "fst.checked" :: + List.Tot.map (fun m -> mk_filename m "fst.checked") (Deps.dependencies g modul)); to = mk_filename modul "krml"; args = Printf.sprintf "--__micro_step extract %s" (mk_filename modul "fst"); } @@ -194,16 +231,18 @@ let produce_h_rules { ty = EverParse; from = - (if clang_format then [mk_filename "" "clang-format"] else []) `List.Tot.append` - (if OS.file_exists (Printf.sprintf "%s.copyright.txt" file) then [copyright] else []) `List.Tot.append` - List.map (fun f -> mk_filename (Options.get_module_name f) "krml") all_files `List.Tot.append` - List.concatMap (fun f -> - let m = Options.get_module_name f in - if Deps.has_output_types g m || - Deps.has_extern_types g m || - Deps.has_extern_functions g m - then [mk_filename (Printf.sprintf "%s_ExternalAPI" m) "krml"] - else []) all_files + add_cfg_file_dep "krml" ( + (if clang_format then [mk_filename "" "clang-format"] else []) `List.Tot.append` + (if OS.file_exists (Printf.sprintf "%s.copyright.txt" file) then [copyright] else []) `List.Tot.append` + List.map (fun f -> mk_filename (Options.get_module_name f) "krml") all_files `List.Tot.append` + List.concatMap (fun f -> + let m = Options.get_module_name f in + if Deps.has_output_types g m || + Deps.has_extern_types g m || + Deps.has_extern_functions g m + then [mk_filename (Printf.sprintf "%s_ExternalAPI" m) "krml"] + else []) all_files + ) ; to = to; (* IMPORTANT: relies on the fact that KaRaMeL generates .c files BEFORE .h files *) args = Printf.sprintf "--__produce_c_from_existing_krml %s" (mk_input_filename file); @@ -315,10 +354,11 @@ let produce_makefile List.concatMap (produce_fst_rules g clang_format) all_files `List.Tot.append` List.concatMap (produce_external_api_fsti_checked_rule g) all_modules `List.Tot.append` List.Tot.map (produce_fsti_checked_rule g) all_modules `List.Tot.append` - List.Tot.map (produce_fst_checked_rule g) all_modules `List.Tot.append` + List.map (produce_fst_checked_rule g) all_modules `List.Tot.append` List.Tot.concatMap (produce_external_api_krml_rule g) all_modules `List.Tot.append` - List.Tot.map (produce_krml_rule g) all_modules `List.Tot.append` - List.concatMap (produce_h_rules g clang_format) all_files + List.map (produce_krml_rule g) all_modules `List.Tot.append` + List.concatMap (produce_h_rules g clang_format) all_files `List.Tot.append` + produce_config_fst_file_rule () in { graph = g; rules = rules; diff --git a/src/3d/GlobalEnv.fst b/src/3d/GlobalEnv.fst index c9775b5ae..87ee9d310 100755 --- a/src/3d/GlobalEnv.fst +++ b/src/3d/GlobalEnv.fst @@ -75,4 +75,5 @@ type global_env = { ge_out_t: H.t ident' decl; //a table for output types declarations ge_extern_t: H.t ident' decl; //a table for extern type declarations ge_extern_fn: H.t ident' decl; //a table for extern function declarations + ge_cfg: option (Config.config & string) } diff --git a/src/3d/HashingOptions.fst b/src/3d/HashingOptions.fst index f3e3a5d77..8618d1d06 100644 --- a/src/3d/HashingOptions.fst +++ b/src/3d/HashingOptions.fst @@ -11,7 +11,8 @@ type micro_step_t = | MicroStepVerify | MicroStepExtract | MicroStepCopyClangFormat - + | MicroStepEmitConfig + type makefile_type = | MakefileGMake | MakefileNMake diff --git a/src/3d/InlineSingletonRecords.fst b/src/3d/InlineSingletonRecords.fst index f2a93d92d..f2f7fad2d 100644 --- a/src/3d/InlineSingletonRecords.fst +++ b/src/3d/InlineSingletonRecords.fst @@ -202,8 +202,7 @@ let simplify_decl (env:env) (d:decl) : ML decl = | OutputType _ | ExternType _ - | ExternFn _ _ _ - | CompileTimeFlag _ -> d + | ExternFn _ _ _ -> d let simplify_prog (p:list decl) = let env = H.create 10 in diff --git a/src/3d/Main.fst b/src/3d/Main.fst index b2b7deb5d..588dcd8c9 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -362,6 +362,20 @@ let process_file (en:env) en.translate_env; } +let emit_config_as_fstar_module () + : ML unit + = match Deps.get_config () with + | None -> raise (Error ("'--__micro_step emitconfig' expects the '--config' option to also be set")) + | Some (cfg, config_module_name) -> + let fst_file_contents = Config.emit_config_as_fstar_module config_module_name cfg in + let fst_file = + open_write_file + (Printf.sprintf "%s/%s.fst" + (Options.get_output_dir()) + config_module_name) in + FStar.IO.write_string fst_file fst_file_contents; + FStar.IO.close_write_file fst_file + let process_files (files_and_modules:list (string & string)) (emit_fstar:string -> ML bool) (emit_output_types_defs:bool) @@ -372,11 +386,12 @@ let process_files (files_and_modules:list (string & string)) (List.map fst files_and_modules |> String.concat " ")); let all_modules = List.map snd files_and_modules in let env = initial_env () in + if Options.get_batch() then emit_config_as_fstar_module(); files_and_modules |> List.fold_left (fun env (fn, modul) -> process_file env fn modul (emit_fstar modul) emit_output_types_defs all_modules) env |> ignore - + let produce_and_postprocess_c (out_dir: string) (file: string) @@ -399,13 +414,19 @@ let produce_and_postprocess_c let go () : ML unit = (* Parse command-line options. This action is only accumulating values into globals, without any further action (other than --help and --version, which interrupt the execution.) *) let cmd_line_files = Options.parse_cmd_line() in - let c = Deps.get_config () in + let cfg_opt = Deps.get_config () in (* Special mode: --check_inplace_hashes *) let inplace_hashes = Options.get_check_inplace_hashes () in if Cons? inplace_hashes then Batch.check_inplace_hashes inplace_hashes else let micro_step = Options.get_micro_step () in + if micro_step = Some HashingOptions.MicroStepEmitConfig + then ( + emit_config_as_fstar_module (); + exit 0 + ) + else if micro_step = Some HashingOptions.MicroStepCopyClangFormat then (* Special mode: --__micro_step copy_clang_format *) diff --git a/src/3d/Options.fst b/src/3d/Options.fst index 1d1c612ea..5ba74ff77 100644 --- a/src/3d/Options.fst +++ b/src/3d/Options.fst @@ -15,6 +15,30 @@ let valid_string let always_valid (_: string) : Tot bool = true +let starts_with_capital (s: string) : Tot bool = + String.length s >= 1 && + begin let first = String.sub s 0 1 in + String.compare first "A" >= 0 && String.compare first "Z" <= 0 + end + +let ends_with (s:string) (suffix:string) : bool = + let l = String.length s in + let sl = String.length suffix in + if sl > l || sl = 0 + then false + else let suffix' = String.sub s (l - sl) sl in + suffix = suffix' + +let check_config_file_name (fn:string) + : bool + = let fn = OS.basename fn in + starts_with_capital fn && + ends_with fn ".3d.config" + +let strip_suffix (fn:string) (sfx:string { ends_with fn sfx }) + : string + = String.sub fn 0 (String.length fn - String.length sfx) + inline_for_extraction let vstring = valid_string always_valid @@ -25,7 +49,7 @@ let batch : ref bool = alloc false let clang_format : ref bool = alloc false let clang_format_executable : ref (option vstring) = alloc None let cleanup : ref bool = alloc false -let config_file : ref (option vstring) = alloc None +let config_file : ref (option (valid_string check_config_file_name)) = alloc None let debug : ref bool = alloc false let inplace_hashes : ref (list vstring) = alloc [] let input_file : ref (list string) = alloc [] @@ -41,6 +65,7 @@ let valid_micro_step (str: string) : Tot bool = match str with | "verify" | "extract" | "copy_clang_format" + | "emit_config" -> true | _ -> false @@ -301,7 +326,7 @@ let (display_usage_2, compute_options_2, fstar_options) = CmdOption "clang_format" (OptBool clang_format) "Call clang-format on extracted .c/.h files (--batch only)" ["batch"]; CmdOption "clang_format_executable" (OptStringOption "clang-format full path" always_valid clang_format_executable) "Set the path to clang-format if not reachable through PATH" ["batch"; "clang_format"]; CmdOption "cleanup" (OptBool cleanup) "Remove *.fst*, *.krml and krml-args.rsp (--batch only)" []; - CmdOption "config" (OptStringOption "config file" always_valid config_file) "The name of a JSON formatted file containing configuration options" []; + CmdOption "config" (OptStringOption "config file" check_config_file_name config_file) "The name of a JSON formatted file containing configuration options" []; CmdOption "emit_output_types_defs" (OptBool emit_output_types_defs) "Emit definitions of output types in a .h file" []; CmdOption "input_stream" (OptStringOption "buffer|extern|static" valid_input_stream_binding input_stream_binding) "Input stream binding (default buffer)" []; CmdOption "input_stream_include" (OptStringOption ".h file" always_valid input_stream_include) "Include file defining the EverParseInputStreamBase type (only for --input_stream extern or static)" []; @@ -318,7 +343,7 @@ let (display_usage_2, compute_options_2, fstar_options) = CmdFStarOption (let open FStar.Getopt in noshort, "version", ZeroArgs (fun _ -> FStar.IO.print_string (Printf.sprintf "EverParse/3d %s\nCopyright 2018, 2019, 2020 Microsoft Corporation\n" Version.everparse_version); exit 0), "Show this version of EverParse"); CmdOption "equate_types" (OptList "an argument of the form A,B, to generate asserts of the form (A.t == B.t)" valid_equate_types equate_types_list) "Takes an argument of the form A,B and then for each entrypoint definition in B, it generates an assert (A.t == B.t) in the B.Types file, useful when refactoring specs, you can provide multiple equate_types on the command line" []; CmdOption "__arg0" (OptStringOption "executable name" always_valid arg0) "executable name to use for the help message" []; - CmdOption "__micro_step" (OptStringOption "verify|extract" valid_micro_step micro_step) "micro step" []; + CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|emit_config" valid_micro_step micro_step) "micro step" []; CmdOption "__produce_c_from_existing_krml" (OptBool produce_c_from_existing_krml) "produce C from .krml files" []; CmdOption "__skip_deps" (OptBool skip_deps) "skip dependency analysis, assume all dependencies are specified on the command line" []; ]; @@ -348,12 +373,6 @@ let split_3d_file_name fn = let get_file_name mname = mname ^ ".3d" -let starts_with_capital (s: string) : Tot bool = - String.length s >= 1 && - begin let first = String.sub s 0 1 in - String.compare first "A" >= 0 && String.compare first "Z" <= 0 - end - let get_module_name (file: string) = match split_3d_file_name file with | Some nm -> @@ -419,6 +438,7 @@ let get_micro_step _ = | Some "verify" -> Some MicroStepVerify | Some "extract" -> Some MicroStepExtract | Some "copy_clang_format" -> Some MicroStepCopyClangFormat + | Some "emit_config" -> Some MicroStepEmitConfig let get_produce_c_from_existing_krml _ = !produce_c_from_existing_krml @@ -459,4 +479,12 @@ let get_input_stream_binding _ = let get_emit_output_types_defs () = !emit_output_types_defs -let get_config_file () = !config_file +let get_config_file () = + match !config_file with + | None -> None + | Some s -> Some s + +let config_module_name () = + match !config_file with + | None -> None + | Some s -> Some (strip_suffix (OS.basename s) ".3d.config") diff --git a/src/3d/Options.fsti b/src/3d/Options.fsti index 575070c32..24b93d1ff 100644 --- a/src/3d/Options.fsti +++ b/src/3d/Options.fsti @@ -55,3 +55,5 @@ val get_input_stream_binding : unit -> ML input_stream_binding_t val get_emit_output_types_defs : unit -> ML bool val get_config_file : unit -> ML (option string) + +val config_module_name : unit -> ML (option string) diff --git a/src/3d/Simplify.fst b/src/3d/Simplify.fst index ab3a1f73d..cfeb85df0 100644 --- a/src/3d/Simplify.fst +++ b/src/3d/Simplify.fst @@ -190,8 +190,6 @@ let simplify_decl (env:T.env_t) (d:decl) : ML decl = let ret = simplify_typ env ret in let params = List.map (fun (t, i, q) -> simplify_typ env t, i, q) params in decl_with_v d (ExternFn f ret params) - - | CompileTimeFlag i -> d let simplify_prog benv senv (p:list decl) = diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index f6ad4ca2a..0dd464f9e 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -1410,10 +1410,6 @@ let translate_decl (env:global_env) (d:A.decl) : ML (list T.decl) = params@[i, t],ds@ds_t) ([], ds) params in ds @ [with_comments (T.Extern_fn f ret params) false []] - | CompileTimeFlag i -> - let t, ds_t = translate_typ tbool in - ds_t @ [with_attrs (T.Assumption (i, t)) false true false false []] - noeq type translate_env = { t_has_reader: H.t ident' bool; diff --git a/src/3d/TypeSizes.fst b/src/3d/TypeSizes.fst index 515a53b22..a3b4a9437 100644 --- a/src/3d/TypeSizes.fst +++ b/src/3d/TypeSizes.fst @@ -428,8 +428,7 @@ let decl_size_with_alignment (env:env_t) (d:decl) | OutputType _ | ExternType _ - | ExternFn _ _ _ - | CompileTimeFlag _ -> d + | ExternFn _ _ _ -> d let size_of_decls (genv:B.global_env) (senv:size_env) (ds:list decl) = let env = diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml index 4ab954e49..67b9b4460 100644 --- a/src/3d/ocaml/Batch.ml +++ b/src/3d/ocaml/Batch.ml @@ -155,10 +155,18 @@ let verify_and_extract_module let fsti_file = Printf.sprintf "%si" fst_file in - let all_files = List.filter file_exists [external_api_fsti_file; types_fst_file; fsti_file; fst_file] in - let all_extract_files = List.filter file_exists [external_api_fsti_file; types_fst_file; fst_file] in - List.iter (verify_fst_file input_stream_binding out_dir) all_files; - List.iter (extract_fst_file input_stream_binding out_dir) all_extract_files + let all_files = [external_api_fsti_file; types_fst_file; fsti_file; fst_file] in + let all_extract_files = [external_api_fsti_file; types_fst_file; fst_file] in + let all_files, all_extract_files = + match Deps.get_config () with + | None -> all_files, all_extract_files + | Some (_, module_name) -> + let cfg_fst_name = filename_concat out_dir (Printf.sprintf "%s.fst" module_name) in + cfg_fst_name::all_files, + cfg_fst_name::all_extract_files + in + List.iter (verify_fst_file input_stream_binding out_dir) (List.filter file_exists all_files); + List.iter (extract_fst_file input_stream_binding out_dir) (List.filter file_exists all_extract_files) let is_krml filename @@ -271,6 +279,11 @@ let krml_args input_stream_binding skip_c_makefiles out_dir files_and_modules = (all_everparse_krmls input_stream_binding) files_and_modules in + let krml_files = + match Options.config_module_name () with + | None -> krml_files + | Some m -> filename_concat out_dir (Printf.sprintf "%s.krml" m) :: krml_files + in let external_api_lib_args = List.fold_left (fun accu (_, modul) -> accu @ (external_api_lib_args modul)) [] files_and_modules in let external_api_no_prefix_args = List.fold_left (fun accu (_, modul) -> @@ -296,16 +309,27 @@ let krml_args input_stream_binding skip_c_makefiles out_dir files_and_modules = "-add-include" :: "\"EverParse.h\"" :: "-fextern-c" :: external_api_lib_args @ external_api_no_prefix_args @ external_typedefs_include_args @ krml_args0 @ krml_files - in - let input_stream_include = HashingOptions.input_stream_include input_stream_binding in - let krml_args = + in + let input_stream_include = HashingOptions.input_stream_include input_stream_binding in + let krml_args = if input_stream_include = "" then krml_args else "-add-include" :: Printf.sprintf "\"%s\"" input_stream_include :: krml_args - in + in + let krml_args = if skip_c_makefiles then "-skip-makefiles" :: krml_args else krml_args + in + let krml_args = + match Deps.get_config () with + | None -> krml_args + | Some (cfg, module_name) -> + let include_file = Printf.sprintf "\"%s\"" cfg.compile_time_flags.include_file in + "-no-prefix" :: module_name :: "-add-include" :: include_file :: krml_args + in + krml_args + let call_krml files_and_modules_cleanup out_dir krml_args = (* append the everparse and krmllib bundles to the list of arguments *) diff --git a/src/3d/tests/Makefile b/src/3d/tests/Makefile index e3438f59f..4911562b3 100644 --- a/src/3d/tests/Makefile +++ b/src/3d/tests/Makefile @@ -20,7 +20,7 @@ modules_static_assertions=TestFieldPtrStaticAssertions.c AlignStaticAssertions.c clean_out_files=$(addsuffix .c,$(modules_or_wrappers)) $(modules_static_assertions) $(addsuffix .h,$(modules_or_wrappers)) OTHER_HEADERS=TestFieldPtrBase.h AlignC.h -all: batch-test batch-test-negative batch-cleanup-test inplace-hash-test modules tcpip extern output-types batch-interpret-test modules-interpret elf-test static funptr +all: batch-test batch-test-negative batch-cleanup-test inplace-hash-test modules tcpip extern output-types batch-interpret-test modules-interpret elf-test static funptr ifdefs #AR: TODO: remove ELF.3d from here @@ -28,6 +28,9 @@ INTERPRETABLE_FILES=$(filter-out FAILNoEntrypoint.3d ELF.3d, $(wildcard *.3d)) INTERPRETABLE_MODULES=$(basename $(INTERPRETABLE_FILES)) interpret_all: $(addsuffix .interpret, $(INTERPRETABLE_MODULES)) +ifdefs: + +$(MAKE) -C ifdefs + extern: +$(MAKE) -C extern diff --git a/src/3d/tests/ifdefs/.gitignore b/src/3d/tests/ifdefs/.gitignore new file mode 100644 index 000000000..b672fdeaf --- /dev/null +++ b/src/3d/tests/ifdefs/.gitignore @@ -0,0 +1 @@ +obj diff --git a/src/3d/tests/ifdefs/Makefile b/src/3d/tests/ifdefs/Makefile new file mode 100644 index 000000000..645da6625 --- /dev/null +++ b/src/3d/tests/ifdefs/Makefile @@ -0,0 +1,94 @@ +# This Makefile is meant to be used with GNU Make. It builds EverParse +# validators and parsers corresponding to the data formats specified +# in src/*.3d files, as well as a test program to run them. + +# Default rule when `make` is run without argument. This rule MUST +# appear first, so we define it here and make it point to a `world` +# rule that will depend on variables defined in the +# EverParse-generated Makefile. +all: world + +######################################################## +# Variables needed by the EverParse-generated Makefile # +######################################################## + +# EVERPARSE_HOME: root of the EverParse tree (source tree or contents +# of the binary package.) +# EVERPARSE_HOME is necessary for the 3d executable. It needs to point to the +# root of the EverParse source tree. However, EVERPARSE_HOME is not needed if +# you run everparse.sh or everparse.cmd from the binary package. +EVERPARSE_HOME ?= $(realpath ../../../..) +export EVERPARSE_HOME + +# Command to run EverParse: path to either the 3d executable or the +# everparse.sh or everparse.cmd script from the EverParse binary +# package; followed by arguments +EVERPARSE_EXE=$(EVERPARSE_HOME)/bin/3d.exe +EVERPARSE_CMD=$(EVERPARSE_EXE) --config $(EVERPARSE_INPUT_DIR)/CompileTimeIfFlags.3d.config + +# Output directory for .c/.h files as well as temporary files (.fst, +# .krml, etc.) +EVERPARSE_OUTPUT_DIR=obj + +# Input directory containing .3d (and auxiliary .3d.copyright.txt) +# files +EVERPARSE_INPUT_DIR=src + +# If a .3d file contains a `refining` clause, then the C compiler must +# be given the include path that contains the .h files pointed to by +# such clauses. +CFLAGS += -I src + +######################################### +# Generating and including the Makefile # +######################################### + +# Define the name and path of the generated Makefile. We cleverly +# decide to have it generated into the output directory along with all +# temporary files. +everparse_makefile=$(EVERPARSE_OUTPUT_DIR)/EverParse.Makefile + +# Create the output directory if it does not exist +$(EVERPARSE_OUTPUT_DIR): + mkdir -p $@ + +# Generate the Makefile if any .3d file is modified +$(everparse_makefile): $(wildcard src/*.3d) $(EVERPARSE_OUTPUT_DIR) + $(EVERPARSE_CMD) --makefile gmake --makefile_name $@ $(wildcard $(EVERPARSE_INPUT_DIR)/*.3d) + +# Include the generated Makefile +include $(everparse_makefile) + +########### +# Cleanup # +########### + +# Since everything is output to the same directory, including the +# generated Makefile, it is enough to remove that directory. +clean: + rm -rf $(EVERPARSE_OUTPUT_DIR) + + +####################################################### +# Specifying the `world` rule run by the default rule # +####################################################### + +# Specify the behavior of the default rule +# excluding AnonNestedStructIfDefs.o for now, since we hit krml bug #293 +world: $(EVERPARSE_OUTPUT_DIR)/CompileTimeIf.o $(EVERPARSE_ALL_C_FILES) batch + +####################################################### +# Also test batch mode +####################################################### + +EVERPARSE_BATCH_OUTPUT_DIR=batch_obj + +$(EVERPARSE_BATCH_OUTPUT_DIR): + mkdir -p $@ + +batch: $(EVERPARSE_BATCH_OUTPUT_DIR) + $(EVERPARSE_CMD) --batch --odir $(EVERPARSE_BATCH_OUTPUT_DIR) $(wildcard $(EVERPARSE_INPUT_DIR)/*.3d) + +# Declare all phony rules. +# Cf. https://www.gnu.org/software/make/manual/html_node/Phony-Targets.html +.PHONY: all world test clean batch diff --git a/src/3d/tests/AnonNestedStruct.3d b/src/3d/tests/ifdefs/src/AnonNestedStructIfDefs.3d similarity index 100% rename from src/3d/tests/AnonNestedStruct.3d rename to src/3d/tests/ifdefs/src/AnonNestedStructIfDefs.3d diff --git a/src/3d/tests/CompileTimeIf.3d b/src/3d/tests/ifdefs/src/CompileTimeIf.3d similarity index 100% rename from src/3d/tests/CompileTimeIf.3d rename to src/3d/tests/ifdefs/src/CompileTimeIf.3d diff --git a/src/3d/tests/ifdefs/src/CompileTimeIfFlags.3d.config b/src/3d/tests/ifdefs/src/CompileTimeIfFlags.3d.config new file mode 100644 index 000000000..8e29f9464 --- /dev/null +++ b/src/3d/tests/ifdefs/src/CompileTimeIfFlags.3d.config @@ -0,0 +1,6 @@ +{ "compile_time_flags": + { + "flags":["ABOVE_DIAGONAL","STRICT","DIM3","DIM4"], + "include_file":"compile_time_flags.h" + } +} \ No newline at end of file diff --git a/src/3d/tests/ifdefs/src/compile_time_flags.h b/src/3d/tests/ifdefs/src/compile_time_flags.h new file mode 100644 index 000000000..fc4b278e1 --- /dev/null +++ b/src/3d/tests/ifdefs/src/compile_time_flags.h @@ -0,0 +1,8 @@ +#ifndef COMPILE_TIME_FLAGS_H + +#define COMPILE_TIME_FLAGS_H + +#define ABOVEDIAGONAL 1 +#define STRICT 0 + +#endif From edc712dc9f15c9c1f9d31a596b83f7d61ef99b23 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 5 Oct 2022 21:02:02 +0000 Subject: [PATCH 08/12] fix up syntax of some examples that miss semicolons on struct fields; fix grouping of fields; fix expected output in one case --- doc/3d-snapshot/TaggedUnion.c | 8 ++--- doc/BF.3d | 2 +- src/3d/Ast.fst | 12 +++++++ src/3d/Main.fst | 2 +- src/3d/TranslateForInterpreter.fst | 41 ++++++++++++---------- src/3d/ocaml/parser.mly | 19 ++-------- src/3d/tests/Arithmetic.3d | 6 ++-- src/3d/tests/Bitfields0.3d | 2 +- src/3d/tests/ELF.3d | 4 +-- src/3d/tests/Test_Synthetic1.3d | 2 +- src/3d/tests/modules-interpret/src/Test.3d | 2 +- src/3d/tests/modules/src/Test.3d | 2 +- src/3d/tests/output_types/TPoint.3d | 2 +- src/3d/tests/tcpip/TCP.3d | 6 ++-- 14 files changed, 58 insertions(+), 52 deletions(-) diff --git a/doc/3d-snapshot/TaggedUnion.c b/doc/3d-snapshot/TaggedUnion.c index de2fd0c7a..834710564 100644 --- a/doc/3d-snapshot/TaggedUnion.c +++ b/doc/3d-snapshot/TaggedUnion.c @@ -44,7 +44,7 @@ ValidateIntPayload( return positionAfterIntPayload; } Err("_int_payload", - "missing", + "value8", EverParseErrorReasonOfResult(positionAfterIntPayload), EverParseGetValidatorErrorKind(positionAfterIntPayload), Ctxt, @@ -73,7 +73,7 @@ ValidateIntPayload( return positionAfterIntPayload; } Err("_int_payload", - "missing", + "value16", EverParseErrorReasonOfResult(positionAfterIntPayload), EverParseGetValidatorErrorKind(positionAfterIntPayload), Ctxt, @@ -102,7 +102,7 @@ ValidateIntPayload( return positionAfterIntPayload; } Err("_int_payload", - "missing", + "value32", EverParseErrorReasonOfResult(positionAfterIntPayload), EverParseGetValidatorErrorKind(positionAfterIntPayload), Ctxt, @@ -119,7 +119,7 @@ ValidateIntPayload( return positionAfterIntPayload; } Err("_int_payload", - "missing", + "_x_2", EverParseErrorReasonOfResult(positionAfterIntPayload), EverParseGetValidatorErrorKind(positionAfterIntPayload), Ctxt, diff --git a/doc/BF.3d b/doc/BF.3d index 5466685af..0d0743a17 100644 --- a/doc/BF.3d +++ b/doc/BF.3d @@ -2,7 +2,7 @@ typedef struct _BF { UINT32 x : 6; UINT32 y : 10 { y <= 900 }; - UINT32 z : 16 { y + z <= 60000 } + UINT32 z : 16 { y + z <= 60000 }; } BF; // SNIPPET_END: BF diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst index f68d5d62b..9fceb8731 100644 --- a/src/3d/Ast.fst +++ b/src/3d/Ast.fst @@ -651,6 +651,18 @@ let tuint16 = mk_prim_t "UINT16" let tuint32 = mk_prim_t "UINT32" let tuint64 = mk_prim_t "UINT64" let tunknown = mk_prim_t "?" +let unit_atomic_field rng = + let dummy_identifier = with_range (to_ident' "_empty_") rng in + let f = { + field_dependence=false; + field_ident=dummy_identifier; + field_type=tunit; + field_array_opt=FieldScalar; + field_constraint=None; + field_bitwidth=None; + field_action=None + } in + with_range f rng let map_opt (f:'a -> ML 'b) (o:option 'a) : ML (option 'b) = match o with diff --git a/src/3d/Main.fst b/src/3d/Main.fst index 588dcd8c9..e4afed33c 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -365,7 +365,7 @@ let process_file (en:env) let emit_config_as_fstar_module () : ML unit = match Deps.get_config () with - | None -> raise (Error ("'--__micro_step emitconfig' expects the '--config' option to also be set")) + | _ -> () | Some (cfg, config_module_name) -> let fst_file_contents = Config.emit_config_as_fstar_module config_module_name cfg in let fst_file = diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index 0dd464f9e..08e19eb44 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/src/3d/TranslateForInterpreter.fst @@ -924,11 +924,11 @@ let translate_atomic_field (f:A.atomic_field) : ML (T.struct_field & T.decls) = noeq type grouped_fields = - | Empty_grouped_field + // | Empty_grouped_field | DependentField : hd:T.field -> tl:grouped_fields -> grouped_fields - | NonDependentField : hd:T.field -> tl:grouped_fields -> grouped_fields + | NonDependentField : hd:T.field -> tl:option grouped_fields -> grouped_fields | ITEGroup : e:T.expr -> then_:grouped_fields -> else_:grouped_fields -> grouped_fields - | GroupThen : id:A.ident -> struct:grouped_fields -> rest:grouped_fields -> grouped_fields + | GroupThen : id:A.ident -> struct:grouped_fields -> rest:option grouped_fields -> grouped_fields let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields) : ML T.parser @@ -936,9 +936,8 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields let parse_typ (fieldname:A.ident) = parse_typ env typename Ast.(fieldname.v.name) in let rec aux (gfs:grouped_fields) : ML parser = match gfs with - | Empty_grouped_field -> - failwith "Unexpected empty list of fields" - + // | Empty_grouped_field -> + // failwith "Unexpected empty list of fields" | DependentField sf gfs -> //This a dependent pair, gfs cannot be empty let get_action = function @@ -983,10 +982,10 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields | NonDependentField sf rest -> ( match rest with - | Empty_grouped_field -> + | None -> parse_typ sf.sf_ident sf.sf_typ - | _ -> + | Some rest -> pair_parser sf.sf_ident (parse_typ sf.sf_ident sf.sf_typ) (aux rest) @@ -1000,10 +999,10 @@ let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields | GroupThen id gfs rest -> ( match rest with - | Empty_grouped_field -> + | None -> aux gfs - | _ -> + | Some rest -> pair_parser id (aux gfs) (aux rest) @@ -1235,25 +1234,31 @@ let rec field_as_grouped_fields (f:A.field) = match f.v with | AtomicField af -> let sf, ds = translate_atomic_field af in - sf.sf_ident, NonDependentField sf Empty_grouped_field, ds + sf.sf_ident, NonDependentField sf None, ds | RecordField fs field_name -> let gfs, ds = - List.fold_right + List.fold_right #_ #(option grouped_fields & T.decls) (fun f (gfs, ds_out) -> match f.v with | AtomicField af -> let sf, ds = translate_atomic_field af in - if sf.sf_dependence - then DependentField sf gfs, ds@ds_out - else NonDependentField sf gfs, ds@ds_out + if sf.sf_dependence && Some? gfs + then Some (DependentField sf (Some?.v gfs)), ds@ds_out + else Some (NonDependentField sf gfs), ds@ds_out | RecordField _ _ | SwitchCaseField _ _ -> let id, gf, ds = field_as_grouped_fields f in - GroupThen id gf gfs, ds@ds_out) + Some (GroupThen id gf gfs), ds@ds_out) fs - (Empty_grouped_field, []) + (None, []) + in + let gfs, ds = + if None? gfs + then let sf, ds' = translate_atomic_field (unit_atomic_field f.range) in + NonDependentField sf None, ds@ds' + else Some?.v gfs, ds in field_name, gfs, ds @@ -1265,7 +1270,7 @@ let rec field_as_grouped_fields (f:A.field) T.( { sf_typ = T.T_false; sf_ident = gen_ident None; sf_dependence = false } ) - Empty_grouped_field + None in let rest, default_group, decls = if List.length cases > 0 diff --git a/src/3d/ocaml/parser.mly b/src/3d/ocaml/parser.mly index 773a4c764..adcd18776 100644 --- a/src/3d/ocaml/parser.mly +++ b/src/3d/ocaml/parser.mly @@ -44,18 +44,6 @@ out_expr_meta = None } - let unit_atomic_field' rng = - let dummy_identifier = with_range (to_ident' "_empty_") rng in - { - field_dependence=false; - field_ident=dummy_identifier; - field_type=tunit; - field_array_opt=FieldScalar; - field_constraint=None; - field_bitwidth=None; - field_action=None - } - %} @@ -311,9 +299,8 @@ static_conditional_body: { let tt = with_range (Constant (Bool true)) ($startpos(e)) in let dummy_identifier = with_range (to_ident' "_") ($startpos(e)) in - let as_field fopt rng = - let unit_atomic_field = AtomicField (with_range (unit_atomic_field' rng) rng) in - let unit_field = with_range unit_atomic_field rng in + let as_field fopt posn = + let unit_field = with_range (AtomicField (unit_atomic_field (mk_pos posn, mk_pos posn))) posn in let fields = match fopt with | None -> [unit_field] @@ -321,7 +308,7 @@ static_conditional_body: in match fields with | [f] -> f - | _ -> with_range (RecordField(fields, dummy_identifier)) rng + | _ -> with_range (RecordField(fields, dummy_identifier)) posn in let f_then = as_field f_then ($startpos(f_then)) in let f_else = as_field f_else ($startpos(f_else)) in diff --git a/src/3d/tests/Arithmetic.3d b/src/3d/tests/Arithmetic.3d index ee80a253f..6da1f2795 100644 --- a/src/3d/tests/Arithmetic.3d +++ b/src/3d/tests/Arithmetic.3d @@ -6,7 +6,7 @@ where param < 100uy { UINT8 field1 { field1 < param + 1uy }; UINT16 field2 { field2 < MAX_UINT16 - (UINT16)field1 }; - UINT32 field3 { field3 < 0xbeefbadd - (UINT32)field2 } + UINT32 field3 { field3 < 0xbeefbadd - (UINT32)field2 }; } Test; entrypoint @@ -15,7 +15,7 @@ where param < 100uy { UINT8 field1 { field1 < param + 1uy }; UINT16 field2 { field2 < MAX_UINT16 - field1 }; - UINT32 field3 { field3 < 0xbeefbadd - field2 } + UINT32 field3 { field3 < 0xbeefbadd - field2 }; } Test2; #define Case1 0x02 @@ -47,7 +47,7 @@ typedef struct _Test3 field3 == field2 / field1 || field3 == (UINT32)field2 * field1 || (field2 >= field1 && field3 == field2 - field1) - } + }; } Test3; // Check that all operators are translated as expected diff --git a/src/3d/tests/Bitfields0.3d b/src/3d/tests/Bitfields0.3d index 73b3780d5..abd95a930 100644 --- a/src/3d/tests/Bitfields0.3d +++ b/src/3d/tests/Bitfields0.3d @@ -1,7 +1,7 @@ typedef struct _BF { UINT32 x : 6; UINT32 y : 10 { y <= 900 }; - UINT32 z : 16 { y + z <= 60000 } + UINT32 z : 16 { y + z <= 60000 }; } BF, *PBF; entrypoint diff --git a/src/3d/tests/ELF.3d b/src/3d/tests/ELF.3d index 1c67155f4..98efef586 100644 --- a/src/3d/tests/ELF.3d +++ b/src/3d/tests/ELF.3d @@ -223,8 +223,8 @@ casetype _PROGRAM_HEADER_TABLE_OPT (UINT16 PhNum, case 0: unit Empty; default: - PROGRAM_HEADER_TABLE_ENTRY(ElfFileSize) Tbl[:byte-size sizeof (PROGRAM_HEADER_TABLE_ENTRY) * PhNum] - } + PROGRAM_HEADER_TABLE_ENTRY(ElfFileSize) Tbl[:byte-size sizeof (PROGRAM_HEADER_TABLE_ENTRY) * PhNum]; + } } PROGRAM_HEADER_TABLE_OPT; diff --git a/src/3d/tests/Test_Synthetic1.3d b/src/3d/tests/Test_Synthetic1.3d index f779de672..73c6ef9c9 100644 --- a/src/3d/tests/Test_Synthetic1.3d +++ b/src/3d/tests/Test_Synthetic1.3d @@ -50,7 +50,7 @@ typedef struct _STRUCT_3 (UINT32 TotalLen) offset >= sizeof(this) }; UINT32_Alias4 f4 { f4 == 0 }; - UINT8 buffer[TotalLen - sizeof(this)] + UINT8 buffer[TotalLen - sizeof(this)]; } STRUCT_3; diff --git a/src/3d/tests/modules-interpret/src/Test.3d b/src/3d/tests/modules-interpret/src/Test.3d index 607638844..67893a8a7 100644 --- a/src/3d/tests/modules-interpret/src/Test.3d +++ b/src/3d/tests/modules-interpret/src/Test.3d @@ -12,7 +12,7 @@ entrypoint typedef struct _T { CIRCLE c; UINT32 f1 { f1 == Constants::FIVE }; UINT32 f2 { f2 == Constants::Four }; - UINT32 f3 { f3 == TEST_ONE } + UINT32 f3 { f3 == TEST_ONE }; } T; refining "Foobar.h" { diff --git a/src/3d/tests/modules/src/Test.3d b/src/3d/tests/modules/src/Test.3d index 607638844..67893a8a7 100644 --- a/src/3d/tests/modules/src/Test.3d +++ b/src/3d/tests/modules/src/Test.3d @@ -12,7 +12,7 @@ entrypoint typedef struct _T { CIRCLE c; UINT32 f1 { f1 == Constants::FIVE }; UINT32 f2 { f2 == Constants::Four }; - UINT32 f3 { f3 == TEST_ONE } + UINT32 f3 { f3 == TEST_ONE }; } T; refining "Foobar.h" { diff --git a/src/3d/tests/output_types/TPoint.3d b/src/3d/tests/output_types/TPoint.3d index 445b9f9bd..c777062d9 100644 --- a/src/3d/tests/output_types/TPoint.3d +++ b/src/3d/tests/output_types/TPoint.3d @@ -20,7 +20,7 @@ typedef struct _POINT (mutable OPOINT* out) { {:on-success out->y = y; return true; - } + }; } POINT; entrypoint diff --git a/src/3d/tests/tcpip/TCP.3d b/src/3d/tests/tcpip/TCP.3d index 989d7b598..5846a8621 100644 --- a/src/3d/tests/tcpip/TCP.3d +++ b/src/3d/tests/tcpip/TCP.3d @@ -115,7 +115,8 @@ where MaxSegSizeAllowed }; UINT16 MaxSegSize {:act - OptRx->MSS_CLAMP = MaxSegSize;} + OptRx->MSS_CLAMP = MaxSegSize; + }; } MAX_SEG_SIZE_PAYLOAD; typedef struct _TIMESTAMP_PAYLOAD(Bool TimeStampAllowed, @@ -131,7 +132,8 @@ where TimeStampAllowed {:act OptRx->SAW_TSTAMP = 1; OptRx->RCV_TSVAL = Tsval; - OptRx->RCV_TSECR = Tsecr;}; + OptRx->RCV_TSECR = Tsecr; + }; } TIMESTAMP_PAYLOAD; typedef struct _SackPerm_PAYLOAD(Bool SackPermAllowed, From 4bc815ba56981bd913ad651d4784d03f09a7ee7e Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sat, 8 Oct 2022 04:48:55 +0000 Subject: [PATCH 09/12] fixing up an ugly typo that was not caught by CI due to a missing PHONY in a Makefile --- src/3d/Main.fst | 3 ++- src/3d/tests/Makefile | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/3d/Main.fst b/src/3d/Main.fst index e4afed33c..e45ff9b21 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -365,7 +365,6 @@ let process_file (en:env) let emit_config_as_fstar_module () : ML unit = match Deps.get_config () with - | _ -> () | Some (cfg, config_module_name) -> let fst_file_contents = Config.emit_config_as_fstar_module config_module_name cfg in let fst_file = @@ -375,6 +374,8 @@ let emit_config_as_fstar_module () config_module_name) in FStar.IO.write_string fst_file fst_file_contents; FStar.IO.close_write_file fst_file + | _ -> () + let process_files (files_and_modules:list (string & string)) (emit_fstar:string -> ML bool) diff --git a/src/3d/tests/Makefile b/src/3d/tests/Makefile index 4911562b3..37bd433b5 100644 --- a/src/3d/tests/Makefile +++ b/src/3d/tests/Makefile @@ -97,4 +97,4 @@ batch-cleanup-test: clean: rm -rf out.batch out.fail.batch out.cleanup out.inplace-hash test-cpp.exe out.batch-interpret -.PHONY: all batch-test batch-test-negative %.negtest clean batch-cleanup-test inplace-hash-test modules modules-interpret tcpip extern %.interpret batch-interpret-test static funptr +.PHONY: all batch-test batch-test-negative %.negtest clean batch-cleanup-test inplace-hash-test modules modules-interpret tcpip extern %.interpret batch-interpret-test static funptr ifdefs From 57694a6fe4984b0b4cbb5d3ba1622ffeef7f0076 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 10 Oct 2022 16:04:01 -0700 Subject: [PATCH 10/12] updating documentation to include #if and config files --- doc/3d-lang.rst | 54 +++++++++ doc/3d-snapshot/PointArch_32_64.c | 137 +++++++++++++++++++++++ doc/3d-snapshot/PointArch_32_64.h | 39 +++++++ doc/3d-snapshot/PointArch_32_64Wrapper.c | 41 +++++++ doc/3d-snapshot/PointArch_32_64Wrapper.h | 16 +++ doc/Arch.3d.config | 6 + doc/Makefile | 10 +- doc/PointArch_32_64.3d | 14 +++ doc/out/arch_flags.h | 1 + 9 files changed, 315 insertions(+), 3 deletions(-) create mode 100755 doc/3d-snapshot/PointArch_32_64.c create mode 100755 doc/3d-snapshot/PointArch_32_64.h create mode 100755 doc/3d-snapshot/PointArch_32_64Wrapper.c create mode 100755 doc/3d-snapshot/PointArch_32_64Wrapper.h create mode 100755 doc/Arch.3d.config create mode 100755 doc/PointArch_32_64.3d create mode 100755 doc/out/arch_flags.h diff --git a/doc/3d-lang.rst b/doc/3d-lang.rst index 23124c724..e9211c4de 100644 --- a/doc/3d-lang.rst +++ b/doc/3d-lang.rst @@ -508,6 +508,60 @@ Restrictions * Actions cannot be associated with bit fields. +Generating code with for several compile-time configurations +------------------------------------------------------------ + +Sometimes one wants to write a single format specification to +accommodate several compile-time configurations, e.g., to support +multiple architectures. 3D offers some limited support for decorating +a specification with compile-time conditionals familiar to C +programmmers, e.g., ``#if`` and ``#else``, and to generate C code +while preserving these C preprocessor directives. + +For example, the listing below shows an integer type that can either +be represented using 64 bits (if ``ARCH64`` is true) or 32 bits. + +.. literalinclude:: PointArch_32_64.3d + :language: c + +To compile such a file using 3D, we also need to provide a +``.3d.config`` file that declares all the compile-time flags used in +the specification and mentions a C header file in which to find +definitions for those flags. Here is a sample config file: + +.. literalinclude:: Arch.3d.config + +Then, one can invoke ``3d.exe --config Arch.3d.config +PointArch_32_64.3d --batch``, which produces the following C code as +output. + +In the header file ``PointArch_32_64.h``, we see an include for +the header file mentioned in the config: + +.. code-block:: c + + #include "arch_flags.h" + +In the generated C file, ``PointArch_32_64.c``, we see the code below, +with the suitable preprocessor directives protecting the two variants +of the the ``Int`` type declared in the source 3d file. + +.. code-block:: c + + static inline uint64_t + ValidateInt(...) { + { + #if ARCH64 + /* Validating field x */ + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + ... + #else + /* Validating field x */ + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + ... + #endif + } + Checking 3d types for correspondence with existing C types ---------------------------------------------------------- diff --git a/doc/3d-snapshot/PointArch_32_64.c b/doc/3d-snapshot/PointArch_32_64.c new file mode 100755 index 000000000..fb32a09d7 --- /dev/null +++ b/doc/3d-snapshot/PointArch_32_64.c @@ -0,0 +1,137 @@ + + +#include "PointArch_32_64.h" + + + +static inline uint64_t +ValidateInt( + uint8_t *Ctxt, + void + (*Err)( + EverParseString x0, + EverParseString x1, + EverParseString x2, + uint64_t x3, + uint8_t *x4, + uint8_t *x5, + uint64_t x6 + ), + uint8_t *Input, + uint64_t InputLen, + uint64_t StartPosition +) +{ + #if ARCH64 + /* Validating field x */ + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes = (uint64_t)8U <= (InputLen - StartPosition); + uint64_t positionAfterInt; + if (hasBytes) + { + positionAfterInt = StartPosition + (uint64_t)8U; + } + else + { + positionAfterInt = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + StartPosition); + } + if (EverParseIsSuccess(positionAfterInt)) + { + return positionAfterInt; + } + Err("_INT", + "x", + EverParseErrorReasonOfResult(positionAfterInt), + EverParseGetValidatorErrorKind(positionAfterInt), + Ctxt, + Input, + StartPosition); + return positionAfterInt; + #else + /* Validating field x */ + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes = (uint64_t)4U <= (InputLen - StartPosition); + uint64_t positionAfterInt; + if (hasBytes) + { + positionAfterInt = StartPosition + (uint64_t)4U; + } + else + { + positionAfterInt = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + StartPosition); + } + if (EverParseIsSuccess(positionAfterInt)) + { + return positionAfterInt; + } + Err("_INT", + "x", + EverParseErrorReasonOfResult(positionAfterInt), + EverParseGetValidatorErrorKind(positionAfterInt), + Ctxt, + Input, + StartPosition); + return positionAfterInt; + #endif +} + +uint64_t +PointArch3264ValidatePoint( + uint8_t *Ctxt, + void + (*Err)( + EverParseString x0, + EverParseString x1, + EverParseString x2, + uint64_t x3, + uint8_t *x4, + uint8_t *x5, + uint64_t x6 + ), + uint8_t *Input, + uint64_t InputLength, + uint64_t StartPosition +) +{ + /* Validating field x */ + uint64_t positionAfterPoint = ValidateInt(Ctxt, Err, Input, InputLength, StartPosition); + uint64_t positionAfterx; + if (EverParseIsSuccess(positionAfterPoint)) + { + positionAfterx = positionAfterPoint; + } + else + { + Err("_POINT", + "x", + EverParseErrorReasonOfResult(positionAfterPoint), + EverParseGetValidatorErrorKind(positionAfterPoint), + Ctxt, + Input, + StartPosition); + positionAfterx = positionAfterPoint; + } + if (EverParseIsError(positionAfterx)) + { + return positionAfterx; + } + /* Validating field y */ + uint64_t positionAfterPoint0 = ValidateInt(Ctxt, Err, Input, InputLength, positionAfterx); + if (EverParseIsSuccess(positionAfterPoint0)) + { + return positionAfterPoint0; + } + Err("_POINT", + "y", + EverParseErrorReasonOfResult(positionAfterPoint0), + EverParseGetValidatorErrorKind(positionAfterPoint0), + Ctxt, + Input, + positionAfterx); + return positionAfterPoint0; +} + diff --git a/doc/3d-snapshot/PointArch_32_64.h b/doc/3d-snapshot/PointArch_32_64.h new file mode 100755 index 000000000..8274fc941 --- /dev/null +++ b/doc/3d-snapshot/PointArch_32_64.h @@ -0,0 +1,39 @@ + + +#ifndef __PointArch_32_64_H +#define __PointArch_32_64_H + +#if defined(__cplusplus) +extern "C" { +#endif + + + + + +#include "arch_flags.h" +#include "EverParse.h" +uint64_t +PointArch3264ValidatePoint( + uint8_t *Ctxt, + void + (*Err)( + EverParseString x0, + EverParseString x1, + EverParseString x2, + uint64_t x3, + uint8_t *x4, + uint8_t *x5, + uint64_t x6 + ), + uint8_t *Input, + uint64_t InputLength, + uint64_t StartPosition +); + +#if defined(__cplusplus) +} +#endif + +#define __PointArch_32_64_H_DEFINED +#endif diff --git a/doc/3d-snapshot/PointArch_32_64Wrapper.c b/doc/3d-snapshot/PointArch_32_64Wrapper.c new file mode 100755 index 000000000..a46015669 --- /dev/null +++ b/doc/3d-snapshot/PointArch_32_64Wrapper.c @@ -0,0 +1,41 @@ +#include "PointArch_32_64Wrapper.h" +#include "EverParse.h" +#include "PointArch_32_64.h" +void PointArch_32_64EverParseError(const char *StructName, const char *FieldName, const char *Reason); + +static +void DefaultErrorHandler( + const char *typename_s, + const char *fieldname, + const char *reason, + uint64_t error_code, + uint8_t *context, + EverParseInputBuffer input, + uint64_t start_pos) +{ + EverParseErrorFrame *frame = (EverParseErrorFrame*)context; + EverParseDefaultErrorHandler( + typename_s, + fieldname, + reason, + error_code, + frame, + input, + start_pos + ); +} + +BOOLEAN PointArch3264CheckPoint(uint8_t *base, uint32_t len) { + EverParseErrorFrame frame; + frame.filled = FALSE; + uint64_t result = PointArch3264ValidatePoint( (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0); + if (EverParseIsError(result)) + { + if (frame.filled) + { + PointArch_32_64EverParseError(frame.typename_s, frame.fieldname, frame.reason); + } + return FALSE; + } + return TRUE; +} diff --git a/doc/3d-snapshot/PointArch_32_64Wrapper.h b/doc/3d-snapshot/PointArch_32_64Wrapper.h new file mode 100755 index 000000000..16b7836fd --- /dev/null +++ b/doc/3d-snapshot/PointArch_32_64Wrapper.h @@ -0,0 +1,16 @@ +#include "EverParseEndianness.h" +#define EVERPARSE_ERROR_GENERIC 1uL +#define EVERPARSE_ERROR_NOT_ENOUGH_DATA 2uL +#define EVERPARSE_ERROR_IMPOSSIBLE 3uL +#define EVERPARSE_ERROR_LIST_SIZE_NOT_MULTIPLE 4uL +#define EVERPARSE_ERROR_ACTION_FAILED 5uL +#define EVERPARSE_ERROR_CONSTRAINT_FAILED 6uL +#define EVERPARSE_ERROR_UNEXPECTED_PADDING 7uL + +#ifdef __cplusplus +extern "C" { +#endif +BOOLEAN PointArch3264CheckPoint(uint8_t *base, uint32_t len); +#ifdef __cplusplus +} +#endif diff --git a/doc/Arch.3d.config b/doc/Arch.3d.config new file mode 100755 index 000000000..bcc5ed855 --- /dev/null +++ b/doc/Arch.3d.config @@ -0,0 +1,6 @@ +{ "compile_time_flags": + { + "flags":["ARCH64"], + "include_file":"arch_flags.h" + } +} \ No newline at end of file diff --git a/doc/Makefile b/doc/Makefile index 4afadb011..a4fae1552 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -9,8 +9,10 @@ export KRML_HOME?=$(realpath $(EVERPARSE_HOME)/../karamel) 3D=$(EVERPARSE_HOME)/bin/3d.exe 3D_EXCLUDE=ConstColor.3d -3D_FILES=$(filter-out $(3D_EXCLUDE),$(wildcard *.3d)) -3D_MODULES=$(basename $(3D_FILES)) +3D_CONFIG=Arch.3d.config +3D_FILES_WITH_CONFIG=PointArch_32_64.3d +3D_FILES=$(filter-out $(3D_EXCLUDE) $(3D_FILES_WITH_CONFIG),$(wildcard *.3d)) +3D_MODULES=$(basename $(3D_FILES) $(3D_FILES_WITH_CONFIG)) 3D_MODULES_AND_WRAPPERS=$(3D_MODULES) $(addsuffix Wrapper,$(3D_MODULES)) 3D_C_AND_H_FILES=$(filter-out BaseWrapper.c BaseWrapper.h,$(addsuffix .c,$(3D_MODULES_AND_WRAPPERS)) $(addsuffix .h,$(3D_MODULES_AND_WRAPPERS))) 3D_DIFF=$(addsuffix .diff,$(3D_C_AND_H_FILES)) @@ -38,17 +40,19 @@ help: 3d: 3d-do-tests -3d-ci: $(3D_DIFF) +3d-ci: $(3D_DIFF) test_compile_time_ifs 3d-do-tests: mkdir -p out $(3D) --odir out --batch $(3D_FILES) + $(3D) --odir out --batch $(3D_FILES_WITH_CONFIG) --config $(3D_CONFIG) cp $(AUX_HEADERS) out +$(MAKE) -C out -f Makefile.basic USER_TARGET=test USER_CFLAGS='-Wno-ignored-qualifiers' test 3d-do-interpreter-tests: mkdir -p interpret.out $(3D) --odir interpret.out --batch $(3D_FILES) --interpret + $(3D) --odir interpret.out --batch $(3D_FILES_WITH_CONFIG) --config $(3D_CONFIG) --interpret cp $(AUX_HEADERS) interpret.out +$(MAKE) -C interpret.out -f Makefile.basic USER_TARGET=test USER_CFLAGS='-Wno-ignored-qualifiers' test diff --git a/doc/PointArch_32_64.3d b/doc/PointArch_32_64.3d new file mode 100755 index 000000000..c24481c8d --- /dev/null +++ b/doc/PointArch_32_64.3d @@ -0,0 +1,14 @@ +typedef struct _INT { +#if ARCH64 + UINT64 x; +#else + UINT32 x; +#endif +} INT; + + +entrypoint +typedef struct _POINT { + INT x; + INT y; +} POINT; diff --git a/doc/out/arch_flags.h b/doc/out/arch_flags.h new file mode 100755 index 000000000..79bb9f68f --- /dev/null +++ b/doc/out/arch_flags.h @@ -0,0 +1 @@ +#define ARCH64 1 From 10f19bfb79f555aed3788fb19d59a038d2a468ec Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 3 Nov 2022 19:58:50 +0000 Subject: [PATCH 11/12] enable ifdef C compiler test and krml bug fix; update snapshot --- doc/3d-snapshot/PointArch_32_64.c | 96 ++++++++++++++++--------------- src/3d/tests/ifdefs/Makefile | 3 +- 2 files changed, 51 insertions(+), 48 deletions(-) diff --git a/doc/3d-snapshot/PointArch_32_64.c b/doc/3d-snapshot/PointArch_32_64.c index fb32a09d7..19c47a28b 100755 --- a/doc/3d-snapshot/PointArch_32_64.c +++ b/doc/3d-snapshot/PointArch_32_64.c @@ -23,59 +23,63 @@ ValidateInt( ) { #if ARCH64 - /* Validating field x */ - /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ - BOOLEAN hasBytes = (uint64_t)8U <= (InputLen - StartPosition); - uint64_t positionAfterInt; - if (hasBytes) - { - positionAfterInt = StartPosition + (uint64_t)8U; - } - else - { - positionAfterInt = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - StartPosition); - } - if (EverParseIsSuccess(positionAfterInt)) { + /* Validating field x */ + /* Checking that we have enough space for a UINT64, i.e., 8 bytes */ + BOOLEAN hasBytes = (uint64_t)8U <= (InputLen - StartPosition); + uint64_t positionAfterInt; + if (hasBytes) + { + positionAfterInt = StartPosition + (uint64_t)8U; + } + else + { + positionAfterInt = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + StartPosition); + } + if (EverParseIsSuccess(positionAfterInt)) + { + return positionAfterInt; + } + Err("_INT", + "x", + EverParseErrorReasonOfResult(positionAfterInt), + EverParseGetValidatorErrorKind(positionAfterInt), + Ctxt, + Input, + StartPosition); return positionAfterInt; } - Err("_INT", - "x", - EverParseErrorReasonOfResult(positionAfterInt), - EverParseGetValidatorErrorKind(positionAfterInt), - Ctxt, - Input, - StartPosition); - return positionAfterInt; #else - /* Validating field x */ - /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ - BOOLEAN hasBytes = (uint64_t)4U <= (InputLen - StartPosition); - uint64_t positionAfterInt; - if (hasBytes) - { - positionAfterInt = StartPosition + (uint64_t)4U; - } - else - { - positionAfterInt = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - StartPosition); - } - if (EverParseIsSuccess(positionAfterInt)) { + /* Validating field x */ + /* Checking that we have enough space for a UINT32, i.e., 4 bytes */ + BOOLEAN hasBytes = (uint64_t)4U <= (InputLen - StartPosition); + uint64_t positionAfterInt; + if (hasBytes) + { + positionAfterInt = StartPosition + (uint64_t)4U; + } + else + { + positionAfterInt = + EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, + StartPosition); + } + if (EverParseIsSuccess(positionAfterInt)) + { + return positionAfterInt; + } + Err("_INT", + "x", + EverParseErrorReasonOfResult(positionAfterInt), + EverParseGetValidatorErrorKind(positionAfterInt), + Ctxt, + Input, + StartPosition); return positionAfterInt; } - Err("_INT", - "x", - EverParseErrorReasonOfResult(positionAfterInt), - EverParseGetValidatorErrorKind(positionAfterInt), - Ctxt, - Input, - StartPosition); - return positionAfterInt; #endif } diff --git a/src/3d/tests/ifdefs/Makefile b/src/3d/tests/ifdefs/Makefile index 645da6625..55262add6 100644 --- a/src/3d/tests/ifdefs/Makefile +++ b/src/3d/tests/ifdefs/Makefile @@ -74,8 +74,7 @@ clean: ####################################################### # Specify the behavior of the default rule -# excluding AnonNestedStructIfDefs.o for now, since we hit krml bug #293 -world: $(EVERPARSE_OUTPUT_DIR)/CompileTimeIf.o $(EVERPARSE_ALL_C_FILES) batch +world: $(EVERPARSE_OUTPUT_DIR)/CompileTimeIf.o $(EVERPARSE_OUTPUT_DIR)/AnonNestedStructIfDefs.o $(EVERPARSE_ALL_C_FILES) batch ####################################################### # Also test batch mode From 80a4185f6007a592b96a0bfa7dbe1729f7eba774 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 3 Nov 2022 22:19:24 +0000 Subject: [PATCH 12/12] remove spurious make target --- doc/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/Makefile b/doc/Makefile index a4fae1552..b35f37ae4 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -40,7 +40,7 @@ help: 3d: 3d-do-tests -3d-ci: $(3D_DIFF) test_compile_time_ifs +3d-ci: $(3D_DIFF) 3d-do-tests: mkdir -p out