diff --git a/lib/check.ml b/lib/check.ml index e22d0889..dfd97c60 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1172,6 +1172,10 @@ let tyvar_in_scope env n = let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t = let loc = t.Ast.tloc in match t.Ast.t with + | Ast.Tname "const" -> + fail loc + "const is not a type on its own — it marks one that can only be read, \ + as in [const u8] or (Ptr const u8)" | Ast.Tname n -> resolve_name env ~seen loc n | Ast.Tslice (c, e) -> Types.Slice ((if c then Types.Const else Types.Mut), resolve env ~seen e) @@ -1209,9 +1213,16 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t = if env' then Types.Fn (ps, r) else Types.CFn (ps, r) | Ast.Tapp (name, args) -> (match name, args with - | "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a) + | "Ptr", [ a ] -> Types.Ptr (Types.Mut, resolve env ~seen a) + (* The pointer beside [[const T]]: nothing is written through it, and a + (Ptr T) converts to one. [const] cannot name a type, so this reading + is the only one the two arguments have. *) + | "Ptr", [ { Ast.t = Ast.Tname "const"; _ }; a ] -> + Types.Ptr (Types.Const, resolve env ~seen a) | "Option", [ a ] -> Types.Option (resolve env ~seen a) - | ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name + | "Ptr", _ -> fail loc "a pointer type is (Ptr T), or (Ptr const T) for one \ + nothing is written through" + | "Option", _ -> fail loc "(Option T) takes exactly one type" | "Vec", [ a ] -> let e = resolve env ~seen a in (* A Vec of a Vec used to be refused here, and the refusal named two @@ -1865,7 +1876,9 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t) | Types.Slice (m, p), Types.Slice (m', a) when m = m' || (ro && m = Types.Const) -> bind_ty ~ro:(m = Types.Const) subst p a - | Types.Ptr p, Types.Ptr a + | Types.Ptr (m, p), Types.Ptr (m', a) + when m = m' || (ro && m = Types.Const) -> + bind_ty ~ro:(m = Types.Const) subst p a | Types.Vec p, Types.Vec a | Types.Option p, Types.Option a -> inner p a | Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && inner p a @@ -1912,7 +1925,7 @@ let rec subst_ty subst (t : Types.t) = | Types.Slice (m, e) -> Types.Slice (m, subst_ty subst e) | Types.Array (n, e) -> Types.Array (n, subst_ty subst e) | Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v) - | Types.Ptr e -> Types.Ptr (subst_ty subst e) + | Types.Ptr (m, e) -> Types.Ptr (m, subst_ty subst e) | Types.Vec e -> Types.Vec (subst_ty subst e) | Types.Option e -> Types.Option (subst_ty subst e) | Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r) @@ -1924,7 +1937,7 @@ let rec subst_ty subst (t : Types.t) = let rec generic_ty (t : Types.t) = match t with | Types.Var _ -> true - | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e | Types.Option e -> generic_ty e | Types.Map (k, v) -> generic_ty k || generic_ty v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -1938,7 +1951,7 @@ let rec generic_ty (t : Types.t) = let rec reaches_dyn (t : Types.t) = match t with | Types.Dyn -> true - | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e | Types.Option e -> reaches_dyn e | Types.Map (k, v) -> reaches_dyn k || reaches_dyn v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -1982,7 +1995,8 @@ let rec mangle_ty (t : Types.t) = | Types.Slice (Types.Const, e) -> "cslice-" ^ mangle_ty e | Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (mangle_ty e) | Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v) - | Types.Ptr e -> "ptr-" ^ mangle_ty e + | Types.Ptr (Types.Mut, e) -> "ptr-" ^ mangle_ty e + | Types.Ptr (Types.Const, e) -> "cptr-" ^ mangle_ty e | Types.Vec e -> "vec-" ^ mangle_ty e | Types.Option e -> "opt-" ^ mangle_ty e | Types.Fn (ps, r) -> @@ -2023,7 +2037,7 @@ let rec occurs_in ~needle (t : Types.t) = Types.equal needle t || match t with - | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e | Types.Option e -> occurs_in ~needle e | Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -2164,11 +2178,11 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc = in Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields }; let ety = Types.Named ename in - let eslot = fresh_slot fctx (Types.Ptr ety) in + let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in let binds = List.mapi (fun i (_, ((b : binding), slot)) -> - let p = mk loc (Types.Ptr ety) (Tast.Local eslot) in + let p = mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Local eslot) in (slot, mk loc b.bty (Tast.Field (mk loc ety (Tast.Deref p), i)))) caught in @@ -2183,7 +2197,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc = caught)) in prefix, Some eslot, Some (mslot, make), - Some (mk loc (Types.Ptr ety) (Tast.Addr (Tast.Plocal mslot))) + Some (mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Addr (Tast.Plocal mslot))) (* A source location as a value, for a runtime trap that has to name the site rather than the runtime. The bounds and slice traps get theirs from [Emit], @@ -2202,6 +2216,8 @@ let rec const_reached (e : Tast.expr) = | Tast.Prim (Tast.At, target :: idx) -> const_steps (const_reached target) target.Tast.ty (List.length idx) | Tast.Field (target, _) -> const_reached target + | Tast.Deref p -> + (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None) | _ -> None (* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *) @@ -2214,14 +2230,27 @@ and const_steps ro (ty : Types.t) n = | Types.Array (_, t) -> const_steps ro t (n - 1) | _ -> ro -(* A store, or an [addr], through a read-only view. *) +(* A store through a read-only view: a [[const T]] or a (Ptr const T). *) let refuse_const_place loc (view : Types.t) = - let elem = match view with Types.Slice (_, t) -> t | t -> t in - Loc.failk "check/store-through-const" loc - "this writes through a %s, which can only be read, so the element is a \ - value and not a place. Write into a slice that can be written: \ - (slice (into v (vec-new %s))) copies v's elements into one" - (Types.to_string view) (Types.to_string elem) + match view with + | Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) -> + Loc.failk "check/store-through-const" loc + "this changes the %s behind a %s, which can only be read through. A \ + container that has to change is handed over as a (Ptr %s)" + (Types.to_string t) (Types.to_string view) (Types.to_string t) + | Types.Ptr (_, t) -> + Loc.failk "check/store-through-const" loc + "this writes through a %s, which can only be read, so what it points at \ + is a value and not a place. (deref p) copies the %s out, and the copy \ + can be written" + (Types.to_string view) (Types.to_string t) + | _ -> + let elem = match view with Types.Slice (_, t) -> t | t -> t in + Loc.failk "check/store-through-const" loc + "this writes through a %s, which can only be read, so the element is a \ + value and not a place. Write into a slice that can be written: \ + (slice (into v (vec-new %s))) copies v's elements into one" + (Types.to_string view) (Types.to_string elem) (* The runtime entry points that change a Vec or a Map, which the backends hand the container's address. An element of a [[const (Vec T)]], or a field @@ -2358,7 +2387,7 @@ let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, [] (* The address of an expression, place or not: the type-erased runtime takes the element [push] copies by pointer. *) let addr_of loc (e : Tast.expr) = - mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ])) + mk loc (Types.Ptr (Types.Mut, e.Tast.ty)) (Tast.Prim (Tast.AddrOf, [ e ])) (* ── Where a rendered number's bytes live ────────────────────────────── @@ -3015,7 +3044,8 @@ let rec thick_enc (t : Types.t) = | Types.Var v -> "y" ^ atom v | Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e | Types.Slice (Types.Const, e) -> "k" ^ thick_enc e - | Types.Ptr e -> "p" ^ thick_enc e + | Types.Ptr (Types.Mut, e) -> "p" ^ thick_enc e + | Types.Ptr (Types.Const, e) -> "q" ^ thick_enc e | Types.Vec e -> "v" ^ thick_enc e | Types.Option e -> "o" ^ thick_enc e | Types.Array (n, e) -> Printf.sprintf "a%Ld-%s" n (thick_enc e) @@ -3060,7 +3090,7 @@ let thick_thunk env loc ps r = that never reads it costs one store the optimiser drops. *) let declare_env ctx = function | Some _ as s -> s - | None -> Some (fresh_slot ctx (Types.Ptr Types.Unit)) + | None -> Some (fresh_slot ctx (Types.Ptr (Types.Mut, Types.Unit))) let numeric_note ~(want : Types.t) ~(got : Types.t) = if not (Types.is_numeric want && Types.is_numeric got) then "" @@ -3095,6 +3125,14 @@ let const_note ~(want : Types.t) ~(got : Types.t) = through it, the %s can be declared %s instead" (Types.to_string got) (Types.to_string want) copy (Types.to_string want) (Types.to_string want) (Types.to_string got) + | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e') + when Types.equal e e' -> + Printf.sprintf + " — a %s can only be read through, and never becomes a %s that can be \ + written through. Copy the %s out with (deref p) and point at the copy; \ + where nothing writes through it, the %s can be declared %s instead" + (Types.to_string got) (Types.to_string want) (Types.to_string e) + (Types.to_string want) (Types.to_string got) | _ -> "" let expect ctx loc ~want (got : Tast.expr) = @@ -3152,7 +3190,7 @@ let expect ctx loc ~want (got : Tast.expr) = (* A writable view seen as a read-only one. The two are the same two words, so the value is only retyped; the reverse is refused below, with [const_note] naming the copy that would make it writable. *) - | Types.Slice (Types.Const, _), _ + | (Types.Slice (Types.Const, _) | Types.Ptr (Types.Const, _)), _ when Types.const_widens ~from:got.Tast.ty ~into:w -> { got with Tast.ty = w } | _ -> got @@ -3239,8 +3277,8 @@ let invented_ctx env ret = (* The address of field [i] of the struct the pointer in slot [p] points at. *) let field_addr_of loc sty fty p i = - let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr sty) (Tast.Local p))) in - mk loc (Types.Ptr fty) (Tast.Addr (Tast.Pfield (target, i))) + let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr (Types.Mut, sty)) (Tast.Local p))) in + mk loc (Types.Ptr (Types.Mut, fty)) (Tast.Addr (Tast.Pfield (target, i))) (* The pointer form is what a Map_Info holds; the direct form is what an emitted hasher calls. See flan_rt.c on why they are two symbols. *) @@ -3337,8 +3375,8 @@ and struct_key_pair env loc n = fail loc "%s has no fields, so it is not a map key — every value of it would \ be the same key" n; - let hparams = [ Types.Ptr sty; hash_ty; Types.Int Types.I64 ] in - let eparams = [ Types.Ptr sty; Types.Ptr sty; Types.Int Types.I64 ] in + let hparams = [ Types.Ptr (Types.Mut, sty); hash_ty; Types.Int Types.I64 ] in + let eparams = [ Types.Ptr (Types.Mut, sty); Types.Ptr (Types.Mut, sty); Types.Int Types.I64 ] in (* Registered before the fields are walked, so a struct reached twice through two different fields emits one pair and not two. A struct cannot contain itself by value, so there is no cycle to break — only sharing. @@ -3358,7 +3396,7 @@ and struct_key_pair env loc n = hashes its bytes and a nested struct hashes field by field. Padding is never reached, because nothing here addresses anything but a field. *) let hctx = invented_ctx env hash_ty in - let kp = fresh_slot ~name:"key" hctx (Types.Ptr sty) in + let kp = fresh_slot ~name:"key" hctx (Types.Ptr (Types.Mut, sty)) in let seed = fresh_slot ~name:"seed" hctx hash_ty in ignore (fresh_slot ~name:"size" hctx (Types.Int Types.I64)); let acc = fresh_slot ~name:"h" hctx hash_ty in @@ -3395,8 +3433,8 @@ and struct_key_pair env loc n = field that differs, which for a struct with a string field is the difference between one memcmp and two. *) let ectx = invented_ctx env (Types.Int Types.I8) in - let ap = fresh_slot ~name:"a" ectx (Types.Ptr sty) in - let bp = fresh_slot ~name:"b" ectx (Types.Ptr sty) in + let ap = fresh_slot ~name:"a" ectx (Types.Ptr (Types.Mut, sty)) in + let bp = fresh_slot ~name:"b" ectx (Types.Ptr (Types.Mut, sty)) in ignore (fresh_slot ~name:"size" ectx (Types.Int Types.I64)); let i8 v = mk loc (Types.Int Types.I8) (Tast.Int (v, Types.I8)) in let checks = @@ -3648,7 +3686,7 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) = List.filter_map (fun i -> match List.nth_opt args i with - | Some ({ Tast.ty = Types.Ptr t; _ } as p) when res_pure p -> + | Some ({ Tast.ty = Types.Ptr (_, t); _ } as p) when res_pure p -> Some (mk loc t (Tast.Deref p), t) | _ -> None) tr.Shim.rekey @@ -4600,7 +4638,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body = pointer is a hidden parameter and the name is a slot loaded from it — a handler that passed [c] to something expecting the struct would otherwise be handed an address. *) - let pslot = fresh_slot hctx (Types.Ptr ty) in + let pslot = fresh_slot hctx (Types.Ptr (Types.Mut, ty)) in let cslot = bind hctx c.Ast.hname ty ~assignable:false in let hbody = map_lr (fun e -> check hctx e) c.Ast.hbody in let hbody = @@ -4609,7 +4647,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body = ([ (cslot, mk c.Ast.hloc ty (Tast.Deref - (mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ], + (mk c.Ast.hloc (Types.Ptr (Types.Mut, ty)) (Tast.Local pslot)))) ], hbody)) ] in (* Named after the function it came out of, and numbered within it: @@ -4642,7 +4680,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body = clause matched, and it cannot know which of them captured. *) let fenv = declare_env hctx fenv in ctx.env.lifted <- - { Tast.name = fname; params = [ Types.Ptr ty ]; + { Tast.name = fname; params = [ Types.Ptr (Types.Mut, ty) ]; slots = Array.of_list (List.rev hctx.slot_tys); snames = Array.of_list (List.rev hctx.slot_names); ret = Types.Unit; body = prefix hbody; fdefers = []; @@ -6362,7 +6400,7 @@ and unknown_name : 'a. ?setting:bool -> ctx -> Loc.t -> string -> 'a = let sname = match ty with | Some (Types.Named n) when fields_named ctx.env n <> None -> Some n - | Some (Types.Ptr (Types.Named n)) when fields_named ctx.env n <> None -> Some n + | Some (Types.Ptr (_, (Types.Named n))) when fields_named ctx.env n <> None -> Some n | _ -> None in match sname, ty with @@ -6455,13 +6493,13 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string = let has n = fields_named ctx.env n <> None in match t.Tast.ty with | Types.Named n when has n -> t, n - | Types.Ptr (Types.Named n) when has n -> + | Types.Ptr (_, (Types.Named n)) when has n -> mk t.Tast.loc (Types.Named n) (Tast.Deref t), n (* A data type's fields belong to one case, and which case it is holding is only known after the tag has been read. [.field] would have to be a read that might be reading something else, so it is not one: [match] is how a data type is opened, and it binds the fields it has proved are there. *) - | (Types.Named n | Types.Ptr (Types.Named n)) + | (Types.Named n | Types.Ptr (_, Types.Named n)) when Hashtbl.mem ctx.env.datas n -> fail target.Ast.loc "%s is a data type, and its fields belong to a case — reach them with \ @@ -6508,6 +6546,26 @@ and refuse_string_place loc (ty : Types.t) = other way across: [load-image-from-memory] over an [embed] is the case. So the address of a read-only element may be taken, and it is a store that is refused. *) +(* Whether a checked place is read-only storage: reached through a + [[const T]] or a (Ptr const T), or a byte of a string. Its address is a + (Ptr const T). *) +and place_const (p : Tast.place) = + match p with + | Tast.Plocal _ | Tast.Pglobal _ -> false + | Tast.Pfield (t, _) -> const_reached t <> None + | Tast.Pderef t -> + (match t.Tast.ty with Types.Ptr (Types.Const, _) -> true | _ -> false) + | Tast.Pindex (t, idx) -> + let rec through_string ty n = + n > 0 + && (match ty with + | Types.String -> true + | Types.Array (_, e) | Types.Slice (_, e) -> through_string e (n - 1) + | _ -> false) + in + const_steps (const_reached t) t.Tast.ty (List.length idx) <> None + || through_string t.Tast.ty (List.length idx) + and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t = match p with | Ast.Pvar name -> @@ -6577,7 +6635,9 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t = | Ast.Pderef target -> let target = check ctx target in (match target.Tast.ty with - | Types.Ptr t -> Tast.Pderef target, t + | Types.Ptr (Types.Const, _) as view when store -> + refuse_const_place loc view + | Types.Ptr (_, t) -> Tast.Pderef target, t | other -> fail loc "deref takes a (Ptr T), found %s" (Types.to_string other)) @@ -6646,7 +6706,7 @@ and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list | Types.Array (_, t) | Types.Slice (_, t) -> t (* A string indexes to its bytes, and only to read them. *) | Types.String -> - Option.iter (fun l -> refuse_string_place l ty) place; + if store then Option.iter (fun l -> refuse_string_place l ty) place; Types.Int Types.U8 | other -> fail i.Ast.loc "%s cannot be indexed" (Types.to_string other) @@ -7290,7 +7350,7 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) = match idx with | [ i ] -> let i = index_expr ctx i in - rt loc (Types.Ptr elem) "flan_vec_at" + rt loc (Types.Ptr (Types.Mut, elem)) "flan_vec_at" [ target; i; size_of loc elem; here loc ], elem | _ -> fail loc @@ -8414,9 +8474,9 @@ and named_call ?(qualified = false) ctx ~want loc name args = | [ target; cur; k; v ] -> let target = check ctx target in let kt, vt = map_kv loc "map-next" target.Tast.ty in - let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in - let k = check ctx ~want:(Types.Ptr kt) k in - let v = check ctx ~want:(Types.Ptr vt) v in + let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in + let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in + let v = check ctx ~want:(Types.Ptr (Types.Mut, vt)) v in let found = rt loc (Types.Int Types.I8) "flan_map_next" [ target; cur; k; v; size_of loc kt; size_of loc vt; here loc ] @@ -8951,7 +9011,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = let target = check ctx target in let elem = match target.Tast.ty with - | Types.Ptr t -> t + | Types.Ptr (_, t) -> t | other -> fail loc "slice-from-ptr takes a (Ptr T) and the number of elements behind \ @@ -8967,7 +9027,10 @@ and named_call ?(qualified = false) ctx ~want loc name args = fail n_loc "slice-from-ptr length %Ld is negative" k | _ -> ()); - prim Tast.SliceFromPtr (Types.Slice (Types.Mut, elem)) [ target; n ] + (* A read-only pointer gives a read-only slice, or [slice-from-ptr] + would undo the const [addr] put there. *) + let m = match target.Tast.ty with Types.Ptr (m, _) -> m | _ -> Types.Mut in + prim Tast.SliceFromPtr (Types.Slice (m, elem)) [ target; n ] | _ -> assert false) (* ── pointers ──────────────────────────────────────────────────── *) @@ -8981,12 +9044,13 @@ and named_call ?(qualified = false) ctx ~want loc name args = or (deref p)" | Some p -> let p, ty = check_place ~store:false ctx a.Ast.loc p in - expect ctx loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p))) + let m = if place_const p then Types.Const else Types.Mut in + expect ctx loc ~want (mk loc (Types.Ptr (m, ty)) (Tast.Addr p))) | "deref" -> arity ctx loc name 1 args; let a = check ctx (List.hd args) in (match a.Tast.ty with - | Types.Ptr t -> expect ctx loc ~want (mk loc t (Tast.Deref a)) + | Types.Ptr (_, t) -> expect ctx loc ~want (mk loc t (Tast.Deref a)) | other -> fail loc "deref takes a (Ptr T), found %s" (Types.to_string other)) @@ -9857,7 +9921,7 @@ and generic_call ctx ~want loc name vars pats pret args = let rec mentions v (t : Types.t) = match t with | Types.Var u -> String.equal u v - | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e + | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e | Types.Option e -> mentions v e | Types.Map (k, w) -> mentions v k || mentions v w | Types.Fn (ps, r) | Types.CFn (ps, r) -> @@ -12197,7 +12261,7 @@ let rec dyn_reach ~through p seen (t : Types.t) = | Types.Dyn -> true | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e | Types.Map (k, v) -> go k || go v - | Types.Ptr e | Types.Slice (_, e) -> through && go e + | Types.Ptr (_, e) | Types.Slice (_, e) -> through && go e | Types.Fn _ -> false | Types.Named n when not (List.mem n seen) -> let seen = n :: seen in @@ -12252,7 +12316,7 @@ let rec dyn_behind_pointer p seen (t : Types.t) = It still terminates. This walk's own [seen] guards its own [Named] recursion, and each crossing starts a separate finite walk of its own. *) - | Types.Ptr e | Types.Slice (_, e) -> dyn_through p [] e + | Types.Ptr (_, e) | Types.Slice (_, e) -> dyn_through p [] e | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e | Types.Map (k, v) -> go k || go v | Types.Dyn | Types.Fn _ -> false @@ -12327,7 +12391,7 @@ let rec hidden_dyn p seen (t : Types.t) : Types.t option = if dyn_anywhere p seen k || dyn_anywhere p seen v then Some t else None (* A pointer and a slice are views of storage something else roots; see the note above. What they point at is checked where it is declared. *) - | Types.Ptr e | Types.Slice (_, e) -> hidden_dyn p seen e + | Types.Ptr (_, e) | Types.Slice (_, e) -> hidden_dyn p seen e | Types.Fn _ -> None | Types.Named n when not (List.mem n seen) -> let seen = n :: seen in @@ -12476,7 +12540,7 @@ let dyn_descriptors (p : Tast.program) = foreign parameter of pointer or slice type receives is the address of a place. Below it the question is [dyn_behind_pointer]'s again. *) let below (t : Types.t) = - match t with Types.Ptr e | Types.Slice (_, e) -> e | t -> t + match t with Types.Ptr (_, e) | Types.Slice (_, e) -> e | t -> t in List.iteri (fun i t -> diff --git a/lib/cimport.ml b/lib/cimport.ml index d72a954b..6d5d067c 100644 --- a/lib/cimport.ml +++ b/lib/cimport.ml @@ -556,6 +556,13 @@ let param_ty env (s : string) : Ast.texpr = "char * is a parameter C may write through, and a Flan string crosses \ as a NUL-terminated copy — the writes would be lost. const char * is \ a string; this one needs a declare-c saying (Ptr u8)" + (* [const T *] is the one pointer C promises not to write through, so it + takes a (Ptr const T) — and with it the address of a read-only + element, which a (Ptr T) parameter would refuse. *) + | _ when is_const -> + (match (value_ty env s).Ast.t with + | Ast.Tapp ("Ptr", [ e ]) -> ty (Ast.Tapp ("Ptr", [ tname "const"; e ])) + | _ -> value_ty env s) | _ -> value_ty env s end else value_ty env s @@ -949,33 +956,41 @@ let c_pointee (s : string) : string option = Some (String.trim (String.sub s 0 (String.length s - 1))) else None +let ptr_agrees_elem env ~inner (elem : Ast.texpr) = + (* [void *] agrees with a pointer to anything, and this is the judgement + call of the arm. C's [void *] is opaque about *what it points at* — that + is the whole of what the spelling means — so there is no element type in + the header to disagree with, and a check that reported one would be + reporting [value_ty]'s guess of [u8] back at the author as if the header + had said it. What is *not* given up is that it is a pointer at all: the + match above requires [(Ptr _)] on the Flan side, so an [i32] or a + [string] declared against a [void *] is still a finding. That + asymmetry is the point — raylib spells thirty-odd parameters [void *] + and none of them is a scalar. *) + let b = bare inner in + if String.equal b "void" then true + else ( + match (try Some (value_ty env inner) with Refused _ -> None) with + | None -> + (* A pointee this cannot render says nothing, exactly as an + unrenderable field type says nothing in [check_structs]. *) + false + | Some want -> + let a = ty_source want and b = ty_source elem in + (* [agrees] and not [String.equal], so a [(Ptr Key)] against the + header's [(Ptr int)] lands on the enum arm. The four bytes are the + same four bytes through a pointer as they are beside one. *) + agrees env want elem || (byte a && byte b)) + let ptr_agrees env ~(c : string) (t : Ast.texpr) = match (c_pointee c, t.Ast.t) with - | Some inner, Ast.Tapp ("Ptr", [ elem ]) -> - (* [void *] agrees with a pointer to anything, and this is the judgement - call of the arm. C's [void *] is opaque about *what it points at* — that - is the whole of what the spelling means — so there is no element type in - the header to disagree with, and a check that reported one would be - reporting [value_ty]'s guess of [u8] back at the author as if the header - had said it. What is *not* given up is that it is a pointer at all: the - match above requires [(Ptr _)] on the Flan side, so an [i32] or a - [string] declared against a [void *] is still a finding. That - asymmetry is the point — raylib spells thirty-odd parameters [void *] - and none of them is a scalar. *) - let b = bare inner in - if String.equal b "void" then true - else ( - match (try Some (value_ty env inner) with Refused _ -> None) with - | None -> - (* A pointee this cannot render says nothing, exactly as an - unrenderable field type says nothing in [check_structs]. *) - false - | Some want -> - let a = ty_source want and b = ty_source elem in - (* [agrees] and not [String.equal], so a [(Ptr Key)] against the - header's [(Ptr int)] lands on the enum arm. The four bytes are the - same four bytes through a pointer as they are beside one. *) - agrees env want elem || (byte a && byte b)) + (* A (Ptr const T) promises C will not write, so the header has to promise + it too: over a [T *] without const, C may write through storage Flan + holds read-only. *) + | Some inner, Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; elem ]) -> + strip_prefix "const " inner <> None + && ptr_agrees_elem env ~inner elem + | Some inner, Ast.Tapp ("Ptr", [ elem ]) -> ptr_agrees_elem env ~inner elem | _ -> false (* The two together, for the one caller that still has the C spelling. A diff --git a/lib/dev.ml b/lib/dev.ml index dfe19dda..7170de14 100644 --- a/lib/dev.ml +++ b/lib/dev.ml @@ -2726,7 +2726,7 @@ let type_of_spelling t spelling : (Types.t, string) result = let addr_extern : Tast.extern = { Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr"; eparams = [ Types.Int Types.I64 ]; - eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown } + eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown } (* Renders the value [(Ptr ty)] holding [addr], in the program. @@ -2761,7 +2761,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t) extra := ty :: !extra; i) } in - let pty = Types.Ptr ty in + let pty = Types.Ptr (Types.Mut, ty) in let root = { Tast.e = Tast.Prim @@ -2771,7 +2771,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t) ("flan/dev-addr", [ { Tast.e = Tast.Int (Int64.of_int addr, Types.I64); ty = Types.Int Types.I64; loc } ]); - ty = Types.Ptr (Types.Int Types.U8); loc } ]); + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } ]); ty = pty; loc } in match Render.render c 0 root with @@ -2935,7 +2935,7 @@ let inspect_addr t ~addr ~want_type = | Ok v -> ok ([ Printf.sprintf ":addr %d" addr; - ":type " ^ Wire.quote (Types.to_string (Types.Ptr ty)); + ":type " ^ Wire.quote (Types.to_string (Types.Ptr (Types.Mut, ty))); ":value " ^ Wire.quote v; ":live " ^ live ] @ told @ where)))))) diff --git a/lib/emit.ml b/lib/emit.ml index a8ccfff7..3e229510 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -791,7 +791,7 @@ let rec dty m d (t : Types.t) : int = | Types.Bool -> basic "bool" 8 "DW_ATE_boolean" | Types.Enum e -> basic e 32 "DW_ATE_signed" | Types.Unit | Types.Never -> composite (Types.to_string t) [] - | Types.Ptr e -> + | Types.Ptr (_, e) -> let id = dalloc d in Hashtbl.replace d.dtys key id; (* [(Ptr Unit)] and [(Ptr Never)] are the opaque pointer, and a DWARF @@ -817,10 +817,10 @@ let rec dty m d (t : Types.t) : int = capacity, so two members are the whole truth about a slice. *) | Types.String -> composite "string" - [ ("ptr", Types.Ptr (Types.Int Types.U8)); ("len", Types.Int Types.I64) ] + [ ("ptr", Types.Ptr (Types.Mut, (Types.Int Types.U8))); ("len", Types.Int Types.I64) ] | Types.Slice (_, e) -> composite (Types.to_string t) - [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64) ] + [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64) ] | Types.Option e -> composite (Types.to_string t) [ ("tag", Types.Int Types.U8); ("value", e) ] @@ -888,7 +888,7 @@ let rec dty m d (t : Types.t) : int = would put the reader's offsets out by one. *) | Types.Vec e -> composite (Types.to_string t) - [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64); + [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64); ("cap", Types.Int Types.I64); ("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ] (* Five fields again, and shown as five for the same reason: a debugger @@ -898,7 +898,7 @@ let rec dty m d (t : Types.t) : int = describing a field that is not there. *) | Types.Map (k, v) -> composite (Types.to_string t) - [ ("data", Types.Ptr (Types.Int Types.U8)); + [ ("data", Types.Ptr (Types.Mut, (Types.Int Types.U8))); ("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64); ("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ] |> fun n -> ignore k; ignore v; n @@ -913,7 +913,7 @@ let rec dty m d (t : Types.t) : int = locals, where they are under the names the source gave them. *) | Types.Fn _ -> composite (Types.to_string t) - [ ("code", Types.Ptr Types.Unit); ("env", Types.Ptr Types.Unit) ] + [ ("code", Types.Ptr (Types.Mut, Types.Unit)); ("env", Types.Ptr (Types.Mut, Types.Unit)) ] (* And the bare one is what it always was: a pointer to code, and lldb is told exactly that and no more. DWARF has DW_TAG_subroutine_type for the signature behind it, and spelling one out would buy a reader @@ -2568,7 +2568,7 @@ and place f (p : Tast.place) : string * Types.t = | Tast.Pindex (target, idx) -> element_addr f target idx | Tast.Pderef target -> let t = match target.Tast.ty with - | Types.Ptr t -> t | t -> internal "deref of %s" (Types.to_string t) + | Types.Ptr (_, t) -> t | t -> internal "deref of %s" (Types.to_string t) in value f target, t diff --git a/lib/render.ml b/lib/render.ml index d45251b6..c5cf9f6d 100644 --- a/lib/render.ml +++ b/lib/render.ml @@ -193,7 +193,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis An address the registry never saw is neither: it prints []. That is a stack local, a global, or a pointer from C, and the shadow stack and the static type table already answer for the first two by name. *) - | Types.Ptr t -> + | Types.Ptr (_, t) -> (match c.ptrs with | None -> [ lit "" ] | Some pt -> diff --git a/lib/session.ml b/lib/session.ml index b86df0e4..2aba91a8 100644 --- a/lib/session.ml +++ b/lib/session.ml @@ -1202,12 +1202,12 @@ let externs : Tast.extern list = is. See [render_locals]. *) { Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot"; eparams = [ Types.Int Types.I64; Types.Int Types.I64 ]; - eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown }; + eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown }; (* The condition the stopped program is holding, same contract: the agent resolves it against the snapshot on top when the thunk runs, and NULL when there is none. See [render_condition]. *) { Tast.ename = "flan/dev-cond"; esym = "flan_agent_condition"; - eparams = []; eret = Types.Ptr (Types.Int Types.U8); + eparams = []; eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown }; (* The character beside a rendered byte. See [Render.pointers]. *) { Tast.ename = "flan/dev-emit-u8-char"; esym = "flan_dev_emit_u8_char"; @@ -1232,10 +1232,10 @@ let externs : Tast.extern list = written" is already the right rendering for an address the registry never saw. *) { Tast.ename = "flan/reg-live"; esym = "flan_dev_reg_live"; - eparams = [ Types.Ptr (Types.Int Types.U8) ]; + eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ]; eret = Types.Int Types.I32; eloc = Loc.unknown }; { Tast.ename = "flan/reg-emit"; esym = "flan_dev_reg_emit"; - eparams = [ Types.Ptr (Types.Int Types.U8) ]; + eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ]; eret = Types.Int Types.I32; eloc = Loc.unknown } ] (* The REPL's emitter. Each piece is one extern call: the dev runtime already @@ -1264,8 +1264,8 @@ let dev_pointers : Render.pointers = let ask name (p : Tast.expr) : Tast.expr = let loc = p.Tast.loc in let byte = - { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Int Types.U8)), [ p ]); - ty = Types.Ptr (Types.Int Types.U8); loc } + { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, (Types.Int Types.U8))), [ p ]); + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } in { Tast.e = Tast.Call (name, [ byte ]); ty = i32; loc } in @@ -1405,11 +1405,11 @@ let render_locals ?(origin = "") t ~frame ~(fn : Tast.fn) ~bound in let address = { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx i ]); - ty = Types.Ptr (Types.Int Types.U8); loc } + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } in let typed = - { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]); - ty = Types.Ptr ty; loc } + { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]); + ty = Types.Ptr (Types.Mut, ty); loc } in let v = { Tast.e = Tast.Deref typed; ty; loc } in match Render.render c 0 v with @@ -1513,11 +1513,11 @@ let render_condition t ~(st : Tast.structure) : change * (string * string) list let cty = Types.Named st.Tast.sname in let address = { Tast.e = Tast.Call ("flan/dev-cond", []); - ty = Types.Ptr (Types.Int Types.U8); loc } + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } in let typed = - { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr cty), [ address ]); - ty = Types.Ptr cty; loc } + { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, cty)), [ address ]); + ty = Types.Ptr (Types.Mut, cty); loc } in let root = { Tast.e = Tast.Deref typed; ty = cty; loc } in let one i (f : Tast.field) = @@ -1770,11 +1770,11 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path let ty = fn.Tast.slots.(slot) in let address = { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]); - ty = Types.Ptr (Types.Int Types.U8); loc } + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } in let typed = - { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]); - ty = Types.Ptr ty; loc } + { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]); + ty = Types.Ptr (Types.Mut, ty); loc } in let root = { Tast.e = Tast.Deref typed; ty; loc } in let rec walk v = function @@ -1805,7 +1805,7 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path Tast.Prim (Tast.Cast (Types.Int Types.I64), [ { Tast.e = Tast.Prim (Tast.AddrOf, [ v ]); - ty = Types.Ptr v.Tast.ty; loc } ]); + ty = Types.Ptr (Types.Mut, v.Tast.ty); loc } ]); ty = Types.Int Types.I64; loc } in let newline = @@ -1985,11 +1985,11 @@ let write_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path let ty = fn.Tast.slots.(slot) in let address = { Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]); - ty = Types.Ptr (Types.Int Types.U8); loc } + ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } in let typed = - { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]); - ty = Types.Ptr ty; loc } + { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]); + ty = Types.Ptr (Types.Mut, ty); loc } in let root = { Tast.e = Tast.Deref typed; ty; loc } in let rec walk v = function diff --git a/lib/shim.ml b/lib/shim.ml index 2c590440..e185d325 100644 --- a/lib/shim.ml +++ b/lib/shim.ml @@ -221,6 +221,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string = else fail loc "%s is %s, which is not a type this shim generator knows" what n) | Ast.Tapp ("Ptr", [ e ]) -> cty env ~needed ~loc ~what e ^ " *" + | Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; e ]) -> + "const " ^ cty env ~needed ~loc ~what e ^ " *" | Ast.Tapp ("Option", _) -> fail loc "%s is an Option, which C has no shape for — declare what C returns and \ diff --git a/lib/types.ml b/lib/types.ml index 7ef1cd4d..bccd930a 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -43,7 +43,7 @@ type t = | Slice of access * t (* [T] [const T] ptr+len, non-owning *) | Array of int64 * t (* [n T] inline, a value, copies *) | Map of t * t (* (Map K V) *) - | Ptr of t (* (Ptr T) *) + | Ptr of access * t (* (Ptr T) (Ptr const T) *) (* [Allocator]: a builtin opaque type, the way [string] is a builtin ptr+len. It is a [Types.t] case with no user-writable constructor, which is what lets spec-memory.md's "procedure plus an opaque data pointer" be @@ -193,7 +193,7 @@ let rec equal a b = | Slice (a, x), Slice (b, y) -> a = b && equal x y | Array (n, x), Array (m, y) -> Int64.equal n m && equal x y | Map (k, v), Map (k', v') -> equal k k' && equal v v' - | Ptr x, Ptr y -> equal x y + | Ptr (a, x), Ptr (b, y) -> a = b && equal x y | Alloc, Alloc -> true | Vec x, Vec y -> equal x y | Option x, Option y -> equal x y @@ -219,7 +219,8 @@ let rec to_string = function | Slice (Const, t) -> "[const " ^ to_string t ^ "]" | Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t) | Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v) - | Ptr t -> "(Ptr " ^ to_string t ^ ")" + | Ptr (Mut, t) -> "(Ptr " ^ to_string t ^ ")" + | Ptr (Const, t) -> "(Ptr const " ^ to_string t ^ ")" | Alloc -> "Allocator" | Vec t -> "(Vec " ^ to_string t ^ ")" | Option t -> "(Option " ^ to_string t ^ ")" @@ -344,7 +345,8 @@ let join a b = same at run time. *) let rec const_widens ~(from : t) ~(into : t) = match from, into with - | Slice (_, a), Slice (Const, b) -> equal a b || const_widens ~from:a ~into:b + | Slice (_, a), Slice (Const, b) | Ptr (_, a), Ptr (Const, b) -> + equal a b || const_widens ~from:a ~into:b | _ -> false (* A function of one signature standing where another is wanted, when the diff --git a/lib/x86.ml b/lib/x86.ml index 7b1f5521..fd80d5f8 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -1554,7 +1554,7 @@ type arg = move-only container by address. *) let classify_c (l : loc) (t : Types.t) = match t with - | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ] + | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr (Types.Mut, Types.Unit)); Alen l ] | Types.Unit | Types.Never -> [] | Types.Vec _ | Types.Map _ -> [ Aptr l ] (* A fixed array crossing into a dyn view (M2 item 3) needs its address for @@ -1816,7 +1816,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit = store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8; (match env with | None -> xor_rr f.b ~dst:rax ~src:rax - | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr Types.Unit)); + | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit))); store_int f.b ~src:rax ~mm:(lmem f (shift dst 8) ~scratch:r11) ~size:8 | Tast.FnAddr r -> fnaddr_at f ~loc:e.Tast.loc ~reg:rax r; @@ -1844,7 +1844,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit = let c = eval f callee in let env = match callee.Tast.ty with - | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr Types.Unit)) + | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr (Types.Mut, Types.Unit))) | _ -> None in call_flan f ?env ~target:(`Loc c) ~args ~rty:t dst @@ -2059,7 +2059,7 @@ and emit_handled f frames body dst t = (match h.Tast.henv with | Some ev -> let l = scoped f (fun () -> eval f ev) in - load_loc f ~reg:rax l (Types.Ptr Types.Unit) + load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit)) | None -> xor_rr f.b ~dst:rax ~src:rax); store_int f.b ~src:rax ~mm:(Frame (slot + h_env)) ~size:8; lea f.b ~dst:rdi ~mm:(Frame slot); @@ -2573,7 +2573,7 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t = and field_loc f (base : loc) (ty : Types.t) i = match ty with | Types.Named sn -> shift base (List.nth (field_offsets f sn) i) - | Types.Ptr (Types.Named sn) -> + | Types.Ptr (_, (Types.Named sn)) -> shift (Lp (off_of base, 0)) (List.nth (field_offsets f sn) i) | Types.String | Types.Slice _ -> shift base (if i = 0 then 0 else 8) | Types.Option el -> let ot, ov = option_lay f el in @@ -2606,7 +2606,7 @@ and elements f (base : loc) (ty : Types.t) (is : Tast.expr list) : loc = | i :: rest -> let elem = match ty with - | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el + | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el | Types.String -> Types.Int Types.U8 | t -> unsupported "index into %s" (Types.to_string t) in @@ -2904,7 +2904,7 @@ and check_cast f (loc : Loc.t) (src : Types.fkind) (k : Types.ikind) = and element f (base : loc) (ty : Types.t) (i : Tast.expr) : loc = let elem = match ty with - | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el + | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el | Types.String -> Types.Int Types.U8 | t -> unsupported "index into %s" (Types.to_string t) in @@ -2966,7 +2966,7 @@ and call_flan f ?env ~target ~args ~rty dst = in (* The channel is this frame's own: a callee that transfers writes through the pointer we were handed, so one cell serves the whole chain. *) - let chan = [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] in + let chan = [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] in (* And the environment last of all, on exactly one kind of call: one through a [(Fn ...)] value, which cannot know whether the body it reaches declared one. Every other call passes what it always passed — this is @@ -3074,7 +3074,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst = args in let flat = List.concat_map (fun (l, ty) -> classify_c l ty) vals in - let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] else flat in + let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] else flat in let nsse = emit_args f flat in (* [al] is how many SSE registers were used, which a variadic callee reads. Harmless on a fixed one, and a [declare] does not say which it is. *) diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c index ec4e0e3f..82c1120c 100644 --- a/runtime/flan_dev.c +++ b/runtime/flan_dev.c @@ -2325,7 +2325,7 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) { } { static const char why[] = - "\nflan: a write through a pointer into read-only memory, " + "\nflan: a write into read-only memory, " "a null, or a stack overflow\n"; crash_puts(why, sizeof why - 1); } diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index c6b9a598..c0c58015 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -95,10 +95,10 @@ forever="dev-loop dev-watch dev-chatty agent-auto" # sweep now and they are five of the MATCHes. # The one whose whole point is a fault, and which therefore cannot be compared -# at this sweep's optimisation level. dev-segv stores through a pointer to a -# string literal's bytes, which is a store into .rodata: LLVM at -O2 deletes it -# as undefined and exits 0, and this backend has no optimiser and exits 139. -# That is not a lowering disagreement. test_dev.ml builds it in a dev session, +# at this sweep's optimisation level. dev-segv stores through a null pointer, +# which is undefined: what LLVM at -O2 does with it is its own business, and +# this backend has no optimiser and exits 139. That is not a lowering +# disagreement. test_dev.ml builds it in a dev session, # where the fault is the thing asserted. It also calls agent/start, so it # leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks # in the break loop instead of dying. diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan index 6ab1db0f..3c64505f 100644 --- a/test/programs/const-slice.flan +++ b/test/programs/const-slice.flan @@ -18,6 +18,9 @@ (set n (+ n (length (at parts i))))) n)) +;; A (Ptr const T) is what the address of read-only storage is. +(defn peek [p (Ptr const u8)] u8 (deref p)) + ;; A function that only reads stands where one that may write is wanted, and ;; one returning a writable slice where a read-only one is wanted. (defn rd [s [const u8]] i32 (length s)) @@ -54,5 +57,9 @@ (println (string (slice (join (slice f) (bytes-view "-")))))) (println (at r 0)) (println (call-rd rd) (call-bare rd) (call-mk mk)) + (let [b (bytes "q")] + (println (peek (addr (at r 1))) (peek (addr (at "abc" 2))) + (peek (addr (at b 0))) + (string (slice-from-ptr (addr (at r 7)) 5)))) (free names)) 0) diff --git a/test/programs/dev-segv.flan b/test/programs/dev-segv.flan index 1ea5ca31..95ce1f54 100644 --- a/test/programs/dev-segv.flan +++ b/test/programs/dev-segv.flan @@ -1,22 +1,21 @@ -;;;; The dogfooding crash, replayed on purpose: a store through a pointer to -;;;; a string literal's bytes lands in read-only memory and takes SIGSEGV. In -;;;; a dev session that used to kill the whole process — daemon, compiler and -;;;; socket together, with no message at all. The dev build's crash handler -;;;; turns it into the same park the no-channel traps take: one line naming -;;;; the address and the frame, then the break loop, with the daemon alive -;;;; and answering behind it. There is no restart to list — a faulting -;;;; instruction has nowhere to resume at — which is the same empty-list -;;;; shape dev-trap-null-alloc.flan pins for free-all. +;;;; A hardware fault, taken on purpose: a store through a null pointer takes +;;;; SIGSEGV. In a dev session that used to kill the whole process — daemon, +;;;; compiler and socket together, with no message at all. The dev build's +;;;; crash handler turns it into the same park the no-channel traps take: one +;;;; line naming the address and the frame, then the break loop, with the +;;;; daemon alive and answering behind it. There is no restart to list — a +;;;; faulting instruction has nowhere to resume at — which is the same +;;;; empty-list shape dev-trap-null-alloc.flan pins for free-all. ;;;; -;;;; Through a pointer, because a store through the [const u8] itself is -;;;; refused at compile time; a (Ptr T) is the C boundary, where nothing is -;;;; checked. +;;;; The crash that first raised this was a write through a bytes-view of a +;;;; string literal, which no longer compiles; a zeroed pointer is the +;;;; surviving way to fault. (import agent "vendor:agent") +(defonce nowhere (Ptr u8)) + (defn main [] i32 (agent/start "/tmp/flan-dev-segv-fallback.sock") - (let [v (bytes-view "INSERTIONSORT") - p (addr (at v 0))] - (set (deref p) \Z) - (print (string v)) - 0)) + (set (deref nowhere) \Z) + (println "not reached") + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 4ef0165a..f06512f6 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -872,7 +872,7 @@ let () = (* [const T]: the checker's alone, so the three builds agree and every row is about which values reach which parameters. *) let const_slice_out = - "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n" + "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n101 99 113 world\n" in outputs "const slices" "programs/const-slice.flan" const_slice_out; outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan" diff --git a/test/test_dev.ml b/test/test_dev.ml index 7701bb2d..46af004a 100644 --- a/test/test_dev.ml +++ b/test/test_dev.ml @@ -1922,7 +1922,7 @@ let () = if refault then begin let faulting = "(:op \"eval-expr\" :code \ - \"(let [v (bytes-view \\\"refault\\\") p (addr (at v 0))] (set (deref p) 90) 1)\" \ + \"(do (set (deref nowhere) 90) 1)\" \ :file \"/tmp/buf.flan\")" in (match ask faulting with _ -> () | exception _ -> ()); @@ -2028,9 +2028,8 @@ let () = word. The dev build's crash handler (flan_dev_crash_enable) enters the same trap hook the six no-channel refusals use, so everything trap_park asserts for them holds here too: stopped and describable, an eval still - answered, a resume refused. The program writes through a pointer to - a literal's bytes, which is the surviving spelling of that crash: a - store through the bytes-view itself no longer compiles. *) + answered, a resume refused. The program stores through a null + pointer: the bytes-view write that first crashed no longer compiles. *) trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" []; (* ── The locals of a stopped frame ─────────────────────────────── *) diff --git a/test/test_flan.ml b/test/test_flan.ml index 77abd557..adc0a418 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2238,12 +2238,10 @@ let () = rejects_check "set through a string's slice" "(defn f [s string] () (set (at (slice s 1) 0) 65))" ~needle:"not a place"; - (* The address of one is the same question and gets the same answer, so - the message has to fit a reader who asked for a pointer and not a - store. *) - rejects_check "the address of a string's byte" + (* The address of one is a (Ptr const u8), so it is not a (Ptr u8). *) + rejects_check "the address of a string's byte is read-only" "(defn f [s string] (Ptr u8) (addr (at s 0)))" - ~needle:"(at s i) is a value and not a place"; + ~needle:"expected (Ptr u8), found (Ptr const u8)"; (* And a string is still not a [u8]: slicing one does not smuggle a byte slice out of it. *) rejects_check "a string slice is not a byte slice" @@ -2322,6 +2320,47 @@ let () = "(defn mk [] [const u8] (bytes-view \"a\")) \ (defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))" ~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])"; + (* (Ptr const T): the pointer beside [const T]. *) + infers "the address of a const element" "(addr (at (bytes-view \"hi\") 0))" + "(Ptr const u8)"; + infers "the address of a string's byte" "(addr (at \"hi\" 0))" + "(Ptr const u8)"; + infers "a const pointer slices to a const slice" + "(slice-from-ptr (addr (at (bytes-view \"hi\") 0)) 2)" "[const u8]"; + rejects_check "a store through a const pointer" + "(defn f [p (Ptr const i32)] () (set (deref p) 1))" + ~needle:"this writes through a (Ptr const i32)"; + rejects_check "a store through the address of a const element" + "(defn f [v [const u8]] () (set (deref (addr (at v 0))) 1))" + ~needle:"this writes through a (Ptr const u8)"; + rejects_check "a store through the address of a string's byte" + "(defn f [s string] () (set (deref (addr (at s 0))) 1))" + ~needle:"this writes through a (Ptr const u8)"; + rejects_check "a field store through a const pointer" + "(defstruct P [x i32]) (defn f [p (Ptr const P)] () (set (.x p) 1))" + ~needle:"this writes through a (Ptr const P)"; + rejects_check "a push through a const pointer" + "(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))" + ~needle:"behind a (Ptr const (Vec i32))"; + rejects_check "a const pointer is not a writable one" + "(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))" + ~needle:"expected (Ptr u8), found (Ptr const u8)"; + rejects_check "slice-from-ptr keeps the const" + "(defn f [v [const u8]] [u8] (slice-from-ptr (addr (at v 0)) 1))" + ~needle:"expected [u8], found [const u8]"; + rejects_check "const alone is not a type" "(defn f [p (Ptr const)] i32 0)" + ~needle:"const is not a type on its own"; + rejects_check "no conversion under a writable pointer" + "(defn f [p (Ptr (Ptr i32))] (Ptr (Ptr const i32)) p)" + ~needle:"expected (Ptr (Ptr const i32)), found (Ptr (Ptr i32))"; + accepts "a writable pointer is a const one" + "(defn f [p (Ptr i32)] (Ptr const i32) p)"; + accepts "and under a const pointer, one level down" + "(defn f [p (Ptr (Ptr i32))] (Ptr const (Ptr const i32)) p)"; + accepts "a generic const pointer binds from a writable one" + "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))"; + accepts "vec-new reads (Ptr const u8) as a type" + "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))"; rejects_check "const is not a name a constant can have" "(defconst const 4)" ~needle:"const cannot be declared"; (* The const is shallow: an element of a [const [u8]] is a writable [u8]. *) @@ -2334,7 +2373,7 @@ let () = accepts "under a const slice the element converts too" "(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))"; accepts "the address of a const element, for C" - "(defn f [s [const u8]] (Ptr u8) (addr (at s 0)))"; + "(defn f [s [const u8]] (Ptr const u8) (addr (at s 0)))"; accepts "a generic reader takes both" "(defn f [a [const i32] b [i32]] i64 (+ (sum-i32 a) (sum-i32 b)))"; @@ -4503,8 +4542,9 @@ let () = something different in a parameter than it does anywhere else. *) emits "const char * as a string parameter" "(declare-c name-length [text string] i32 \"name_length\")"; - emits "a pointer parameter" - "(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")"; + (* const int * is a pointer C promises not to write through. *) + emits "a const pointer parameter" + "(declare-c count-at [values (Ptr const i32) n i32] i32 \"count_at\")"; (* struct Pair is both Pair and Point in the header and the package describes it once, so both names have to land on the one defstruct — raylib does exactly this with Texture2D and TextureCubemap. *) @@ -5140,6 +5180,10 @@ let () = "(declare-c name-length [text string] i32 \"name_length\")"; agreed "a pointer that matches the header exactly" "(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")"; + agreed "a const pointer that matches the header exactly" + "(declare-c count-at [values (Ptr const i32) n i32] i32 \"count_at\")"; + agreed "a const pointer where the header says const void *" + "(declare-c blit [dst (Ptr Pair) src (Ptr const Shade) n i32] \"blit\")"; (* void * is opaque about what it points at, so there is no element type in the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *) agreed "any pointer where the header says void *" @@ -5155,12 +5199,17 @@ let () = name the disagreement. *) differs "a pointer to the wrong named type" "(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")" - "parameter p is (Ptr Shade) and the header says (Ptr Pair)"; + "parameter p is (Ptr Shade) and the header says (Ptr const Pair)"; differs "a pointer to the wrong width" "(declare-c count-at [values (Ptr f64) n i32] i32 \"count_at\")" "parameter values is (Ptr f64)"; (* void * gives up the element type and nothing else. It is still a pointer, and a scalar declared against one is still a finding. *) + (* A (Ptr const T) promises C will not write, and the header has to say so + too. *) + differs "a const pointer where the header may write" + "(declare-c blit [dst (Ptr const u8) src (Ptr u8) n i32] \"blit\")" + "parameter dst is (Ptr const u8)"; differs "a scalar where the header says void *" "(declare-c blit [dst i64 src (Ptr u8) n i32] \"blit\")" "parameter dst is i64"; diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index b381a2fe..fad8cea3 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -441,9 +441,8 @@ let dev_sweep () = sanitized run must produce ASan's report and must NOT produce the handler's line, and that is the assertion. - And it has to be built at -O0. At the sweep's -O2 the write through a - pointer to a string literal's bytes does not fault at all — measured, both - builds print the unmodified string — so a case that is about what happens + And it has to be built at -O0. At the sweep's -O2 a store through a null + pointer is undefined and need not fault — so a case that is about what happens on a fault has to be compiled where the fault happens. Same family as the -O0/-O2 split [unchecked_controls] records for bounds.flan. diff --git a/vendor/raylib/generated.flan b/vendor/raylib/generated.flan index 7ff58dbd..2ce0d70f 100644 --- a/vendor/raylib/generated.flan +++ b/vendor/raylib/generated.flan @@ -78,7 +78,7 @@ (declare-c load-file-data [file-name string data-size (Ptr i32)] (Ptr u8) "LoadFileData") (declare-c unload-file-data [data (Ptr u8)] "UnloadFileData") (declare-c save-file-data [file-name string data (Ptr u8) data-size i32] bool "SaveFileData") -(declare-c export-data-as-code [data (Ptr u8) data-size i32 file-name string] bool "ExportDataAsCode") +(declare-c export-data-as-code [data (Ptr const u8) data-size i32 file-name string] bool "ExportDataAsCode") (declare-c file-exists [file-name string] bool "FileExists") (declare-c directory-exists [dir-path string] bool "DirectoryExists") (declare-c file-extension? [file-name string ext string] bool "IsFileExtension") @@ -95,9 +95,9 @@ (declare-c path-file? [path string] bool "IsPathFile") (declare-c file-name-valid? [file-name string] bool "IsFileNameValid") (declare-c file-dropped? [] bool "IsFileDropped") -(declare-c compress-data [data (Ptr u8) data-size i32 comp-data-size (Ptr i32)] (Ptr u8) "CompressData") -(declare-c decompress-data [comp-data (Ptr u8) comp-data-size i32 data-size (Ptr i32)] (Ptr u8) "DecompressData") -(declare-c decode-data-base-64 [data (Ptr u8) output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64") +(declare-c compress-data [data (Ptr const u8) data-size i32 comp-data-size (Ptr i32)] (Ptr u8) "CompressData") +(declare-c decompress-data [comp-data (Ptr const u8) comp-data-size i32 data-size (Ptr i32)] (Ptr u8) "DecompressData") +(declare-c decode-data-base-64 [data (Ptr const u8) output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64") (declare-c compute-crc32 [data (Ptr u8) data-size i32] u32 "ComputeCRC32") (declare-c compute-md5 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeMD5") (declare-c compute-sha1 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeSHA1") @@ -117,7 +117,7 @@ (declare-c set-mouse-scale [scale-x f32 scale-y f32] "SetMouseScale") (declare-c get-mouse-wheel-move-v [] Vector2 "GetMouseWheelMoveV") (declare-c update-camera-pro [camera (Ptr Camera3D) movement Vector3 rotation Vector3 zoom f32] "UpdateCameraPro") -(declare-c draw-line-strip-raw [points (Ptr Vector2) point-count i32 color Color] "DrawLineStrip") +(declare-c draw-line-strip-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawLineStrip") (declare-c draw-line-bezier [start-pos Vector2 end-pos Vector2 thick f32 color Color] "DrawLineBezier") (declare-c draw-circle-sector [center Vector2 radius f32 start-angle f32 end-angle f32 segments i32 color Color] "DrawCircleSector") (declare-c draw-circle-sector-lines [center Vector2 radius f32 start-angle f32 end-angle f32 segments i32 color Color] "DrawCircleSectorLines") @@ -126,16 +126,16 @@ (declare-c draw-rectangle-gradient-v [pos-x i32 pos-y i32 width i32 height i32 top Color bottom Color] "DrawRectangleGradientV") (declare-c draw-rectangle-gradient-h [pos-x i32 pos-y i32 width i32 height i32 left Color right Color] "DrawRectangleGradientH") (declare-c draw-rectangle-gradient-ex [rec Rectangle top-left Color bottom-left Color top-right Color bottom-right Color] "DrawRectangleGradientEx") -(declare-c draw-triangle-fan-raw [points (Ptr Vector2) point-count i32 color Color] "DrawTriangleFan") -(declare-c draw-triangle-strip-raw [points (Ptr Vector2) point-count i32 color Color] "DrawTriangleStrip") +(declare-c draw-triangle-fan-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawTriangleFan") +(declare-c draw-triangle-strip-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawTriangleStrip") (declare-c draw-poly [center Vector2 sides i32 radius f32 rotation f32 color Color] "DrawPoly") (declare-c draw-poly-lines [center Vector2 sides i32 radius f32 rotation f32 color Color] "DrawPolyLines") (declare-c draw-poly-lines-ex [center Vector2 sides i32 radius f32 rotation f32 line-thick f32 color Color] "DrawPolyLinesEx") -(declare-c draw-spline-linear-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineLinear") -(declare-c draw-spline-basis-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBasis") -(declare-c draw-spline-catmull-rom-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineCatmullRom") -(declare-c draw-spline-bezier-quadratic-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierQuadratic") -(declare-c draw-spline-bezier-cubic-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierCubic") +(declare-c draw-spline-linear-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineLinear") +(declare-c draw-spline-basis-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBasis") +(declare-c draw-spline-catmull-rom-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineCatmullRom") +(declare-c draw-spline-bezier-quadratic-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierQuadratic") +(declare-c draw-spline-bezier-cubic-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierCubic") (declare-c draw-spline-segment-linear [p-1 Vector2 p-2 Vector2 thick f32 color Color] "DrawSplineSegmentLinear") (declare-c draw-spline-segment-basis [p-1 Vector2 p-2 Vector2 p-3 Vector2 p-4 Vector2 thick f32 color Color] "DrawSplineSegmentBasis") (declare-c draw-spline-segment-catmull-rom [p-1 Vector2 p-2 Vector2 p-3 Vector2 p-4 Vector2 thick f32 color Color] "DrawSplineSegmentCatmullRom") @@ -148,7 +148,7 @@ (declare-c get-spline-point-bezier-cubic [p-1 Vector2 c-2 Vector2 c-3 Vector2 p-4 Vector2 t f32] Vector2 "GetSplinePointBezierCubic") (declare-c load-image-raw [file-name string width i32 height i32 format i32 header-size i32] Image "LoadImageRaw") (declare-c load-image-anim [file-name string frames (Ptr i32)] Image "LoadImageAnim") -(declare-c load-image-anim-from-memory [file-type string file-data (Ptr u8) data-size i32 frames (Ptr i32)] Image "LoadImageAnimFromMemory") +(declare-c load-image-anim-from-memory [file-type string file-data (Ptr const u8) data-size i32 frames (Ptr i32)] Image "LoadImageAnimFromMemory") (declare-c load-image-from-texture [texture Texture2D] Image "LoadImageFromTexture") (declare-c load-image-from-screen [] Image "LoadImageFromScreen") (declare-c export-image-to-memory [image Image file-type string file-size (Ptr i32)] (Ptr u8) "ExportImageToMemory") @@ -171,7 +171,7 @@ (declare-c image-alpha-mask [image (Ptr Image) alpha-mask Image] "ImageAlphaMask") (declare-c image-alpha-premultiply [image (Ptr Image)] "ImageAlphaPremultiply") (declare-c image-blur-gaussian [image (Ptr Image) blur-size i32] "ImageBlurGaussian") -(declare-c image-kernel-convolution [image (Ptr Image) kernel (Ptr f32) kernel-size i32] "ImageKernelConvolution") +(declare-c image-kernel-convolution [image (Ptr Image) kernel (Ptr const f32) kernel-size i32] "ImageKernelConvolution") (declare-c image-resize-canvas [image (Ptr Image) new-width i32 new-height i32 offset-x i32 offset-y i32 fill Color] "ImageResizeCanvas") (declare-c image-mipmaps [image (Ptr Image)] "ImageMipmaps") (declare-c image-dither [image (Ptr Image) r-bpp i32 g-bpp i32 b-bpp i32 a-bpp i32] "ImageDither") @@ -211,8 +211,8 @@ (declare-c image-draw-text [dst (Ptr Image) text string pos-x i32 pos-y i32 font-size i32 color Color] "ImageDrawText") (declare-c image-draw-text-ex [dst (Ptr Image) font Font text string position Vector2 font-size f32 spacing f32 tint Color] "ImageDrawTextEx") (declare-c load-texture-cubemap [image Image layout i32] Texture2D "LoadTextureCubemap") -(declare-c update-texture [texture Texture2D pixels (Ptr u8)] "UpdateTexture") -(declare-c update-texture-rec [texture Texture2D rec Rectangle pixels (Ptr u8)] "UpdateTextureRec") +(declare-c update-texture [texture Texture2D pixels (Ptr const u8)] "UpdateTexture") +(declare-c update-texture-rec [texture Texture2D rec Rectangle pixels (Ptr const u8)] "UpdateTextureRec") (declare-c gen-texture-mipmaps [texture (Ptr Texture2D)] "GenTextureMipmaps") (declare-c set-texture-wrap [texture Texture2D wrap i32] "SetTextureWrap") (declare-c color-is-equal [col-1 Color col-2 Color] bool "ColorIsEqual") @@ -229,13 +229,13 @@ (declare-c set-pixel-color [dst-ptr (Ptr u8) color Color format i32] "SetPixelColor") (declare-c get-pixel-data-size [width i32 height i32 format i32] i32 "GetPixelDataSize") (declare-c load-font-from-image [image Image key Color first-char i32] Font "LoadFontFromImage") -(declare-c load-font-from-memory [file-type string file-data (Ptr u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32] Font "LoadFontFromMemory") -(declare-c load-font-data [file-data (Ptr u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32 type i32] (Ptr GlyphInfo) "LoadFontData") -(declare-c gen-image-font-atlas [glyphs (Ptr GlyphInfo) glyph-recs (Ptr (Ptr Rectangle)) glyph-count i32 font-size i32 padding i32 pack-method i32] Image "GenImageFontAtlas") +(declare-c load-font-from-memory [file-type string file-data (Ptr const u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32] Font "LoadFontFromMemory") +(declare-c load-font-data [file-data (Ptr const u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32 type i32] (Ptr GlyphInfo) "LoadFontData") +(declare-c gen-image-font-atlas [glyphs (Ptr const GlyphInfo) glyph-recs (Ptr (Ptr Rectangle)) glyph-count i32 font-size i32 padding i32 pack-method i32] Image "GenImageFontAtlas") (declare-c unload-font-data [glyphs (Ptr GlyphInfo) glyph-count i32] "UnloadFontData") (declare-c export-font-as-code [font Font file-name string] bool "ExportFontAsCode") (declare-c draw-text-pro [font Font text string position Vector2 origin Vector2 rotation f32 font-size f32 spacing f32 tint Color] "DrawTextPro") -(declare-c draw-text-codepoints [font Font codepoints (Ptr i32) codepoint-count i32 position Vector2 font-size f32 spacing f32 tint Color] "DrawTextCodepoints") +(declare-c draw-text-codepoints [font Font codepoints (Ptr const i32) codepoint-count i32 position Vector2 font-size f32 spacing f32 tint Color] "DrawTextCodepoints") (declare-c set-text-line-spacing [spacing i32] "SetTextLineSpacing") (declare-c load-codepoints [text string count (Ptr i32)] (Ptr i32) "LoadCodepoints") (declare-c unload-codepoints [codepoints (Ptr i32)] "UnloadCodepoints") @@ -246,7 +246,7 @@ (declare-c text-is-equal [text-1 string text-2 string] bool "TextIsEqual") (declare-c text-length [text string] u32 "TextLength") (declare-c text-subtext [text string position i32 length i32] string "TextSubtext") -(declare-c text-join [text-list (Ptr (Ptr i8)) count i32 delimiter string] string "TextJoin") +(declare-c text-join [text-list (Ptr const (Ptr i8)) count i32 delimiter string] string "TextJoin") (declare-c text-split [text string delimiter i8 count (Ptr i32)] (Ptr (Ptr i8)) "TextSplit") (declare-c text-find-index [text string find string] i32 "TextFindIndex") (declare-c text-to-upper [text string] string "TextToUpper") @@ -260,7 +260,7 @@ (declare-c draw-point-3d [position Vector3 color Color] "DrawPoint3D") (declare-c draw-circle-3d [center Vector3 radius f32 rotation-axis Vector3 rotation-angle f32 color Color] "DrawCircle3D") (declare-c draw-triangle-3d [v-1 Vector3 v-2 Vector3 v-3 Vector3 color Color] "DrawTriangle3D") -(declare-c draw-triangle-strip-3d-raw [points (Ptr Vector3) point-count i32 color Color] "DrawTriangleStrip3D") +(declare-c draw-triangle-strip-3d-raw [points (Ptr const Vector3) point-count i32 color Color] "DrawTriangleStrip3D") (declare-c draw-cube-wires-v [position Vector3 size Vector3 color Color] "DrawCubeWiresV") (declare-c draw-sphere-ex [center-pos Vector3 radius f32 rings i32 slices i32 color Color] "DrawSphereEx") (declare-c draw-cylinder [position Vector3 radius-top f32 radius-bottom f32 height f32 slices i32 color Color] "DrawCylinder") @@ -286,7 +286,7 @@ (declare-c draw-billboard-rec [camera Camera3D texture Texture2D source Rectangle position Vector3 size Vector2 tint Color] "DrawBillboardRec") (declare-c draw-billboard-pro [camera Camera3D texture Texture2D source Rectangle position Vector3 up Vector3 size Vector2 origin Vector2 rotation f32 tint Color] "DrawBillboardPro") (declare-c upload-mesh [mesh (Ptr Mesh) dynamic bool] "UploadMesh") -(declare-c update-mesh-buffer [mesh Mesh index i32 data (Ptr u8) data-size i32 offset i32] "UpdateMeshBuffer") +(declare-c update-mesh-buffer [mesh Mesh index i32 data (Ptr const u8) data-size i32 offset i32] "UpdateMeshBuffer") (declare-c unload-mesh [mesh Mesh] "UnloadMesh") (declare-c get-mesh-bounding-box [mesh Mesh] BoundingBox "GetMeshBoundingBox") (declare-c gen-mesh-tangents [mesh (Ptr Mesh)] "GenMeshTangents") @@ -312,14 +312,14 @@ (declare-c get-ray-collision-mesh [ray Ray mesh Mesh transform Matrix] RayCollision "GetRayCollisionMesh") (declare-c get-ray-collision-triangle [ray Ray p-1 Vector3 p-2 Vector3 p-3 Vector3] RayCollision "GetRayCollisionTriangle") (declare-c get-ray-collision-quad [ray Ray p-1 Vector3 p-2 Vector3 p-3 Vector3 p-4 Vector3] RayCollision "GetRayCollisionQuad") -(declare-c load-wave-from-memory [file-type string file-data (Ptr u8) data-size i32] Wave "LoadWaveFromMemory") -(declare-c update-sound [sound Sound data (Ptr u8) sample-count i32] "UpdateSound") +(declare-c load-wave-from-memory [file-type string file-data (Ptr const u8) data-size i32] Wave "LoadWaveFromMemory") +(declare-c update-sound [sound Sound data (Ptr const u8) sample-count i32] "UpdateSound") (declare-c export-wave-as-code [wave Wave file-name string] bool "ExportWaveAsCode") -(declare-c load-music-stream-from-memory [file-type string data (Ptr u8) data-size i32] Music "LoadMusicStreamFromMemory") +(declare-c load-music-stream-from-memory [file-type string data (Ptr const u8) data-size i32] Music "LoadMusicStreamFromMemory") (declare-c load-audio-stream [sample-rate u32 sample-size u32 channels u32] AudioStream "LoadAudioStream") (declare-c audio-stream-valid? [stream AudioStream] bool "IsAudioStreamValid") (declare-c unload-audio-stream [stream AudioStream] "UnloadAudioStream") -(declare-c update-audio-stream [stream AudioStream data (Ptr u8) frame-count i32] "UpdateAudioStream") +(declare-c update-audio-stream [stream AudioStream data (Ptr const u8) frame-count i32] "UpdateAudioStream") (declare-c audio-stream-processed? [stream AudioStream] bool "IsAudioStreamProcessed") (declare-c play-audio-stream [stream AudioStream] "PlayAudioStream") (declare-c pause-audio-stream [stream AudioStream] "PauseAudioStream") diff --git a/vendor/raylib/raylib.flan b/vendor/raylib/raylib.flan index cba15d63..702129ba 100644 --- a/vendor/raylib/raylib.flan +++ b/vendor/raylib/raylib.flan @@ -582,10 +582,10 @@ ;; out-of-bounds read, and raylib answers false for a polygon with no points ;; anyway. (declare-c collision-point-poly?-raw - [point Vector2 points (Ptr Vector2) count i32] bool + [point Vector2 points (Ptr const Vector2) count i32] bool "CheckCollisionPointPoly") -(defn collision-point-poly? [point Vector2 points [Vector2]] bool +(defn collision-point-poly? [point Vector2 points [const Vector2]] bool (if (= (length points) 0) false (collision-point-poly?-raw point (addr (at points 0)) (length points)))) @@ -801,7 +801,7 @@ ;; which integer type a C count parameter is. The Flan wrapper below takes the ;; slice apart, which is where that idiom lives everywhere else in this file. (declare-c load-image-from-memory-raw - [file-type string file-data (Ptr u8) data-size i32] Image + [file-type string file-data (Ptr const u8) data-size i32] Image "LoadImageFromMemory") ;; Empty is answered here rather than passed on, exactly as in @@ -1015,42 +1015,42 @@ ;; Each -raw below is a generated declaration whose name moved aside; see the ;; `name` lines at the foot of `bindings`. -(defn draw-line-strip [points [Vector2] color Color] () +(defn draw-line-strip [points [const Vector2] color Color] () (when (> (length points) 0) (draw-line-strip-raw (addr (at points 0)) (length points) color))) -(defn draw-triangle-fan [points [Vector2] color Color] () +(defn draw-triangle-fan [points [const Vector2] color Color] () (when (> (length points) 0) (draw-triangle-fan-raw (addr (at points 0)) (length points) color))) -(defn draw-triangle-strip [points [Vector2] color Color] () +(defn draw-triangle-strip [points [const Vector2] color Color] () (when (> (length points) 0) (draw-triangle-strip-raw (addr (at points 0)) (length points) color))) -(defn draw-triangle-strip-3d [points [Vector3] color Color] () +(defn draw-triangle-strip-3d [points [const Vector3] color Color] () (when (> (length points) 0) (draw-triangle-strip-3d-raw (addr (at points 0)) (length points) color))) ;; The five spline drawers. raylib reads the same point array five different ;; ways; the only difference between these wrappers is which one it calls. -(defn draw-spline-linear [points [Vector2] thick f32 color Color] () +(defn draw-spline-linear [points [const Vector2] thick f32 color Color] () (when (> (length points) 0) (draw-spline-linear-raw (addr (at points 0)) (length points) thick color))) -(defn draw-spline-basis [points [Vector2] thick f32 color Color] () +(defn draw-spline-basis [points [const Vector2] thick f32 color Color] () (when (> (length points) 0) (draw-spline-basis-raw (addr (at points 0)) (length points) thick color))) -(defn draw-spline-catmull-rom [points [Vector2] thick f32 color Color] () +(defn draw-spline-catmull-rom [points [const Vector2] thick f32 color Color] () (when (> (length points) 0) (draw-spline-catmull-rom-raw (addr (at points 0)) (length points) thick color))) -(defn draw-spline-bezier-quadratic [points [Vector2] thick f32 color Color] () +(defn draw-spline-bezier-quadratic [points [const Vector2] thick f32 color Color] () (when (> (length points) 0) (draw-spline-bezier-quadratic-raw (addr (at points 0)) (length points) thick color))) -(defn draw-spline-bezier-cubic [points [Vector2] thick f32 color Color] () +(defn draw-spline-bezier-cubic [points [const Vector2] thick f32 color Color] () (when (> (length points) 0) (draw-spline-bezier-cubic-raw (addr (at points 0)) (length points) thick color))) @@ -1595,7 +1595,7 @@ ;; half no longer carries the string-faced version at all — a binding that is ;; wrong for the only direction it reads in is worse than no binding. (declare-c get-codepoint-previous-raw - [text (Ptr u8) codepoint-size (Ptr i32)] i32 + [text (Ptr const u8) codepoint-size (Ptr i32)] i32 "GetCodepointPrevious") ;; The face a caller wants: the bytes and an offset into them, rather than an