diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000000..f41b1071d7 --- /dev/null +++ b/.ocamlformat @@ -0,0 +1 @@ +version = 0.26.1 diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index 7935a6bc34..3e64a04141 100644 --- a/asllib/Interpreter.ml +++ b/asllib/Interpreter.ml @@ -208,8 +208,7 @@ module Make (B : Backend.S) (C : Config) = struct in let fold = function | TopoSort.ASTFold.Single d -> process_one_decl d - | TopoSort.ASTFold.Recursive ds -> - List.fold_right process_one_decl ds + | TopoSort.ASTFold.Recursive ds -> List.fold_right process_one_decl ds in fun ast -> TopoSort.ASTFold.fold fold ast @@ -841,8 +840,7 @@ module Make (B : Backend.S) (C : Config) = struct List.fold_left2 folder (return_normal env) ldis liv |: SemanticsRule.LDTuple (* End *) - | LDI_Var _, None - | LDI_Tuple _, None -> + | LDI_Var _, None | LDI_Tuple _, None -> (* Should not happen in V1 because of TypingRule.LDUninitialisedTuple *) fatal_from s Error.TypeInferenceNeeded @@ -991,17 +989,14 @@ module Make (B : Backend.S) (C : Config) = struct let () = if debug then let open Format in - let pp_value fmt v = - B.debug_value v |> pp_print_string fmt - in + let pp_value fmt v = B.debug_value v |> pp_print_string fmt in eprintf "@[@<2>%a:@ @[%a@]@ ->@ %a@]@." PP.pp_pos s (pp_print_list ~pp_sep:pp_print_space PP.pp_expr) args (pp_print_list ~pp_sep:pp_print_space pp_value) vs else ( - List.map B.debug_value vs - |> String.concat " " |> print_string; + List.map B.debug_value vs |> String.concat " " |> print_string; print_newline ()) in return_continue env |: SemanticsRule.SDebug diff --git a/asllib/Typing.ml b/asllib/Typing.ml index ac1f2714e8..c423a32df9 100644 --- a/asllib/Typing.ml +++ b/asllib/Typing.ml @@ -102,7 +102,7 @@ let rename_ty_eqs : (AST.identifier * AST.expr) list -> AST.ty -> AST.ty = T_Int (WellConstrained constraints) |> add_pos_from_st ty | _ -> ty -(* Begin Lit *) +(* Begin Lit *) let annotate_literal = function | L_Int _ as v -> integer_exact' (literal v) | L_Bool _ -> T_Bool @@ -1804,11 +1804,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (S_Try (s'', catchers', otherwise') |> here, env) |: TypingRule.STry (* End *) | S_Print { args; debug } -> - let args' = - List.map (fun e -> annotate_expr env e |> snd) args - in - (S_Print { args = args'; debug } |> here, env) - |: TypingRule.SDebug + let args' = List.map (fun e -> annotate_expr env e |> snd) args in + (S_Print { args = args'; debug } |> here, env) |: TypingRule.SDebug and annotate_catcher env (name_opt, ty, stmt) = let+ () = check_structure_exception ty env ty in @@ -2019,8 +2016,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct else add_global_storage name ty keyword env let declare_const loc name t v env = - add_global_storage loc name GDK_Constant env t - |> add_global_constant name v + add_global_storage loc name GDK_Constant env t |> add_global_constant name v let rec check_is_valid_bitfield loc env width bitfield () = let slices = bitfield_get_slices bitfield in @@ -2182,8 +2178,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Shouldn't happen because of parser construction. *) Error.fatal_from loc (Error.NotYetImplemented - "Global storage declaration must have an initial value or \ - a type.") + "Global storage declaration must have an initial value or a type.") (* End *) let rename_primitive loc env (f : AST.func) = @@ -2244,8 +2239,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct match d.desc with | D_Func ({ body = SB_ASL _; name; _ } as f) -> let () = - if false then - Format.eprintf "@[Analysing decl %s.@]@." name + if false then Format.eprintf "@[Analysing decl %s.@]@." name in D_Func (try_annotate_subprogram d env f) |> add_pos_from d | D_Func ({ body = SB_Primitive; _ } as f) -> @@ -2261,9 +2255,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | TopoSort.ASTFold.Single d -> type_check_decl d | TopoSort.ASTFold.Recursive ds -> type_check_mutually_rec ds in - let fold_topo ast acc = - TopoSort.ASTFold.fold fold ast acc - in + let fold_topo ast acc = TopoSort.ASTFold.fold fold ast acc in fun ast env -> let ast_rev, env = fold_topo ast ([], env) in (List.rev ast_rev, env) diff --git a/asllib/bitvector.ml b/asllib/bitvector.ml index 2e03844e8b..434ee08b0e 100644 --- a/asllib/bitvector.ml +++ b/asllib/bitvector.ml @@ -90,8 +90,7 @@ let _pp_data f (length, data) = pp_print_char f 'x'; String.iter (fun c -> fprintf f "%x" @@ Char.code c) data -let create_data_bytes length = - Bytes.create ((length + 7)/8) +let create_data_bytes length = Bytes.create ((length + 7) / 8) (** [String.for_all] taken directly out of stdlib version 4.13 . *) let string_for_all p s = @@ -260,8 +259,7 @@ let z64 = Z.shift_left Z.one 64 let printable bv = let z = to_z_signed bv in - if Z.geq z z63 then Z.sub z z64 - else z + if Z.geq z z63 then Z.sub z z64 else z let of_string s = let result = Buffer.create ((String.length s / 8) + 1) in @@ -434,47 +432,44 @@ let write_slice (length_dst, data_dst) (length_src, data_src) positions = let () = List.iteri copy_bit_here positions in remask (length_dst, Bytes.unsafe_to_string result) - (* Retuns length of destination *) -let pp (l,bs) = - Printf.sprintf "%s<%d>" - (to_string (l,Bytes.to_string bs)) l +let pp (l, bs) = Printf.sprintf "%s<%d>" (to_string (l, Bytes.to_string bs)) l let pp_bytes n dst = - let sz = (n+1)*8 in - pp (sz,dst) + let sz = (n + 1) * 8 in + pp (sz, dst) (* [mix_chars_start off low_c high_c] return a char, whose off lower order bits are from low_c and the 8-off higher order bits are the 8-off lower order bits of high_c *) let mix_chars_start off low_c high_c = - let low_bits = (1 lsl off-1) land (Char.code low_c) - and high_bits = (Char.code high_c) lsl off in - low_bits lor high_bits |> (land) 0xff |> Char.chr + let low_bits = ((1 lsl off) - 1) land Char.code low_c + and high_bits = Char.code high_c lsl off in + low_bits lor high_bits |> ( land ) 0xff |> Char.chr (* [mix_chars_body off low_c high_c] return a char, whose off lower order bits are the off higher order bits of low_c and the 8-off higher order bits are the 8-off lower order bits of high_c *) let mix_chars_body off low_c high_c = - let low_bits = (Char.code low_c) lsr (8-off) - and high_bits = (Char.code high_c) lsl off in - low_bits lor high_bits |> (land) 0xff |> Char.chr + let low_bits = Char.code low_c lsr (8 - off) + and high_bits = Char.code high_c lsl off in + low_bits lor high_bits |> ( land ) 0xff |> Char.chr (* [mix_chars_final off c] return a char, whose sz lower order bits are the sz bits of c at possition off. *) let mix_char_final off sz c = - (Char.code c lsr off) land (1 lsl sz-1) |> Char.chr + (Char.code c lsr off) land ((1 lsl sz) - 1) |> Char.chr -let copy_into dst (length_src, data_src as b) offset = +let copy_into dst ((length_src, data_src) as b) offset = let () = if false then - Printf.eprintf "copy_into %s + %s, offset=%d\n%!" - (to_string b) - (pp (offset,dst)) - offset in + Printf.eprintf "copy_into %s + %s, offset=%d\n%!" (to_string b) + (pp (offset, dst)) + offset + in let length_dst = offset + length_src in if length_src <= 0 then length_dst else @@ -489,11 +484,10 @@ let copy_into dst (length_src, data_src as b) offset = * copied into the 8-m_off high order_bits of * dst.[n_off] *) let prec_c = Bytes.get dst n_off and next_c = String.get data_src 0 in - mix_chars_start m_off prec_c next_c |> Bytes.set dst n_off ; + mix_chars_start m_off prec_c next_c |> Bytes.set dst n_off; let () = - if false then - Printf.eprintf "Start: %s\n%!" - (pp_bytes n_off dst) in + if false then Printf.eprintf "Start: %s\n%!" (pp_bytes n_off dst) + in (* * Now, loop. * At each step, 8-off bits are taken from @@ -502,43 +496,43 @@ let copy_into dst (length_src, data_src as b) offset = * lower order bits of the next_char *) (* Number of bits still to write *) - let rem_bits = length_src - (8-m_off) in + let rem_bits = length_src - (8 - m_off) in (* Useful string length *) - let src_str_len = (length_src+7) / 8 in - let rec do_rec i_src i_dst rem_bits = - if i_src+1 >= src_str_len then - i_src,i_dst,rem_bits - else begin + let src_str_len = (length_src + 7) / 8 in + let rec do_rec i_src i_dst rem_bits = + if i_src + 1 >= src_str_len then (i_src, i_dst, rem_bits) + else let prec_c = String.get data_src i_src in let next_c = String.get data_src (i_src + 1) in - mix_chars_body (m_off) prec_c next_c |> Bytes.set dst i_dst; + mix_chars_body m_off prec_c next_c |> Bytes.set dst i_dst; let () = if false then - Printf.eprintf "Body -> %s\n%!" (pp_bytes i_dst dst) in - do_rec (i_src+1) (i_dst+1) (rem_bits-8) - end in - let i_src,i_dst,rem_bits = do_rec 0 (n_off+1) rem_bits in - let () = - if false then - Printf.eprintf "i_src=%d, i_dst=%d, rem_bits=%d\n%!" - i_src i_dst rem_bits in - if rem_bits > 0 then begin - let c = String.get data_src i_src in - mix_char_final (8-m_off) rem_bits c |> Bytes.set dst i_dst - end in + Printf.eprintf "Body -> %s\n%!" (pp_bytes i_dst dst) + in + do_rec (i_src + 1) (i_dst + 1) (rem_bits - 8) + in + let i_src, i_dst, rem_bits = do_rec 0 (n_off + 1) rem_bits in + let () = + if false then + Printf.eprintf "i_src=%d, i_dst=%d, rem_bits=%d\n%!" i_src i_dst + rem_bits + in + if rem_bits > 0 then + let c = String.get data_src i_src in + mix_char_final (8 - m_off) rem_bits c |> Bytes.set dst i_dst + in let () = if false then - Printf.eprintf "copy_into %s + %s ->%s\n%!" - (to_string b) - (pp (offset,dst)) - (pp (length_dst, dst)) in + Printf.eprintf "copy_into %s + %s ->%s\n%!" (to_string b) + (pp (offset, dst)) + (pp (length_dst, dst)) + in length_dst let concat bvs = - if false then begin - let pp = List.map to_string bvs in - Printf.eprintf "Concat %s\n%!" (String.concat "," pp) - end ; + (if false then + let pp = List.map to_string bvs in + Printf.eprintf "Concat %s\n%!" (String.concat "," pp)); let length = List.fold_left (fun acc bv -> acc + length bv) 0 bvs in let result = create_data_bytes length in let _ = List.fold_right (copy_into result) bvs 0 in diff --git a/asllib/dune b/asllib/dune index 226fb43064..a4380201d9 100644 --- a/asllib/dune +++ b/asllib/dune @@ -1,19 +1,28 @@ -(rule (copy ../Version.ml Version.ml)) +(rule + (copy ../Version.ml Version.ml)) (ocamllex Lexer) + (ocamllex SimpleLexer0) + (ocamllex splitasl) -(menhir (modules Parser)) -(menhir (modules Parser0) (flags --unused-tokens --table)) +(menhir + (modules Parser)) + +(menhir + (modules Parser0) + (flags --unused-tokens --table)) (library (name asllib) - (modules (:standard \ aslref bundler)) + (modules + (:standard \ aslref bundler)) (public_name herdtools7.asllib) (private_modules Parser0 Gparser0 Lexer0 SimpleLexer0 RepeatableLexer) (modules_without_implementation Backend AST) - (flags (:standard -w -40-42)) + (flags + (:standard -w -40-42)) (libraries menhirLib zarith)) (documentation) @@ -25,8 +34,7 @@ (modules aslref)) (executable - (public_name aslbundler) - (name bundler) - (libraries asllib) - (modules bundler)) - + (public_name aslbundler) + (name bundler) + (libraries asllib) + (modules bundler)) diff --git a/asllib/tests/dune b/asllib/tests/dune index abd32c5050..ec6a4b02e3 100644 --- a/asllib/tests/dune +++ b/asllib/tests/dune @@ -1,35 +1,44 @@ (library - (name test_helpers) - (modules Helpers) - (libraries asllib)) + (name test_helpers) + (modules Helpers) + (libraries asllib)) (test - (name asltests) - (modes native) - (modules asltests) - (libraries asllib test_helpers) - (deps (glob_files asl/required/*.asl) asltests.ml ../libdir/stdlib.asl) - (action - (setenv ASL_LIBDIR %{project_root}/asllib/libdir/ - (run %{test} asl/required)))) + (name asltests) + (modes native) + (modules asltests) + (libraries asllib test_helpers) + (deps + (glob_files asl/required/*.asl) + asltests.ml + ../libdir/stdlib.asl) + (action + (setenv + ASL_LIBDIR + %{project_root}/asllib/libdir/ + (run %{test} asl/required)))) (test - (name toposort) - (modes native) - (enabled_if %{lib-available:qcheck}) - (libraries asllib qcheck) - (modules toposort)) + (name toposort) + (modes native) + (enabled_if %{lib-available:qcheck}) + (libraries asllib qcheck) + (modules toposort)) (tests - (names static bitvector types) - (modules static bitvector types) - (modes native) - (deps (:standard ../libdir/stdlib.asl)) - (libraries asllib test_helpers zarith) - (flags (:standard -w -40-42)) - (action - (setenv ASL_LIBDIR %{project_root}/asllib/libdir/ - (run %{test} -e)))) + (names static bitvector types) + (modules static bitvector types) + (modes native) + (deps + (:standard ../libdir/stdlib.asl)) + (libraries asllib test_helpers zarith) + (flags + (:standard -w -40-42)) + (action + (setenv + ASL_LIBDIR + %{project_root}/asllib/libdir/ + (run %{test} -e)))) (cram - (deps %{bin:aslref})) + (deps %{bin:aslref})) diff --git a/asllib/tests/types.ml b/asllib/tests/types.ml index 4b5ade0c18..65b05c7d75 100644 --- a/asllib/tests/types.ml +++ b/asllib/tests/types.ml @@ -91,7 +91,7 @@ let structure_example () = () let subtype_examples () = -(* + (* let bits_4 = !!(T_Bits (!$4, [])) in let bits_2_4 = !!(T_Bits @@ -170,8 +170,8 @@ let type_clashes () = () let enum_example () = - let variants = [ "A"; "B"] in - let variants' = [ "A"; "B"] in + let variants = [ "A"; "B" ] in + let variants' = [ "A"; "B" ] in let t1 = !!(T_Enum variants) in let t2 = !!(T_Enum variants') in diff --git a/asllib/types.ml b/asllib/types.ml index bb5440688a..23de88e520 100644 --- a/asllib/types.ml +++ b/asllib/types.ml @@ -62,8 +62,7 @@ let rec make_anonymous (env : env) (ty : ty) : ty = (* Begin Structure *) let rec get_structure (env : env) (ty : ty) : ty = let () = - if false then - Format.eprintf "@[Getting structure of %a.@]@." PP.pp_ty ty + if false then Format.eprintf "@[Getting structure of %a.@]@." PP.pp_ty ty in let with_pos = add_pos_from ty in (match ty.desc with @@ -75,14 +74,10 @@ let rec get_structure (env : env) (ty : ty) : ty = | T_Tuple tys -> T_Tuple (List.map (get_structure env) tys) |> with_pos | T_Array (e, t) -> T_Array (e, (get_structure env) t) |> with_pos | T_Record fields -> - let fields' = - assoc_map (get_structure env) fields |> canonical_fields - in + let fields' = assoc_map (get_structure env) fields |> canonical_fields in T_Record fields' |> with_pos | T_Exception fields -> - let fields' = - assoc_map (get_structure env) fields |> canonical_fields - in + let fields' = assoc_map (get_structure env) fields |> canonical_fields in T_Exception fields' |> with_pos) |: TypingRule.Structure (* End *) @@ -113,8 +108,7 @@ let is_builtin ty = (* Begin Named *) let is_named ty = - (match ty.desc with T_Named _ -> true | _ -> false) - |: TypingRule.NamedType + (match ty.desc with T_Named _ -> true | _ -> false) |: TypingRule.NamedType (* End *) (* Begin Anonymous *) @@ -152,8 +146,7 @@ let rec is_non_primitive ty = (* End *) (* Begin Primitive *) -let is_primitive ty = - (not (is_non_primitive ty)) |: TypingRule.PrimitiveType +let is_primitive ty = (not (is_non_primitive ty)) |: TypingRule.PrimitiveType (* End *) let under_constrained_constraints = @@ -189,11 +182,9 @@ module Domain = struct | D_Bool | D_String | D_Real - | D_Symbols of ISet.t - (** The domain of an enum is a set of symbols *) + | D_Symbols of ISet.t (** The domain of an enum is a set of symbols *) | D_Int of int_set - | D_Bits of int_set - (** The domain of a bitvector is given by its width. *) + | D_Bits of int_set (** The domain of a bitvector is given by its width. *) (* |: TypingRule.Domain *) (* End *) @@ -232,8 +223,7 @@ module Domain = struct with StaticInterpreter.NotYetImplemented -> e in try StaticInterpreter.static_eval env e - with - | Error.ASLException { desc = Error.UndefinedIdentifier _; _ } -> + with Error.ASLException { desc = Error.UndefinedIdentifier _; _ } -> raise_notrace StaticEvaluationTop in match v with @@ -255,8 +245,7 @@ module Domain = struct match constraints with | [] -> failwith - "A well-constrained integer cannot have an empty list of \ - constraints." + "A well-constrained integer cannot have an empty list of constraints." | _ -> ( try Finite @@ -267,8 +256,7 @@ module Domain = struct let int_set_to_int_constraints = let interval_to_constraint interval = - let x = IntSet.Interval.x interval - and y = IntSet.Interval.y interval in + let x = IntSet.Interval.x interval and y = IntSet.Interval.y interval in let expr_of_z z = L_Int z |> literal in Constraint_Range (expr_of_z x, expr_of_z y) in @@ -283,8 +271,7 @@ module Domain = struct | Finite is1, Finite is2 -> Finite (IntSet.fold - (fun i1 -> - IntSet.fold (fun i2 -> IntSet.add (fop i1 i2)) is2) + (fun i1 -> IntSet.fold (fun i2 -> IntSet.add (fop i1 i2)) is2) is1 IntSet.empty) | Finite is1, FromSyntax _ -> let s1 = int_set_to_int_constraints is1 in @@ -311,8 +298,7 @@ module Domain = struct | L_Real _ -> D_Real | L_String _ -> D_String | L_BitVector bv -> - D_Bits - (Finite (Bitvector.length bv |> Z.of_int |> IntSet.singleton)) + D_Bits (Finite (Bitvector.length bv |> Z.of_int |> IntSet.singleton)) let rec of_expr env e = match e.desc with @@ -329,10 +315,8 @@ module Domain = struct of_expr env (E_Binop (MINUS, !$0, e') |> add_pos_from e) | E_Unop _ -> assert false | E_Binop (((PLUS | MINUS | MUL) as op), e1, e2) -> - let is1 = - match of_expr env e1 with D_Int is -> is | _ -> assert false - and is2 = - match of_expr env e2 with D_Int is -> is | _ -> assert false + let is1 = match of_expr env e1 with D_Int is -> is | _ -> assert false + and is2 = match of_expr env e2 with D_Int is -> is | _ -> assert false and fop = match op with | PLUS -> monotone_interval_op Z.add @@ -344,9 +328,8 @@ module Domain = struct | _ -> let () = if false then - Format.eprintf - "@[<2>Cannot interpret as int set:@ @[%a@]@]@." PP.pp_expr - e + Format.eprintf "@[<2>Cannot interpret as int set:@ @[%a@]@]@." + PP.pp_expr e in raise StaticEvaluationTop @@ -531,8 +514,7 @@ and structural_subtype_satisfies env t s = | [], _ -> true | _, [] -> false | bfs_s, bfs_t -> - bitwidth_equal env w_s w_t - && bitfields_included env bfs_s bfs_t) + bitwidth_equal env w_s w_t && bitfields_included env bfs_s bfs_t) | T_Bits _, _ -> false (* If S has the structure of an array type with elements of type E then T must have the structure of an array type with elements of type E, @@ -564,8 +546,7 @@ and structural_subtype_satisfies env t s = String.equal name_s name_t && type_equal env ty_s ty_t) fields_t) fields_s - | T_Exception _, _ | T_Record _, _ -> - false (* A structure cannot be a name *) + | T_Exception _, _ | T_Record _, _ -> false (* A structure cannot be a name *) | T_Named _, _ -> assert false) |: TypingRule.StructuralSubtypeSatisfaction @@ -582,9 +563,8 @@ and domain_subtype_satisfies env t s = and d_t = get_structure env t |> Domain.of_type env in let () = if false then - Format.eprintf - "domain_subtype_satisfies: %a included in %a?@." Domain.pp - d_t Domain.pp d_s + Format.eprintf "domain_subtype_satisfies: %a included in %a?@." + Domain.pp d_t Domain.pp d_s in Domain.is_subset env d_t d_s | T_Bits _ -> ( @@ -599,8 +579,8 @@ and domain_subtype_satisfies env t s = and s_domain = Domain.of_type env s_struct in let () = if false then - Format.eprintf "Is %a included in %a?@." Domain.pp t_domain - Domain.pp s_domain + Format.eprintf "Is %a included in %a?@." Domain.pp t_domain Domain.pp + s_domain in match ( Domain.get_width_singleton_opt s_domain, @@ -620,11 +600,10 @@ and subtype_satisfies env t s = if false then let b1 = structural_subtype_satisfies env t s in let b2 = domain_subtype_satisfies env t s in - Format.eprintf "%a subtypes %a ? struct: %B -- domain: %B@." - PP.pp_ty t PP.pp_ty s b1 b2 + Format.eprintf "%a subtypes %a ? struct: %B -- domain: %B@." PP.pp_ty t + PP.pp_ty s b1 b2 in - (structural_subtype_satisfies env t s - && domain_subtype_satisfies env t s) + (structural_subtype_satisfies env t s && domain_subtype_satisfies env t s) |: TypingRule.SubtypeSatisfaction (* End *) @@ -669,8 +648,7 @@ let rec type_clashes env t s = (* We will add a rule for boolean and boolean. *) ((subtypes env s t || subtypes env t s) || - let s_struct = get_structure env s - and t_struct = get_structure env t in + let s_struct = get_structure env s and t_struct = get_structure env t in match (s_struct.desc, t_struct.desc) with | T_Int _, T_Int _ | T_Real, T_Real @@ -777,9 +755,7 @@ let rec lowest_common_ancestor env s t = let maybe_ancestors = List.map2 (lowest_common_ancestor env) li_s li_t in - let ancestors = - List.filter_map Fun.id maybe_ancestors - in + let ancestors = List.filter_map Fun.id maybe_ancestors in if List.compare_lengths ancestors li_s = 0 then Some (add_dummy_pos (T_Tuple ancestors)) else None) @@ -793,8 +769,7 @@ let rec lowest_common_ancestor env s t = (* If either S or T have the structure of an under-constrained integer type: the under-constrained integer type. *) Some t - | T_Int (WellConstrained cs_s), T_Int (WellConstrained cs_t) - -> ( + | T_Int (WellConstrained cs_s), T_Int (WellConstrained cs_t) -> ( (* Implicit: cs_s and cs_t are non-empty, see patterns above. *) (* If S and T both have the structure of well-constrained integer types: @@ -810,9 +785,7 @@ let rec lowest_common_ancestor env s t = | _ -> (* TODO: simplify domains ? If domains use a form of diets, this could be more efficient. *) - Some - (add_dummy_pos - (T_Int (WellConstrained (cs_s @ cs_t))))) + Some (add_dummy_pos (T_Int (WellConstrained (cs_s @ cs_t))))) | T_Int UnConstrained, _ -> ( (* Here S has the structure of an unconstrained integer type. *) (* TODO: revisit? *) @@ -873,19 +846,16 @@ let rec base_value loc env t = | T_Bits (e, _) -> let e = normalize env e in E_Call ("Zeros", [ e ], []) |> add_pos_from t - | T_Enum li -> - IMap.find (List.hd li) env.global.constants_values |> lit + | T_Enum li -> IMap.find (List.hd li) env.global.constants_values |> lit | T_Int UnConstrained -> !$0 | T_Int (UnderConstrained _) -> (* This case cannot happen: For example, if you have a variable declaration var foo: ty, ty cannot be an underconstrained integer type, as there is no syntax for it. *) - failwith - "Cannot get the base-value of an under-constrained integer." + failwith "Cannot get the base-value of an under-constrained integer." | T_Int (WellConstrained []) -> - failwith - "Well Constrained integers cannot have an empty constraint." + failwith "Well Constrained integers cannot have an empty constraint." | T_Int (WellConstrained (Constraint_Exact e :: _)) | T_Int (WellConstrained (Constraint_Range (e, _) :: _)) -> normalize env e diff --git a/dune b/dune index fd28ebdf1c..b03bb06120 100644 --- a/dune +++ b/dune @@ -8,8 +8,8 @@ (alias (name default) (deps - (alias install) - (alias internal/all))) + (alias install) + (alias internal/all))) (alias (name jerd) diff --git a/gen/.ocamlformat b/gen/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/gen/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/gen/dune b/gen/dune index 3b8afc4395..4db27dd44f 100644 --- a/gen/dune +++ b/gen/dune @@ -1,11 +1,13 @@ (ocamllex lexUtil lexLog_gen lexConf_gen autoLex) -(rule (copy ../Version.ml Version.ml)) + +(rule + (copy ../Version.ml Version.ml)) + (executables - (names - readRelax atoms diycross mexpand atomize diyone nexts classify diy norm - ) - (public_names - readRelax7 atoms7 diycross7 mexpand7 atomize7 diyone7 nexts7 classify7 diy7 norm7 - ) - (libraries herdtools unix) - (modules_without_implementation archLoc archRun arch_gen atom autoInterpret builder fence XXXCompile_gen rmw)) + (names readRelax atoms diycross mexpand atomize diyone nexts classify diy + norm) + (public_names readRelax7 atoms7 diycross7 mexpand7 atomize7 diyone7 nexts7 + classify7 diy7 norm7) + (libraries herdtools unix) + (modules_without_implementation archLoc archRun arch_gen atom autoInterpret + builder fence XXXCompile_gen rmw)) diff --git a/herd-www/.ocamlformat b/herd-www/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/herd-www/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/herd-www/dune b/herd-www/dune index c1d2a2545b..b432058447 100644 --- a/herd-www/dune +++ b/herd-www/dune @@ -1,13 +1,20 @@ -(copy_files (files ../herd/*.{ml,mli})) +(copy_files + (files ../herd/*.{ml,mli})) (executable - (name jerd) - (modes js) - (optional) - (libraries herdtools js_of_ocaml zarith_stubs_js) - (preprocess (per_module - ((pps js_of_ocaml-ppx) jerd) - ((action (system "awk -f herd-www/notwww.awk %{input-file}")) - AArch64ParseTest ParseTest Top_herd))) - (js_of_ocaml (flags --disable genprim)) - (modules_without_implementation AArch64Sig action arch_herd monad sem XXXMem)) + (name jerd) + (modes js) + (optional) + (libraries herdtools js_of_ocaml zarith_stubs_js) + (preprocess + (per_module + ((pps js_of_ocaml-ppx) + jerd) + ((action + (system "awk -f herd-www/notwww.awk %{input-file}")) + AArch64ParseTest + ParseTest + Top_herd))) + (js_of_ocaml + (flags --disable genprim)) + (modules_without_implementation AArch64Sig action arch_herd monad sem XXXMem)) diff --git a/herd/.ocamlformat-ignore b/herd/.ocamlformat-ignore new file mode 100644 index 0000000000..f7dd6e7325 --- /dev/null +++ b/herd/.ocamlformat-ignore @@ -0,0 +1,139 @@ +AArch64Annot.ml +AArch64Arch_herd.ml +AArch64ParseTest.ml +AArch64Sem.ml +AArch64Sig.mli +access.ml +access.mli +action.mli +AllBarrier.ml +AllBarrier.mli +arch_herd.mli +archAction.ml +archExtra_herd.ml +ARMArch_herd.ml +ARMParseTest.ml +ARMParseTest.mli +ARMSem.ml +BellAction.ml +BellArch_herd.ml +BellMem.ml +BellSem.ml +branch.ml +byteSize.ml +CAction.ml +CArch_herd.ml +CAV12.ml +CMem.ml +cmo.ml +cmo.mli +constraints.ml +CParseTest.ml +CParseTest.mli +CSem.ml +debug_herd.ml +debug_herd.mli +dir.ml +dir.mli +dotEdgeAttr.ml +dotEdgeAttr.mli +equivSpec.ml +equivSpec.mli +event.ml +eventsMonad.ml +explicit.ml +explicit.mli +GenericArch_herd.ml +getModel.ml +getModel.mli +graph.ml +graph.mli +handler.ml +handler.mli +herd.ml +itimer.ml +itimer.mli +JavaAction.ml +JavaArch_herd.ml +JAVAParseTest.ml +JAVAParseTest.mli +JavaSem.ml +lexConf_herd.mli +LISAParseTest.ml +LISAParseTest.mli +loader.ml +loader.mli +machAction.ml +machModelChecker.ml +mem.ml +MemCat.ml +memUtils.ml +memUtils.mli +MemWithCav12.ml +MIPSArch_herd.ml +MIPSParseTest.ml +MIPSParseTest.mli +MIPSSem.ml +model.ml +model.mli +modelUtils.ml +modelUtils.mli +monad.mli +noLevelNorTLBI.ml +noLevelNorTLBI.mli +noSemEnv.ml +noSemEnv.mli +optAce.ml +optAce.mli +opts.ml +opts.mli +parseTest.ml +parseTest.mli +partition.ml +partition.mli +PPCArch_herd.ml +PPCParseTest.ml +PPCParseTest.mli +PPCSem.ml +Pretty.ml +prettyConf.ml +prettyConf.mli +prettyUtils.ml +prettyUtils.mli +pteValSets.ml +rc11.ml +restrict.ml +restrict.mli +RISCVArch_herd.ml +RISCVParseTest.ml +RISCVParseTest.mli +RISCVSem.ml +runTest.ml +runTest.mli +SelaEvent.ml +sem.mli +semExtra.ml +show.ml +show.mli +slrc11.ml +speed.ml +speed.mli +splines.ml +splines.mli +test_herd.ml +test_herd.mli +top_herd.ml +valconstraint.ml +variant.ml +variant.mli +view.ml +view.mli +X86_64Arch_herd.ml +X86_64ParseTest.ml +X86_64ParseTest.mli +X86_64Sem.ml +X86Arch_herd.ml +X86ParseTest.ml +X86ParseTest.mli +X86Sem.ml +XXXMem.mli diff --git a/herd/AArch64ASLParseTest.ml b/herd/AArch64ASLParseTest.ml index af5eac6bd2..88a680124b 100644 --- a/herd/AArch64ASLParseTest.ml +++ b/herd/AArch64ASLParseTest.ml @@ -14,8 +14,7 @@ (* "http://www.cecill.info". We also give a copy in LICENSE.txt. *) (****************************************************************************) -module Make(Conf:RunTest.Config)(ModelConfig:MemCat.Config) = struct - +module Make (Conf : RunTest.Config) (ModelConfig : MemCat.Config) = struct let is_morello = Conf.variant Variant.Morello module LexConfig = struct @@ -23,39 +22,35 @@ module Make(Conf:RunTest.Config)(ModelConfig:MemCat.Config) = struct let is_morello = is_morello end - module ArchConfig = SemExtra.ConfigToArchConfig(Conf) + module ArchConfig = SemExtra.ConfigToArchConfig (Conf) - module AArch64ASLValue = - AArch64ASLValue.Make - (struct - let is_morello = is_morello - end) + module AArch64ASLValue = AArch64ASLValue.Make (struct + let is_morello = is_morello + end) - module AArch64ASLArch = - AArch64Arch_herd.Make(ArchConfig)(AArch64ASLValue) + module AArch64ASLArch = AArch64Arch_herd.Make (ArchConfig) (AArch64ASLValue) module AArch64ASLLexParse = struct type instruction = AArch64ASLArch.parsedPseudo type token = AArch64Parser.token - module Lexer = AArch64Lexer.Make(LexConfig) + + module Lexer = AArch64Lexer.Make (LexConfig) + let lexer = Lexer.token let parser = AArch64Parser.main end let run dirty start_time name chan env splitted = let module SemConf = struct - module C = Conf - let dirty = ModelConfig.dirty - let procs_user = ProcsUser.get splitted.Splitter.info - end in - let module AArch64ASLS = - AArch64ASLSem.Make(SemConf)(AArch64ASLValue) in - let module - AArch64ASLM = MemCat.Make(ModelConfig)(AArch64ASLS) in - let module P = - GenParser.Make (Conf) (AArch64ASLArch) (AArch64ASLLexParse) in - let module X = - RunTest.Make (AArch64ASLS) (P) (AArch64ASLM) (Conf) in + module C = Conf + + let dirty = ModelConfig.dirty + let procs_user = ProcsUser.get splitted.Splitter.info + end in + let module AArch64ASLS = AArch64ASLSem.Make (SemConf) (AArch64ASLValue) in + let module AArch64ASLM = MemCat.Make (ModelConfig) (AArch64ASLS) in + let module P = GenParser.Make (Conf) (AArch64ASLArch) (AArch64ASLLexParse) + in + let module X = RunTest.Make (AArch64ASLS) (P) (AArch64ASLM) (Conf) in X.run dirty start_time name chan env splitted end - diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml index bf26dd3594..c0ca1b1219 100644 --- a/herd/AArch64ASLSem.ml +++ b/herd/AArch64ASLSem.ml @@ -156,7 +156,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : let ( ^= ) x e = S_Decl (LDK_Let, LDI_Var x, Some e) |> with_pos in let ( ^^= ) x e = let le_x = LE_Var x |> with_pos in - S_Assign (le_x, e, V1) |> with_pos in + S_Assign (le_x, e, V1) |> with_pos + in let lit v = E_Literal v |> with_pos in let liti i = lit (L_Int (Z.of_int i)) in let litb b = lit (L_Bool b) in @@ -176,49 +177,44 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : in match ii.A.inst with | I_NOP -> - let added = - (* ASL implementation is "return;" that our interpreter rejects, - expecting integer return... *) - ASLBase.stmts_from_string "return 0;" in - Some - ("system/hints/NOP_HI_hints.opn",stmt [added;]) + let added = + (* ASL implementation is "return;" that our interpreter rejects, + expecting integer return... *) + ASLBase.stmts_from_string "return 0;" + in + Some ("system/hints/NOP_HI_hints.opn", stmt [ added ]) | I_B lab -> - let off = tgt2offset ii lab in - Some ("branch/unconditional/immediate/B_only_branch_imm.opn", - stmt - [ - "offset" ^= litbv 64 off; - "_PC" ^^= litbv 64 ii.A.addr; ]) - | I_CBZ (v,rt,lab) - | I_CBNZ (v,rt,lab) as i - -> - let off = tgt2offset ii lab in - let file = - match i with - | I_CBZ _ -> "CBZ_32_compbranch.opn" - | I_CBNZ _ -> "CBNZ_32_compbranch.opn" - | _ -> assert false in - Some - ("branch/conditional/compare/" ^ file, - stmt - [ - "t" ^= reg rt; - "datasize" ^= variant v; - "offset" ^= litbv 64 off; - "_PC" ^^= litbv 64 ii.A.addr; - ]) - | I_BC (c,lab) - -> - let off = tgt2offset ii lab in - Some - ("branch/conditional/cond/B_only_condbranch.opn", - stmt - [ - "offset" ^= litbv 64 off; - "cond" ^= cond c; - "_PC" ^^= litbv 64 ii.A.addr; - ]) - + let off = tgt2offset ii lab in + Some + ( "branch/unconditional/immediate/B_only_branch_imm.opn", + stmt [ "offset" ^= litbv 64 off; "_PC" ^^= litbv 64 ii.A.addr ] ) + | (I_CBZ (v, rt, lab) | I_CBNZ (v, rt, lab)) as i -> + let off = tgt2offset ii lab in + let file = + match i with + | I_CBZ _ -> "CBZ_32_compbranch.opn" + | I_CBNZ _ -> "CBNZ_32_compbranch.opn" + | _ -> assert false + in + Some + ( "branch/conditional/compare/" ^ file, + stmt + [ + "t" ^= reg rt; + "datasize" ^= variant v; + "offset" ^= litbv 64 off; + "_PC" ^^= litbv 64 ii.A.addr; + ] ) + | I_BC (c, lab) -> + let off = tgt2offset ii lab in + Some + ( "branch/conditional/cond/B_only_condbranch.opn", + stmt + [ + "offset" ^= litbv 64 off; + "cond" ^= cond c; + "_PC" ^^= litbv 64 ii.A.addr; + ] ) | I_SWP (v, t, rs, rt, rn) -> Some ( "memory/atomicops/swp/SWP_32_memop.opn", @@ -342,16 +338,17 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : "container_size" ^= liti csz; ]) *) - | I_EXTR (v,rd,rn,rm,imms) -> - Some - ("integer/ins-ext/extract/immediate/EXTR_32_extract.opn", - stmt - [ - "d" ^= reg rd; - "n" ^= reg rn; - "m" ^= reg rm; - "datasize" ^= variant v; - "lsb" ^= liti imms;]) + | I_EXTR (v, rd, rn, rm, imms) -> + Some + ( "integer/ins-ext/extract/immediate/EXTR_32_extract.opn", + stmt + [ + "d" ^= reg rd; + "n" ^= reg rn; + "m" ^= reg rm; + "datasize" ^= variant v; + "lsb" ^= liti imms; + ] ) | I_UBFM (v, rd, rn, immr, imms) | I_SBFM (v, rd, rn, immr, imms) -> let datasize = variant_raw v in let bitvariant = @@ -521,27 +518,27 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : "imm" ^= litbv datasize k; "datasize" ^= liti datasize; ] ) - | I_OP3 - (v,(ASR|LSL|LSR|ROR as op), - rd,rn,OpExt.Reg (rm, s)) - when OpExt.is_no_shift s - -> - let shift_type,fname = - match op with - | ASR -> "ShiftType_ASR","ASRV_32_dp_2src.opn" - | LSL -> "ShiftType_LSL","LSLV_32_dp_2src.opn" - | LSR -> "ShiftType_LSR","LSRV_32_dp_2src.opn" - | ROR -> "ShiftType_ROR","RORV_32_dp_2src.opn" - | _ -> assert false in - Some - ("integer/shift/variable/" ^ fname, - stmt [ - "d" ^= reg rd; - "n" ^= reg rn; - "m" ^= reg rm; - "datasize" ^= variant v; - "shift_type" ^= var shift_type;]) - | ( I_STR (v, rt, rn, MemExt.Reg (_vm, rm, e, s)) + | I_OP3 (v, ((ASR | LSL | LSR | ROR) as op), rd, rn, OpExt.Reg (rm, s)) + when OpExt.is_no_shift s -> + let shift_type, fname = + match op with + | ASR -> ("ShiftType_ASR", "ASRV_32_dp_2src.opn") + | LSL -> ("ShiftType_LSL", "LSLV_32_dp_2src.opn") + | LSR -> ("ShiftType_LSR", "LSRV_32_dp_2src.opn") + | ROR -> ("ShiftType_ROR", "RORV_32_dp_2src.opn") + | _ -> assert false + in + Some + ( "integer/shift/variable/" ^ fname, + stmt + [ + "d" ^= reg rd; + "n" ^= reg rn; + "m" ^= reg rm; + "datasize" ^= variant v; + "shift_type" ^= var shift_type; + ] ) + | ( I_STR (v, rt, rn, MemExt.Reg (_vm, rm, e, s)) | I_LDR (v, rt, rn, MemExt.Reg (_vm, rm, e, s)) ) as i -> let fname = match i with @@ -970,12 +967,12 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : let monads = Seq.map one_pair (ASLE.EventRel.to_seq rel) in Seq.fold_left ( ||| ) (return ()) monads - let tr_execution ii (conc, cs, set_pp, vbpp) = let get_cat_show get x = match StringMap.find_opt x set_pp with | Some e -> get e - | None -> get ESet.empty in + | None -> get ESet.empty + in let () = if _dbg then Printf.eprintf "Translating event structure:\n" in let () = if _dbg then ( @@ -988,9 +985,9 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : in let events = get_cat_show ESet.to_seq "AArch64" in let is_data = - let data_set = - get_cat_show Misc.identity "AArch64_DATA" in - fun e -> ESet.mem e data_set in + let data_set = get_cat_show Misc.identity "AArch64_DATA" in + fun e -> ESet.mem e data_set + in let () = if _dbg then Printf.eprintf "\t- events: " in let event_list = List.of_seq events in let event_to_monad_map = @@ -1019,30 +1016,30 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : | ASLS.Act.Access (Dir.W, ASLS.A.Location_reg (_, ASLBase.ArchReg reg), v, _, _) -> - let v = tr_v v in - let () = - if _dbg then - Printf.eprintf "Recording %s <- %s\n%!" - (AArch64Base.pp_reg reg) (A.V.pp_v v) in - (reg,v)::bds - | ASLS.Act.Access (Dir.W, loc , v, _, _) - -> + let v = tr_v v in + let () = + if _dbg then + Printf.eprintf "Recording %s <- %s\n%!" + (AArch64Base.pp_reg reg) (A.V.pp_v v) + in + (reg, v) :: bds + | ASLS.Act.Access (Dir.W, loc, v, _, _) -> if _dbg then - Printf.eprintf - "Not recorded in B.Next: %s <- %s\n" - (ASLS.A.pp_location loc) (ASLS.A.V.pp_v v) ; + Printf.eprintf "Not recorded in B.Next: %s <- %s\n" + (ASLS.A.pp_location loc) (ASLS.A.V.pp_v v); bds - | _ -> bds in + | _ -> bds + in let bds = List.fold_left one_event [] event_list in - let finals = get_cat_show Misc.identity "AArch64Finals" in + let finals = get_cat_show Misc.identity "AArch64Finals" in let pc = - let n_pc = (* Count writes to PC *) + let n_pc = + (* Count writes to PC *) List.fold_left - (fun c (r,_) -> - match r with - | AArch64Base.PC -> c+1 - | _ -> c) - 0 bds in + (fun c (r, _) -> + match r with AArch64Base.PC -> c + 1 | _ -> c) + 0 bds + in (* Branching instructions all generate one, initial, * PC assignement and a second PC assignement * that gives the branch target. This applies even @@ -1058,15 +1055,17 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) : (fun e r -> match e.ASLE.action with | ASLS.Act.Access - (Dir.W, - ASLS.A.Location_reg - (_, - ASLBase.ArchReg AArch64Base.PC), v, _, _) -> - Some (tr_v v) + ( Dir.W, + ASLS.A.Location_reg (_, ASLBase.ArchReg AArch64Base.PC), + v, + _, + _ ) -> + Some (tr_v v) | _ -> r) - finals None in + finals None + in match Misc.seq_opt A.V.as_int pc with - | Some v -> B.Jump (B.Addr v,bds) + | Some v -> B.Jump (B.Addr v, bds) | None -> B.Next bds in let () = diff --git a/herd/ASLAction.ml b/herd/ASLAction.ml index 3bbd2919d2..785009feda 100644 --- a/herd/ASLAction.ml +++ b/herd/ASLAction.ml @@ -52,13 +52,10 @@ module Make (A : S) = struct let mk_init_write loc sz v = Access (W, loc, v, sz, AArch64Annot.N) let pp_action = function - | Access (d, l, v, _sz,a) -> - Printf.sprintf "%s%s=%s%s" - (pp_dirn d) (A.pp_location l) (V.pp false v) + | Access (d, l, v, _sz, a) -> + Printf.sprintf "%s%s=%s%s" (pp_dirn d) (A.pp_location l) (V.pp false v) (let open AArch64Annot in - match a with - | N -> "" - | _ -> AArch64Annot.pp a) + match a with N -> "" | _ -> AArch64Annot.pp a) | Barrier b -> A.pp_barrier_short b | TooFar msg -> Printf.sprintf "TooFar:%s" msg | NoAction -> "" @@ -157,14 +154,8 @@ module Make (A : S) = struct let annot_in_list _str _act = false (* Barriers *) - let is_barrier = function - | Barrier _ -> true - | _ -> false - - let barrier_of = function - | Barrier b -> Some b - | _ -> None - + let is_barrier = function Barrier _ -> true | _ -> false + let barrier_of = function Barrier b -> Some b | _ -> None let same_barrier_id _a1 _a2 = assert false (* Commits *) @@ -188,11 +179,9 @@ module Make (A : S) = struct let simplify_vars_in_action soln a = match a with | Access (d, l, v, sz, a) -> - Access - (d, A.simplify_vars_in_loc soln l, - V.simplify_var soln v, sz, a) + Access (d, A.simplify_vars_in_loc soln l, V.simplify_var soln v, sz, a) | Barrier _ | TooFar _ | NoAction -> a end -module FakeModuleForCheckingSignatures (A : S) : Action.S - with module A = A = Make (A) +module FakeModuleForCheckingSignatures (A : S) : Action.S with module A = A = + Make (A) diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index 9b394bd11b..5d6a537eae 100644 --- a/herd/ASLSem.ml +++ b/herd/ASLSem.ml @@ -475,13 +475,13 @@ module Make (C : Config) = struct let loc_pc ii = A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.PC) - let read_pc (ii,poi) () = + let read_pc (ii, poi) () = read_loc MachSize.Quad (loc_pc ii) aneutral (use_ii_with_poi ii poi) - let write_pc (ii,poi) v_m = + let write_pc (ii, poi) v_m = let* v = v_m >>= to_int_unsigned in - write_loc MachSize.Quad (loc_pc ii) - v aneutral (use_ii_with_poi ii poi) >>! [] + write_loc MachSize.Quad (loc_pc ii) v aneutral (use_ii_with_poi ii poi) + >>! [] let do_read_memory (ii, poi) addr_m datasize_m an = let* addr = addr_m and* datasize = datasize_m in @@ -639,18 +639,18 @@ module Make (C : Config) = struct let bv_64 = bv_lit 64 in let t_named x = T_Named x |> with_pos in [ -(* Fences *) + (* Fences *) p0 "primitive_isb" (primitive_isb ii_env); p2 "primitive_dmb" ("d", integer) ("t", integer) (primitive_dmb ii_env); p2 "primitive_dsb" ("d", integer) ("t", integer) (primitive_dsb ii_env); -(* Registers *) + (* Registers *) p1r "read_register" ("reg", reg) ~returns:bv_64 (read_register ii_env); p2 "write_register" ("data", bv_64) ("reg", reg) (write_register ii_env); p0r "read_pc" ~returns:bv_64 (read_pc ii_env); p1 "write_pc" ("data", bv_64) (write_pc ii_env); p0r "SP_EL0" ~returns:bv_64 (read_sp ii_env); p1 "SP_EL0" ("data", bv_64) (write_sp ii_env); -(* Memory *) + (* Memory *) p2r "read_memory" ("addr", bv_64) ("size", integer) ~returns:bv_64 (read_memory ii_env); p3r "read_memory_gen" ("addr", bv_64) ("size", integer) @@ -663,8 +663,8 @@ module Make (C : Config) = struct ("data", bv_var "size") ("accdesc", t_named "AccessDescriptor") (write_memory_gen ii_env); -(* Translations *) - p1r "UInt" + (* Translations *) + p1r "UInt" ~parameters:[ ("N", None) ] ("x", bv_var "N") ~returns:integer uint; @@ -672,7 +672,7 @@ module Make (C : Config) = struct ~parameters:[ ("N", None) ] ("x", bv_var "N") ~returns:integer sint; -(* Misc *) + (* Misc *) p0r "ProcessorID" ~returns:integer (processor_id ii_env); p2r "CanPredictFrom" ~parameters:[ ("N", None) ] diff --git a/herd/dune b/herd/dune index bcf1b55ea0..5f59b0c658 100644 --- a/herd/dune +++ b/herd/dune @@ -1,11 +1,12 @@ (dirs :standard \ tests libdir) -(rule (copy ../Version.ml Version.ml)) +(rule + (copy ../Version.ml Version.ml)) (ocamllex lexConf_herd) (executable - (name herd) - (public_name herd7) - (libraries unix herdtools) - (modules_without_implementation AArch64Sig action arch_herd monad sem XXXMem)) + (name herd) + (public_name herd7) + (libraries unix herdtools) + (modules_without_implementation AArch64Sig action arch_herd monad sem XXXMem)) diff --git a/internal/.ocamlformat b/internal/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/internal/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/jingle/.ocamlformat b/jingle/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/jingle/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/jingle/dune b/jingle/dune index 3b3ef26020..6e6deb7fb0 100644 --- a/jingle/dune +++ b/jingle/dune @@ -1,10 +1,10 @@ -(rule (copy ../Version.ml Version.ml)) +(rule + (copy ../Version.ml Version.ml)) + (ocamllex callMap parseMap) + (executables - (names - jingle gen_theme - ) - (public_names jingle7 gen_theme7) - (libraries herdtools str) - (modules_without_implementation ) -) + (names jingle gen_theme) + (public_names jingle7 gen_theme7) + (libraries herdtools str) + (modules_without_implementation)) diff --git a/lib/.ocamlformat-ignore b/lib/.ocamlformat-ignore new file mode 100644 index 0000000000..d29da654f9 --- /dev/null +++ b/lib/.ocamlformat-ignore @@ -0,0 +1,240 @@ +AArch64Base.ml +AArch64Instr.ml +AArch64Lexer.mli +AArch64Op.ml +AArch64PteVal.ml +AArch64PteVal.mli +AArch64Value.ml +accessModes.ml +archBase.mli +archDump.mli +archOp.ml +Archs.ml +Archs.mli +archUtils.ml +archUtils.mli +argUtils.ml +argUtils.mli +ARMBase.ml +ARMLexer.mli +AST.mli +ASTUtils.ml +ASTUtils.mli +baseUint64.ml +baseUint128.ml +BellBase.ml +BellCheck.ml +BellCheck.mli +BellInfo.ml +BellInfo.mli +BellInterpreter.ml +BellLexer.mli +BellModel.ml +BellModel.mli +BellName.ml +BellName.mli +branchTarget.ml +branchTarget.mli +cacheType.mli +capabilityScalar.ml +CapabilityValue.ml +CAst.mli +CAstUtils.ml +CAstUtils.mli +CBase.ml +CGenParser_lib.ml +checkName.ml +checkName.mli +CLexer.mli +constant.ml +constant.mli +constrGen.ml +constrGen.mli +coreDumper.ml +CTestHash.ml +CTestHash.mli +CType.ml +CType.mli +dirtyBit.mli +dumpCAst.ml +dumpCAst.mli +dumpUtils.ml +dumpUtils.mli +endian.ml +endian.mli +extArray.ml +extArray.mli +fault.ml +fault.mli +faultType.ml +faultType.mli +flag.ml +flag.mli +genParser.ml +genParser.mli +genParserUtils.ml +genParserUtils.mli +hashcons.ml +hashcons.mli +hint.ml +hint.mli +innerRel.ml +innerRel.mli +InnerTransRel.ml +InnerTransRel.mli +instr.ml +instr.mli +instrLit.ml +instrLit.mli +int32Constant.ml +int32Scalar.ml +int32Value.ml +int64Constant.ml +int64Scalar.ml +int64Value.ml +int128.ml +int128Constant.ml +int128Scalar.ml +int128Value.ml +interpreter.ml +IntMap.ml +IntMap.mli +intOrd.ml +intOrd.mli +IntSet.ml +IntSet.mli +JavaAst.ml +JavaBase.ml +JavaGenParser_lib.ml +JavaLexer.mli +label.ml +label.mli +lexHint.mli +lexItem.ml +lexItem.mli +lexMisc.ml +lexMisc.mli +lexOutMapping.mli +lexRename.mli +lexScan.mli +lexSplit.mli +lexUtils.mli +location.ml +locationsItem.ml +locationsItem.mli +machSize.ml +machSize.mli +MakeAArch64Base.ml +memOrder.ml +memOrder.mli +memOrderOrAnnot.ml +memOrderOrAnnot.mli +memoryType.ml +memoryType.mli +metaConst.ml +metaConst.mli +MIPSBase.ml +MIPSLexer.mli +misc.ml +misc.mli +miscParser.ml +miscParser.mli +modelLexer.mli +modelOption.ml +modelOption.mli +myLib.ml +myLib.mli +myMap.ml +mySet.ml +mySet.mli +mySys.ml +mySys.mli +name.mli +names.ml +names.mli +op.ml +op.mli +outMapping.ml +outMapping.mli +outputAddress.ml +outputAddress.mli +outStd.ml +outStd.mli +outTar.ml +outTar.mli +outTests.mli +parsedConstant.ml +parsedConstant.mli +parsedPteVal.ml +parsedPteVal.mli +parseModel.ml +parseModel.mli +parseTag.ml +parseTag.mli +pos.ml +pos.mli +PPCBase.ml +PPCLexer.mli +PPMode.mli +precision.ml +precision.mli +proc.ml +proc.mli +procsUser.ml +procsUser.mli +pseudo.ml +pteVal.ml +pteVal.mli +rbit.ml +rbit.mli +readBell.ml +readNames.ml +readNames.mli +rel.ml +rel.mli +RISCVBase.ml +RISCVLexer.mli +scalar.mli +scopeLexer.mli +sign.mli +simpleDumper.ml +splitter.mli +stateLexer.mli +StringMap.ml +StringMap.mli +StringRel.ml +StringRel.mli +StringSet.ml +StringSet.mli +symbConstant.ml +symbConstant.mli +symbReg.ml +symbReg.mli +symbValue.ml +symbValue.mli +tar.ml +tar.mli +tblRename.ml +tblRename.mli +testHash.ml +testHash.mli +testType.ml +testType.mli +testVariant.ml +testVariant.mli +txtLoc.ml +txtLoc.mli +uint.ml +uint.mli +uint128Scalar.ml +uint128Value.ml +value.mli +warn.ml +warn.mli +X86_64Base.ml +X86_64Lexer.mli +X86Base.ml +X86Lexer.mli +tests/dune +tests/int128_test.ml +tests/uint_test.ml diff --git a/lib/AArch64ASLValue.ml b/lib/AArch64ASLValue.ml index 5fecd74f81..2e54e45988 100644 --- a/lib/AArch64ASLValue.ml +++ b/lib/AArch64ASLValue.ml @@ -18,17 +18,20 @@ module Make (C : sig val is_morello : bool end) : Value.AArch64ASL = struct if C.is_morello then - Warn.fatal "-variant asl and -variant morello are not conmpatible" ; + Warn.fatal "-variant asl and -variant morello are not conmpatible" + module AArch64I = AArch64Instr.Make (C) + module ASLScalar = struct include ASLScalar let printable = function - | S_BitVector bv -> S_Int (Asllib.Bitvector.printable bv) + | S_BitVector bv -> S_Int (Asllib.Bitvector.printable bv) | S_Bool b -> S_Int (if b then Z.one else Z.zero) | S_Int i -> S_Int (printable_z i) end + module AArch64Cst = SymbConstant.Make (ASLScalar) (AArch64PteVal) (AArch64I) - module AArch64Op = AArch64Op.Make(ASLScalar)(ASLOp) + module AArch64Op = AArch64Op.Make (ASLScalar) (ASLOp) include SymbValue.Make (AArch64Cst) (AArch64Op) end diff --git a/lib/ASLOp.ml b/lib/ASLOp.ml index b9a8f17c06..87d68a3809 100644 --- a/lib/ASLOp.ml +++ b/lib/ASLOp.ml @@ -164,17 +164,16 @@ let do_op1 op cst = | Constant.Concrete s -> let* s' = ASLScalar.try_extract_slice s positions in return_concrete s' - | Constant.Symbolic x -> + | Constant.Symbolic x -> ( if Misc.list_eq ( = ) positions all_64_bits_positions then Some (Constant.Symbolic x) - else begin - (* MSB of virtual address is assumed null. - * This hypothesis is reasonable for user programs, - * less so for kernel code. *) + else + (* MSB of virtual address is assumed null. + * This hypothesis is reasonable for user programs, + * less so for kernel code. *) match positions with - | [63] -> Some (Constant.Concrete ASLScalar.zeros_size_one) - | _ -> None - end + | [ 63 ] -> Some (Constant.Concrete ASLScalar.zeros_size_one) + | _ -> None) | _ -> None) | BoolNot -> ( let open Constant in diff --git a/lib/ASLScalar.ml b/lib/ASLScalar.ml index b9ff52fe8f..ce847d79a7 100644 --- a/lib/ASLScalar.ml +++ b/lib/ASLScalar.ml @@ -47,32 +47,29 @@ let zeros sz = S_BitVector (BV.zeros sz) * 0xffffffffffffffff and not as 0x-1 *) -let z63 = Z.shift_left Z.one (MachSize.nbits machsize-1) +let z63 = Z.shift_left Z.one (MachSize.nbits machsize - 1) let z64 = Z.shift_left Z.one (MachSize.nbits machsize) - let norm_unsigned z = if Z.sign z < 0 then Z.add z z64 else z + let norm_signed z = let z = Z.erem z z64 in - if Z.geq z z63 then Z.sub z z64 - else z + if Z.geq z z63 then Z.sub z z64 else z let pp hexa = function | S_Int i -> - if hexa then norm_unsigned i |> Z.format "%x" - else Z.format "%d" i + if hexa then norm_unsigned i |> Z.format "%x" else Z.format "%d" i | S_Bool true -> "TRUE" | S_Bool false -> "FALSE" | S_BitVector bv -> BV.to_string bv let pp_unsigned hexa = function | S_Int i -> - let i = norm_unsigned i in - if hexa then "0x" ^ Z.format "%x" i else Z.format "%d" i + let i = norm_unsigned i in + if hexa then "0x" ^ Z.format "%x" i else Z.format "%d" i | S_Bool true -> "TRUE" | S_Bool false -> "FALSE" | S_BitVector bv -> BV.to_string bv - let of_string s = try S_Int (Z.of_string s) with Invalid_argument _ -> ( @@ -84,11 +81,10 @@ let of_string s = let of_int i = S_Int (Z.of_int i) let to_int = function - | S_Int i -> Z.to_int (norm_signed i) + | S_Int i -> Z.to_int (norm_signed i) | S_Bool true -> 1 | S_Bool false -> 0 - | S_BitVector bv -> - BV.to_int_signed bv + | S_BitVector bv -> BV.to_int_signed bv let of_int64 i = S_Int (Z.of_int64 i) @@ -128,16 +124,13 @@ let zop_expressive pp_op op s1 s2 = | S_BitVector bv1, S_Int i2 -> let sz = BV.length bv1 in S_BitVector (bv1 |> BV.to_z_unsigned |> op i2 |> BV.of_z sz) - | S_BitVector bv1, S_BitVector bv2 - when BV.length bv1=BV.length bv2 - -> - let z1 = BV.to_z_unsigned bv1 - and z2 = BV.to_z_unsigned bv2 in - let z = op z1 z2 in - S_BitVector (BV.of_z (BV.length bv1) z) + | S_BitVector bv1, S_BitVector bv2 when BV.length bv1 = BV.length bv2 -> + let z1 = BV.to_z_unsigned bv1 and z2 = BV.to_z_unsigned bv2 in + let z = op z1 z2 in + S_BitVector (BV.of_z (BV.length bv1) z) | _ -> - Warn.fatal "ASLScalar invalid op: %s %s %s" - (pp false s1) pp_op (pp false s2) + Warn.fatal "ASLScalar invalid op: %s %s %s" (pp false s1) pp_op + (pp false s2) let add = zop_expressive "add" Z.add and sub = zop_expressive "sub" Z.sub @@ -146,12 +139,11 @@ let zop pp_op op s1 s2 = match (s1, s2) with | S_Int i1, S_Int i2 -> S_Int (op i1 i2) | _ -> - Warn.fatal "ASLScalar invalid op: %s %s %s" - pp_op - (pp false s1) + Warn.fatal "ASLScalar invalid op: %s %s %s" pp_op (pp false s1) (pp false s2) let asl_rem z1 z2 = Z.sub z1 (Z.mul z2 (Z.fdiv z1 z2)) + let mul = zop "mul" Z.mul and div = zop "div" Z.divexact and rem = zop "rem" asl_rem @@ -205,11 +197,9 @@ let shift_right_arithmetic = function let addk = function | S_Int i -> fun k -> S_Int (Z.add i (Z.of_int k)) | S_BitVector bv -> - fun k -> - S_BitVector - (BV.to_z_unsigned bv - |> Z.add (Z.of_int k) - |> BV.of_z (BV.length bv)) + fun k -> + S_BitVector + (BV.to_z_unsigned bv |> Z.add (Z.of_int k) |> BV.of_z (BV.length bv)) | s1 -> Warn.fatal "ASLScalar invalid op: %s addk" (pp false s1) let bit_at i1 = function @@ -284,7 +274,7 @@ let try_extract_slice s positions = else Some (S_BitVector (BV.extract_slice bv positions)) | S_Int i -> if Z.equal Z.zero i then - Some (S_BitVector (BV.zeros (List.length positions) )) + Some (S_BitVector (BV.zeros (List.length positions))) else if Z.equal Z.minus_one i then Some (S_BitVector (BV.ones (List.length positions))) else if List.exists (( <= ) 64) positions then None @@ -311,7 +301,5 @@ let try_write_slice positions dst src = let empty = S_BitVector BV.empty let zeros_size_one = S_BitVector (BV.zeros 1) - let printable_z z = norm_signed z - -let rbit _ _ = Warn.fatal "ASLScalar.rbit non-existent" +let rbit _ _ = Warn.fatal "ASLScalar.rbit non-existent" diff --git a/lib/ASLValue.ml b/lib/ASLValue.ml index 0dbd93beff..f942a710bd 100644 --- a/lib/ASLValue.ml +++ b/lib/ASLValue.ml @@ -33,7 +33,9 @@ module ASLScalar = struct include ASLScalar + let printable c = c end + module ASLConstant = SymbConstant.Make (ASLScalar) (PteVal.ASL) (ASLBase.Instr) module V = SymbValue.Make (ASLConstant) (ASLOp) diff --git a/lib/dune b/lib/dune index 067ed0c4a6..57904e8c20 100644 --- a/lib/dune +++ b/lib/dune @@ -1,36 +1,67 @@ -(ocamllex AArch64Lexer ARMLexer BellLexer CLexer lexHint lexOutMapping lexRename lexSplit lexUtils MIPSLexer modelLexer PPCLexer RISCVLexer scopeLexer splitter stateLexer X86Lexer X86_64Lexer echo dirtyBit cacheType lexScan JavaLexer) +(ocamllex AArch64Lexer ARMLexer BellLexer CLexer lexHint lexOutMapping + lexRename lexSplit lexUtils MIPSLexer modelLexer PPCLexer RISCVLexer + scopeLexer splitter stateLexer X86Lexer X86_64Lexer echo dirtyBit cacheType + lexScan JavaLexer) +(menhir + (modules PPCParser) + (flags --fixed-exception)) +(menhir + (modules ARMParser) + (flags --fixed-exception)) -(menhir (modules PPCParser) (flags --fixed-exception)) -(menhir (modules ARMParser) (flags --fixed-exception)) -(menhir (modules MIPSParser) (flags --fixed-exception)) -(menhir (modules X86Parser) (flags --fixed-exception)) -(menhir (modules X86_64Parser) (flags --fixed-exception)) -(menhir (modules modelParser) (flags --fixed-exception)) -(menhir (modules RISCVParser) (flags --fixed-exception)) -(menhir (modules JavaParser) (flags --fixed-exception)) -(menhir (modules stateParser) (flags --explain --fixed-exception)) +(menhir + (modules MIPSParser) + (flags --fixed-exception)) -(menhir (modules procRules scopeRules BellExtraRules AArch64Parser) - (merge_into AArch64Parser) - (flags --fixed-exception)) +(menhir + (modules X86Parser) + (flags --fixed-exception)) -(menhir (modules procRules scopeRules BellExtraRules LISAParser) - (merge_into LISAParser) - (flags --fixed-exception)) +(menhir + (modules X86_64Parser) + (flags --fixed-exception)) -(menhir (modules scopeRules scopeParser) - (merge_into scopeParser) - (flags --fixed-exception)) +(menhir + (modules modelParser) + (flags --fixed-exception)) -(menhir (modules scopeRules BellExtraRules CParser) - (merge_into CParser) - (flags --fixed-exception)) +(menhir + (modules RISCVParser) + (flags --fixed-exception)) + +(menhir + (modules JavaParser) + (flags --fixed-exception)) + +(menhir + (modules stateParser) + (flags --explain --fixed-exception)) + +(menhir + (modules procRules scopeRules BellExtraRules AArch64Parser) + (merge_into AArch64Parser) + (flags --fixed-exception)) + +(menhir + (modules procRules scopeRules BellExtraRules LISAParser) + (merge_into LISAParser) + (flags --fixed-exception)) + +(menhir + (modules scopeRules scopeParser) + (merge_into scopeParser) + (flags --fixed-exception)) + +(menhir + (modules scopeRules BellExtraRules CParser) + (merge_into CParser) + (flags --fixed-exception)) (library (name herdtools) (wrapped false) (libraries str asllib zarith) - (modules_without_implementation sign outTests AST CAst Scalar archBase archDump - PPMode name value)) + (modules_without_implementation sign outTests AST CAst Scalar archBase + archDump PPMode name value)) diff --git a/litmus/.ocamlformat b/litmus/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/litmus/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/litmus/dune b/litmus/dune index 2c9f20b763..8850bc70e0 100644 --- a/litmus/dune +++ b/litmus/dune @@ -1,11 +1,12 @@ -(rule (copy ../Version.ml Version.ml)) -(ocamllex lexAffinity lexConf_litmus lexFmt lexHaveRcu prefetch showcode lexO infoAlign) -(executables - (names - litmus klitmus - ) - (public_names litmus7 klitmus7) - (libraries herdtools) - (modules_without_implementation answer arch_litmus compCondUtils emitPrintf fmt pseudoAbstract target LISATarget XXXCompile_litmus) +(rule + (copy ../Version.ml Version.ml)) + +(ocamllex lexAffinity lexConf_litmus lexFmt lexHaveRcu prefetch showcode lexO + infoAlign) -) +(executables + (names litmus klitmus) + (public_names litmus7 klitmus7) + (libraries herdtools) + (modules_without_implementation answer arch_litmus compCondUtils emitPrintf + fmt pseudoAbstract target LISATarget XXXCompile_litmus)) diff --git a/tools/.ocamlformat b/tools/.ocamlformat new file mode 100644 index 0000000000..4d6556cb8b --- /dev/null +++ b/tools/.ocamlformat @@ -0,0 +1 @@ +disable = true diff --git a/tools/dune b/tools/dune index 4e4bb649ae..469520d927 100644 --- a/tools/dune +++ b/tools/dune @@ -1,13 +1,18 @@ -(rule (copy ../Version.ml Version.ml)) -(ocamllex lexHashLog lexInterval lexLog_tools lexName mflags mheader splitdot trTrue bento lexMiaou) +(rule + (copy ../Version.ml Version.ml)) + +(ocamllex lexHashLog lexInterval lexLog_tools lexName mflags mheader splitdot + trTrue bento lexMiaou) (executables - (names - mfind moutcomes splitcond mshowhashes mlog2cond mflags mdiag recond mcycles mmixer knames mdiff mcmp madd mtopos mfilter mapply mcompare mhash mrcu mprog mnames ksort mobserved msort msum mselect mcond mproj rehash splitdot mlock mtrue mlisa2c cat2html mlog2name mcat2includes bento miaou - ) - (public_names - mfind7 moutcomes7 splitcond7 mshowhashes7 mlog2cond7 mflags7 mdiag7 recond7 mcycles7 mmixer7 knames7 mdiff7 mcmp7 madd7 mtopos7 mfilter7 mapply7 mcompare7 mhash7 mrcu7 mprog7 mnames7 ksort7 mobserved7 msort7 msum7 mselect7 mcond7 mproj7 rehash7 splitdot7 mlock7 mtrue7 mlisa2c7 cat2html7 mlog2name7 mcat2includes7 bento miaou7 - ) - (libraries herdtools unix str) - (modules_without_implementation arch_tools) -) + (names mfind moutcomes splitcond mshowhashes mlog2cond mflags mdiag recond + mcycles mmixer knames mdiff mcmp madd mtopos mfilter mapply mcompare mhash + mrcu mprog mnames ksort mobserved msort msum mselect mcond mproj rehash + splitdot mlock mtrue mlisa2c cat2html mlog2name mcat2includes bento miaou) + (public_names mfind7 moutcomes7 splitcond7 mshowhashes7 mlog2cond7 mflags7 + mdiag7 recond7 mcycles7 mmixer7 knames7 mdiff7 mcmp7 madd7 mtopos7 + mfilter7 mapply7 mcompare7 mhash7 mrcu7 mprog7 mnames7 ksort7 mobserved7 + msort7 msum7 mselect7 mcond7 mproj7 rehash7 splitdot7 mlock7 mtrue7 + mlisa2c7 cat2html7 mlog2name7 mcat2includes7 bento miaou7) + (libraries herdtools unix str) + (modules_without_implementation arch_tools))