The address of read-only storage is a (Ptr const T), which nothing is written through and which a C const T * parameter takes
This commit is contained in:
parent
c0b4b22357
commit
d8945ae4ae
166
lib/check.ml
166
lib/check.ml
@ -1172,6 +1172,10 @@ let tyvar_in_scope env n =
|
|||||||
let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
||||||
let loc = t.Ast.tloc in
|
let loc = t.Ast.tloc in
|
||||||
match t.Ast.t with
|
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.Tname n -> resolve_name env ~seen loc n
|
||||||
| Ast.Tslice (c, e) ->
|
| Ast.Tslice (c, e) ->
|
||||||
Types.Slice ((if c then Types.Const else Types.Mut), resolve env ~seen 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)
|
if env' then Types.Fn (ps, r) else Types.CFn (ps, r)
|
||||||
| Ast.Tapp (name, args) ->
|
| Ast.Tapp (name, args) ->
|
||||||
(match name, args with
|
(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)
|
| "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 ] ->
|
| "Vec", [ a ] ->
|
||||||
let e = resolve env ~seen a in
|
let e = resolve env ~seen a in
|
||||||
(* A Vec of a Vec used to be refused here, and the refusal named two
|
(* 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)
|
| Types.Slice (m, p), Types.Slice (m', a)
|
||||||
when m = m' || (ro && m = Types.Const) ->
|
when m = m' || (ro && m = Types.Const) ->
|
||||||
bind_ty ~ro:(m = Types.Const) subst p a
|
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.Vec p, Types.Vec a
|
||||||
| Types.Option p, Types.Option a -> inner p 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
|
| 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.Slice (m, e) -> Types.Slice (m, subst_ty subst e)
|
||||||
| Types.Array (n, e) -> Types.Array (n, 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.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.Vec e -> Types.Vec (subst_ty subst e)
|
||||||
| Types.Option e -> Types.Option (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)
|
| 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) =
|
let rec generic_ty (t : Types.t) =
|
||||||
match t with
|
match t with
|
||||||
| Types.Var _ -> true
|
| 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.Option e -> generic_ty e
|
||||||
| Types.Map (k, v) -> generic_ty k || generic_ty v
|
| Types.Map (k, v) -> generic_ty k || generic_ty v
|
||||||
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
|
| 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) =
|
let rec reaches_dyn (t : Types.t) =
|
||||||
match t with
|
match t with
|
||||||
| Types.Dyn -> true
|
| 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.Option e -> reaches_dyn e
|
||||||
| Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
|
| Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
|
||||||
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
|
| 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.Slice (Types.Const, e) -> "cslice-" ^ mangle_ty e
|
||||||
| Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (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.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.Vec e -> "vec-" ^ mangle_ty e
|
||||||
| Types.Option e -> "opt-" ^ mangle_ty e
|
| Types.Option e -> "opt-" ^ mangle_ty e
|
||||||
| Types.Fn (ps, r) ->
|
| Types.Fn (ps, r) ->
|
||||||
@ -2023,7 +2037,7 @@ let rec occurs_in ~needle (t : Types.t) =
|
|||||||
Types.equal needle t
|
Types.equal needle t
|
||||||
||
|
||
|
||||||
match t with
|
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.Option e -> occurs_in ~needle e
|
||||||
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
|
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
|
||||||
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
|
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
|
||||||
@ -2164,11 +2178,11 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
|
|||||||
in
|
in
|
||||||
Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields };
|
Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields };
|
||||||
let ety = Types.Named ename in
|
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 =
|
let binds =
|
||||||
List.mapi
|
List.mapi
|
||||||
(fun i (_, ((b : binding), slot)) ->
|
(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))))
|
(slot, mk loc b.bty (Tast.Field (mk loc ety (Tast.Deref p), i))))
|
||||||
caught
|
caught
|
||||||
in
|
in
|
||||||
@ -2183,7 +2197,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
|
|||||||
caught))
|
caught))
|
||||||
in
|
in
|
||||||
prefix, Some eslot, Some (mslot, make),
|
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
|
(* 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],
|
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) ->
|
| Tast.Prim (Tast.At, target :: idx) ->
|
||||||
const_steps (const_reached target) target.Tast.ty (List.length idx)
|
const_steps (const_reached target) target.Tast.ty (List.length idx)
|
||||||
| Tast.Field (target, _) -> const_reached target
|
| Tast.Field (target, _) -> const_reached target
|
||||||
|
| Tast.Deref p ->
|
||||||
|
(match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
|
||||||
| _ -> None
|
| _ -> None
|
||||||
|
|
||||||
(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
|
(* [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)
|
| Types.Array (_, t) -> const_steps ro t (n - 1)
|
||||||
| _ -> ro
|
| _ -> 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 refuse_const_place loc (view : Types.t) =
|
||||||
let elem = match view with Types.Slice (_, t) -> t | t -> t in
|
match view with
|
||||||
Loc.failk "check/store-through-const" loc
|
| Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
|
||||||
"this writes through a %s, which can only be read, so the element is a \
|
Loc.failk "check/store-through-const" loc
|
||||||
value and not a place. Write into a slice that can be written: \
|
"this changes the %s behind a %s, which can only be read through. A \
|
||||||
(slice (into v (vec-new %s))) copies v's elements into one"
|
container that has to change is handed over as a (Ptr %s)"
|
||||||
(Types.to_string view) (Types.to_string elem)
|
(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
|
(* 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
|
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 address of an expression, place or not: the type-erased runtime takes
|
||||||
the element [push] copies by pointer. *)
|
the element [push] copies by pointer. *)
|
||||||
let addr_of loc (e : Tast.expr) =
|
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 ──────────────────────────────
|
(* ── 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.Var v -> "y" ^ atom v
|
||||||
| Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e
|
| Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e
|
||||||
| Types.Slice (Types.Const, e) -> "k" ^ 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.Vec e -> "v" ^ thick_enc e
|
||||||
| Types.Option e -> "o" ^ thick_enc e
|
| Types.Option e -> "o" ^ thick_enc e
|
||||||
| Types.Array (n, e) -> Printf.sprintf "a%Ld-%s" n (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. *)
|
that never reads it costs one store the optimiser drops. *)
|
||||||
let declare_env ctx = function
|
let declare_env ctx = function
|
||||||
| Some _ as s -> s
|
| 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) =
|
let numeric_note ~(want : Types.t) ~(got : Types.t) =
|
||||||
if not (Types.is_numeric want && Types.is_numeric got) then ""
|
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"
|
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 got) (Types.to_string want) copy (Types.to_string want)
|
||||||
(Types.to_string want) (Types.to_string got)
|
(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) =
|
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
|
(* 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,
|
words, so the value is only retyped; the reverse is refused below,
|
||||||
with [const_note] naming the copy that would make it writable. *)
|
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 ->
|
when Types.const_widens ~from:got.Tast.ty ~into:w ->
|
||||||
{ got with Tast.ty = w }
|
{ got with Tast.ty = w }
|
||||||
| _ -> got
|
| _ -> 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. *)
|
(* 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 field_addr_of loc sty fty p i =
|
||||||
let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr sty) (Tast.Local p))) in
|
let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr (Types.Mut, sty)) (Tast.Local p))) in
|
||||||
mk loc (Types.Ptr fty) (Tast.Addr (Tast.Pfield (target, i)))
|
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
|
(* 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. *)
|
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
|
fail loc
|
||||||
"%s has no fields, so it is not a map key — every value of it would \
|
"%s has no fields, so it is not a map key — every value of it would \
|
||||||
be the same key" n;
|
be the same key" n;
|
||||||
let hparams = [ Types.Ptr sty; hash_ty; Types.Int Types.I64 ] in
|
let hparams = [ Types.Ptr (Types.Mut, sty); hash_ty; Types.Int Types.I64 ] in
|
||||||
let eparams = [ Types.Ptr sty; Types.Ptr sty; 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
|
(* Registered before the fields are walked, so a struct reached twice
|
||||||
through two different fields emits one pair and not two. A struct cannot
|
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.
|
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
|
hashes its bytes and a nested struct hashes field by field. Padding is
|
||||||
never reached, because nothing here addresses anything but a field. *)
|
never reached, because nothing here addresses anything but a field. *)
|
||||||
let hctx = invented_ctx env hash_ty in
|
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
|
let seed = fresh_slot ~name:"seed" hctx hash_ty in
|
||||||
ignore (fresh_slot ~name:"size" hctx (Types.Int Types.I64));
|
ignore (fresh_slot ~name:"size" hctx (Types.Int Types.I64));
|
||||||
let acc = fresh_slot ~name:"h" hctx hash_ty in
|
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
|
field that differs, which for a struct with a string field is the
|
||||||
difference between one memcmp and two. *)
|
difference between one memcmp and two. *)
|
||||||
let ectx = invented_ctx env (Types.Int Types.I8) in
|
let ectx = invented_ctx env (Types.Int Types.I8) in
|
||||||
let ap = fresh_slot ~name:"a" 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 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));
|
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 i8 v = mk loc (Types.Int Types.I8) (Tast.Int (v, Types.I8)) in
|
||||||
let checks =
|
let checks =
|
||||||
@ -3648,7 +3686,7 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
|
|||||||
List.filter_map
|
List.filter_map
|
||||||
(fun i ->
|
(fun i ->
|
||||||
match List.nth_opt args i with
|
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)
|
Some (mk loc t (Tast.Deref p), t)
|
||||||
| _ -> None)
|
| _ -> None)
|
||||||
tr.Shim.rekey
|
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
|
pointer is a hidden parameter and the name is a slot loaded from
|
||||||
it — a handler that passed [c] to something expecting the struct
|
it — a handler that passed [c] to something expecting the struct
|
||||||
would otherwise be handed an address. *)
|
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 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 = map_lr (fun e -> check hctx e) c.Ast.hbody in
|
||||||
let hbody =
|
let hbody =
|
||||||
@ -4609,7 +4647,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
|
|||||||
([ (cslot,
|
([ (cslot,
|
||||||
mk c.Ast.hloc ty
|
mk c.Ast.hloc ty
|
||||||
(Tast.Deref
|
(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)) ]
|
hbody)) ]
|
||||||
in
|
in
|
||||||
(* Named after the function it came out of, and numbered within it:
|
(* 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. *)
|
clause matched, and it cannot know which of them captured. *)
|
||||||
let fenv = declare_env hctx fenv in
|
let fenv = declare_env hctx fenv in
|
||||||
ctx.env.lifted <-
|
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);
|
slots = Array.of_list (List.rev hctx.slot_tys);
|
||||||
snames = Array.of_list (List.rev hctx.slot_names);
|
snames = Array.of_list (List.rev hctx.slot_names);
|
||||||
ret = Types.Unit; body = prefix hbody; fdefers = [];
|
ret = Types.Unit; body = prefix hbody; fdefers = [];
|
||||||
@ -6362,7 +6400,7 @@ and unknown_name : 'a. ?setting:bool -> ctx -> Loc.t -> string -> 'a =
|
|||||||
let sname =
|
let sname =
|
||||||
match ty with
|
match ty with
|
||||||
| Some (Types.Named n) when fields_named ctx.env n <> None -> Some n
|
| 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
|
| _ -> None
|
||||||
in
|
in
|
||||||
match sname, ty with
|
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
|
let has n = fields_named ctx.env n <> None in
|
||||||
match t.Tast.ty with
|
match t.Tast.ty with
|
||||||
| Types.Named n when has n -> t, n
|
| 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
|
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
|
(* 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
|
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
|
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. *)
|
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 ->
|
when Hashtbl.mem ctx.env.datas n ->
|
||||||
fail target.Ast.loc
|
fail target.Ast.loc
|
||||||
"%s is a data type, and its fields belong to a case — reach them with \
|
"%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
|
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
|
the address of a read-only element may be taken, and it is a store that is
|
||||||
refused. *)
|
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 =
|
and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
|
||||||
match p with
|
match p with
|
||||||
| Ast.Pvar name ->
|
| Ast.Pvar name ->
|
||||||
@ -6577,7 +6635,9 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
|
|||||||
| Ast.Pderef target ->
|
| Ast.Pderef target ->
|
||||||
let target = check ctx target in
|
let target = check ctx target in
|
||||||
(match target.Tast.ty with
|
(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 ->
|
| other ->
|
||||||
fail loc "deref takes a (Ptr T), found %s" (Types.to_string 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
|
| Types.Array (_, t) | Types.Slice (_, t) -> t
|
||||||
(* A string indexes to its bytes, and only to read them. *)
|
(* A string indexes to its bytes, and only to read them. *)
|
||||||
| Types.String ->
|
| 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
|
Types.Int Types.U8
|
||||||
| other ->
|
| other ->
|
||||||
fail i.Ast.loc "%s cannot be indexed" (Types.to_string 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
|
match idx with
|
||||||
| [ i ] ->
|
| [ i ] ->
|
||||||
let i = index_expr ctx i in
|
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
|
[ target; i; size_of loc elem; here loc ], elem
|
||||||
| _ ->
|
| _ ->
|
||||||
fail loc
|
fail loc
|
||||||
@ -8414,9 +8474,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
|||||||
| [ target; cur; k; v ] ->
|
| [ target; cur; k; v ] ->
|
||||||
let target = check ctx target in
|
let target = check ctx target in
|
||||||
let kt, vt = map_kv loc "map-next" target.Tast.ty 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 cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
|
||||||
let k = check ctx ~want:(Types.Ptr kt) k in
|
let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
|
||||||
let v = check ctx ~want:(Types.Ptr vt) v in
|
let v = check ctx ~want:(Types.Ptr (Types.Mut, vt)) v in
|
||||||
let found =
|
let found =
|
||||||
rt loc (Types.Int Types.I8) "flan_map_next"
|
rt loc (Types.Int Types.I8) "flan_map_next"
|
||||||
[ target; cur; k; v; size_of loc kt; size_of loc vt; here loc ]
|
[ 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 target = check ctx target in
|
||||||
let elem =
|
let elem =
|
||||||
match target.Tast.ty with
|
match target.Tast.ty with
|
||||||
| Types.Ptr t -> t
|
| Types.Ptr (_, t) -> t
|
||||||
| other ->
|
| other ->
|
||||||
fail loc
|
fail loc
|
||||||
"slice-from-ptr takes a (Ptr T) and the number of elements behind \
|
"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
|
fail n_loc
|
||||||
"slice-from-ptr length %Ld is negative" k
|
"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)
|
| _ -> assert false)
|
||||||
|
|
||||||
(* ── pointers ──────────────────────────────────────────────────── *)
|
(* ── pointers ──────────────────────────────────────────────────── *)
|
||||||
@ -8981,12 +9044,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
|
|||||||
or (deref p)"
|
or (deref p)"
|
||||||
| Some p ->
|
| Some p ->
|
||||||
let p, ty = check_place ~store:false ctx a.Ast.loc p in
|
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" ->
|
| "deref" ->
|
||||||
arity ctx loc name 1 args;
|
arity ctx loc name 1 args;
|
||||||
let a = check ctx (List.hd args) in
|
let a = check ctx (List.hd args) in
|
||||||
(match a.Tast.ty with
|
(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"
|
| other -> fail loc "deref takes a (Ptr T), found %s"
|
||||||
(Types.to_string other))
|
(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) =
|
let rec mentions v (t : Types.t) =
|
||||||
match t with
|
match t with
|
||||||
| Types.Var u -> String.equal u v
|
| 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.Option e -> mentions v e
|
||||||
| Types.Map (k, w) -> mentions v k || mentions v w
|
| Types.Map (k, w) -> mentions v k || mentions v w
|
||||||
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
|
| 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.Dyn -> true
|
||||||
| Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
|
| Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
|
||||||
| Types.Map (k, v) -> go k || go v
|
| 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.Fn _ -> false
|
||||||
| Types.Named n when not (List.mem n seen) ->
|
| Types.Named n when not (List.mem n seen) ->
|
||||||
let seen = n :: seen in
|
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]
|
It still terminates. This walk's own [seen] guards its own [Named]
|
||||||
recursion, and each crossing starts a separate finite walk of its own. *)
|
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.Array (_, e) | Types.Vec e | Types.Option e -> go e
|
||||||
| Types.Map (k, v) -> go k || go v
|
| Types.Map (k, v) -> go k || go v
|
||||||
| Types.Dyn | Types.Fn _ -> false
|
| 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
|
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
|
(* 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. *)
|
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.Fn _ -> None
|
||||||
| Types.Named n when not (List.mem n seen) ->
|
| Types.Named n when not (List.mem n seen) ->
|
||||||
let seen = n :: seen in
|
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
|
foreign parameter of pointer or slice type receives is the address
|
||||||
of a place. Below it the question is [dyn_behind_pointer]'s again. *)
|
of a place. Below it the question is [dyn_behind_pointer]'s again. *)
|
||||||
let below (t : Types.t) =
|
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
|
in
|
||||||
List.iteri
|
List.iteri
|
||||||
(fun i t ->
|
(fun i t ->
|
||||||
|
|||||||
@ -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 \
|
"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 \
|
as a NUL-terminated copy — the writes would be lost. const char * is \
|
||||||
a string; this one needs a declare-c saying (Ptr u8)"
|
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
|
| _ -> value_ty env s
|
||||||
end
|
end
|
||||||
else value_ty env s
|
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)))
|
Some (String.trim (String.sub s 0 (String.length s - 1)))
|
||||||
else None
|
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) =
|
let ptr_agrees env ~(c : string) (t : Ast.texpr) =
|
||||||
match (c_pointee c, t.Ast.t) with
|
match (c_pointee c, t.Ast.t) with
|
||||||
| Some inner, Ast.Tapp ("Ptr", [ elem ]) ->
|
(* A (Ptr const T) promises C will not write, so the header has to promise
|
||||||
(* [void *] agrees with a pointer to anything, and this is the judgement
|
it too: over a [T *] without const, C may write through storage Flan
|
||||||
call of the arm. C's [void *] is opaque about *what it points at* — that
|
holds read-only. *)
|
||||||
is the whole of what the spelling means — so there is no element type in
|
| Some inner, Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; elem ]) ->
|
||||||
the header to disagree with, and a check that reported one would be
|
strip_prefix "const " inner <> None
|
||||||
reporting [value_ty]'s guess of [u8] back at the author as if the header
|
&& ptr_agrees_elem env ~inner elem
|
||||||
had said it. What is *not* given up is that it is a pointer at all: the
|
| Some inner, Ast.Tapp ("Ptr", [ elem ]) -> ptr_agrees_elem env ~inner elem
|
||||||
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))
|
|
||||||
| _ -> false
|
| _ -> false
|
||||||
|
|
||||||
(* The two together, for the one caller that still has the C spelling. A
|
(* The two together, for the one caller that still has the C spelling. A
|
||||||
|
|||||||
@ -2726,7 +2726,7 @@ let type_of_spelling t spelling : (Types.t, string) result =
|
|||||||
let addr_extern : Tast.extern =
|
let addr_extern : Tast.extern =
|
||||||
{ Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr";
|
{ Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr";
|
||||||
eparams = [ Types.Int Types.I64 ];
|
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.
|
(* 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;
|
extra := ty :: !extra;
|
||||||
i) }
|
i) }
|
||||||
in
|
in
|
||||||
let pty = Types.Ptr ty in
|
let pty = Types.Ptr (Types.Mut, ty) in
|
||||||
let root =
|
let root =
|
||||||
{ Tast.e =
|
{ Tast.e =
|
||||||
Tast.Prim
|
Tast.Prim
|
||||||
@ -2771,7 +2771,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
|
|||||||
("flan/dev-addr",
|
("flan/dev-addr",
|
||||||
[ { Tast.e = Tast.Int (Int64.of_int addr, Types.I64);
|
[ { Tast.e = Tast.Int (Int64.of_int addr, Types.I64);
|
||||||
ty = Types.Int Types.I64; loc } ]);
|
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 }
|
ty = pty; loc }
|
||||||
in
|
in
|
||||||
match Render.render c 0 root with
|
match Render.render c 0 root with
|
||||||
@ -2935,7 +2935,7 @@ let inspect_addr t ~addr ~want_type =
|
|||||||
| Ok v ->
|
| Ok v ->
|
||||||
ok
|
ok
|
||||||
([ Printf.sprintf ":addr %d" addr;
|
([ 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 ]
|
":value " ^ Wire.quote v; ":live " ^ live ]
|
||||||
@ told @ where))))))
|
@ told @ where))))))
|
||||||
|
|
||||||
|
|||||||
14
lib/emit.ml
14
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.Bool -> basic "bool" 8 "DW_ATE_boolean"
|
||||||
| Types.Enum e -> basic e 32 "DW_ATE_signed"
|
| Types.Enum e -> basic e 32 "DW_ATE_signed"
|
||||||
| Types.Unit | Types.Never -> composite (Types.to_string t) []
|
| Types.Unit | Types.Never -> composite (Types.to_string t) []
|
||||||
| Types.Ptr e ->
|
| Types.Ptr (_, e) ->
|
||||||
let id = dalloc d in
|
let id = dalloc d in
|
||||||
Hashtbl.replace d.dtys key id;
|
Hashtbl.replace d.dtys key id;
|
||||||
(* [(Ptr Unit)] and [(Ptr Never)] are the opaque pointer, and a DWARF
|
(* [(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. *)
|
capacity, so two members are the whole truth about a slice. *)
|
||||||
| Types.String ->
|
| Types.String ->
|
||||||
composite "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) ->
|
| Types.Slice (_, e) ->
|
||||||
composite (Types.to_string t)
|
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 ->
|
| Types.Option e ->
|
||||||
composite (Types.to_string t)
|
composite (Types.to_string t)
|
||||||
[ ("tag", Types.Int Types.U8); ("value", e) ]
|
[ ("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. *)
|
would put the reader's offsets out by one. *)
|
||||||
| Types.Vec e ->
|
| Types.Vec e ->
|
||||||
composite (Types.to_string t)
|
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);
|
("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
|
||||||
("epoch", Types.Int Types.I64) ]
|
("epoch", Types.Int Types.I64) ]
|
||||||
(* Five fields again, and shown as five for the same reason: a debugger
|
(* 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. *)
|
describing a field that is not there. *)
|
||||||
| Types.Map (k, v) ->
|
| Types.Map (k, v) ->
|
||||||
composite (Types.to_string t)
|
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);
|
("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64);
|
||||||
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|
||||||
|> fun n -> ignore k; ignore v; n
|
|> 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. *)
|
locals, where they are under the names the source gave them. *)
|
||||||
| Types.Fn _ ->
|
| Types.Fn _ ->
|
||||||
composite (Types.to_string t)
|
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
|
(* 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
|
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
|
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.Pindex (target, idx) -> element_addr f target idx
|
||||||
| Tast.Pderef target ->
|
| Tast.Pderef target ->
|
||||||
let t = match target.Tast.ty with
|
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
|
in
|
||||||
value f target, t
|
value f target, t
|
||||||
|
|
||||||
|
|||||||
@ -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 [<ptr>]. That
|
An address the registry never saw is neither: it prints [<ptr>]. That
|
||||||
is a stack local, a global, or a pointer from C, and the shadow stack
|
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. *)
|
and the static type table already answer for the first two by name. *)
|
||||||
| Types.Ptr t ->
|
| Types.Ptr (_, t) ->
|
||||||
(match c.ptrs with
|
(match c.ptrs with
|
||||||
| None -> [ lit "<ptr>" ]
|
| None -> [ lit "<ptr>" ]
|
||||||
| Some pt ->
|
| Some pt ->
|
||||||
|
|||||||
@ -1202,12 +1202,12 @@ let externs : Tast.extern list =
|
|||||||
is. See [render_locals]. *)
|
is. See [render_locals]. *)
|
||||||
{ Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot";
|
{ Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot";
|
||||||
eparams = [ Types.Int Types.I64; Types.Int Types.I64 ];
|
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
|
(* The condition the stopped program is holding, same contract: the agent
|
||||||
resolves it against the snapshot on top when the thunk runs, and NULL
|
resolves it against the snapshot on top when the thunk runs, and NULL
|
||||||
when there is none. See [render_condition]. *)
|
when there is none. See [render_condition]. *)
|
||||||
{ Tast.ename = "flan/dev-cond"; esym = "flan_agent_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 };
|
eloc = Loc.unknown };
|
||||||
(* The character beside a rendered byte. See [Render.pointers]. *)
|
(* The character beside a rendered byte. See [Render.pointers]. *)
|
||||||
{ Tast.ename = "flan/dev-emit-u8-char"; esym = "flan_dev_emit_u8_char";
|
{ 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
|
written" is already the right rendering for an address the registry
|
||||||
never saw. *)
|
never saw. *)
|
||||||
{ Tast.ename = "flan/reg-live"; esym = "flan_dev_reg_live";
|
{ 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 };
|
eret = Types.Int Types.I32; eloc = Loc.unknown };
|
||||||
{ Tast.ename = "flan/reg-emit"; esym = "flan_dev_reg_emit";
|
{ 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 } ]
|
eret = Types.Int Types.I32; eloc = Loc.unknown } ]
|
||||||
|
|
||||||
(* The REPL's emitter. Each piece is one extern call: the dev runtime already
|
(* 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 ask name (p : Tast.expr) : Tast.expr =
|
||||||
let loc = p.Tast.loc in
|
let loc = p.Tast.loc in
|
||||||
let byte =
|
let byte =
|
||||||
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Int Types.U8)), [ p ]);
|
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, (Types.Int Types.U8))), [ p ]);
|
||||||
ty = Types.Ptr (Types.Int Types.U8); loc }
|
ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
|
||||||
in
|
in
|
||||||
{ Tast.e = Tast.Call (name, [ byte ]); ty = i32; loc }
|
{ Tast.e = Tast.Call (name, [ byte ]); ty = i32; loc }
|
||||||
in
|
in
|
||||||
@ -1405,11 +1405,11 @@ let render_locals ?(origin = "<locals>") t ~frame ~(fn : Tast.fn) ~bound
|
|||||||
in
|
in
|
||||||
let address =
|
let address =
|
||||||
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx i ]);
|
{ 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
|
in
|
||||||
let typed =
|
let typed =
|
||||||
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
|
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
|
||||||
ty = Types.Ptr ty; loc }
|
ty = Types.Ptr (Types.Mut, ty); loc }
|
||||||
in
|
in
|
||||||
let v = { Tast.e = Tast.Deref typed; ty; loc } in
|
let v = { Tast.e = Tast.Deref typed; ty; loc } in
|
||||||
match Render.render c 0 v with
|
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 cty = Types.Named st.Tast.sname in
|
||||||
let address =
|
let address =
|
||||||
{ Tast.e = Tast.Call ("flan/dev-cond", []);
|
{ 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
|
in
|
||||||
let typed =
|
let typed =
|
||||||
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr cty), [ address ]);
|
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, cty)), [ address ]);
|
||||||
ty = Types.Ptr cty; loc }
|
ty = Types.Ptr (Types.Mut, cty); loc }
|
||||||
in
|
in
|
||||||
let root = { Tast.e = Tast.Deref typed; ty = cty; loc } in
|
let root = { Tast.e = Tast.Deref typed; ty = cty; loc } in
|
||||||
let one i (f : Tast.field) =
|
let one i (f : Tast.field) =
|
||||||
@ -1770,11 +1770,11 @@ let render_slot ?(origin = "<inspect>") t ~frame ~(fn : Tast.fn) ~slot ~path
|
|||||||
let ty = fn.Tast.slots.(slot) in
|
let ty = fn.Tast.slots.(slot) in
|
||||||
let address =
|
let address =
|
||||||
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
|
{ 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
|
in
|
||||||
let typed =
|
let typed =
|
||||||
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
|
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
|
||||||
ty = Types.Ptr ty; loc }
|
ty = Types.Ptr (Types.Mut, ty); loc }
|
||||||
in
|
in
|
||||||
let root = { Tast.e = Tast.Deref typed; ty; loc } in
|
let root = { Tast.e = Tast.Deref typed; ty; loc } in
|
||||||
let rec walk v = function
|
let rec walk v = function
|
||||||
@ -1805,7 +1805,7 @@ let render_slot ?(origin = "<inspect>") t ~frame ~(fn : Tast.fn) ~slot ~path
|
|||||||
Tast.Prim
|
Tast.Prim
|
||||||
(Tast.Cast (Types.Int Types.I64),
|
(Tast.Cast (Types.Int Types.I64),
|
||||||
[ { Tast.e = Tast.Prim (Tast.AddrOf, [ v ]);
|
[ { 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 }
|
ty = Types.Int Types.I64; loc }
|
||||||
in
|
in
|
||||||
let newline =
|
let newline =
|
||||||
@ -1985,11 +1985,11 @@ let write_slot ?(origin = "<set>") t ~frame ~(fn : Tast.fn) ~slot ~path
|
|||||||
let ty = fn.Tast.slots.(slot) in
|
let ty = fn.Tast.slots.(slot) in
|
||||||
let address =
|
let address =
|
||||||
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
|
{ 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
|
in
|
||||||
let typed =
|
let typed =
|
||||||
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
|
{ Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
|
||||||
ty = Types.Ptr ty; loc }
|
ty = Types.Ptr (Types.Mut, ty); loc }
|
||||||
in
|
in
|
||||||
let root = { Tast.e = Tast.Deref typed; ty; loc } in
|
let root = { Tast.e = Tast.Deref typed; ty; loc } in
|
||||||
let rec walk v = function
|
let rec walk v = function
|
||||||
|
|||||||
@ -221,6 +221,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
|
|||||||
else
|
else
|
||||||
fail loc "%s is %s, which is not a type this shim generator knows" what n)
|
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", [ 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", _) ->
|
| Ast.Tapp ("Option", _) ->
|
||||||
fail loc
|
fail loc
|
||||||
"%s is an Option, which C has no shape for — declare what C returns and \
|
"%s is an Option, which C has no shape for — declare what C returns and \
|
||||||
|
|||||||
10
lib/types.ml
10
lib/types.ml
@ -43,7 +43,7 @@ type t =
|
|||||||
| Slice of access * t (* [T] [const T] ptr+len, non-owning *)
|
| Slice of access * t (* [T] [const T] ptr+len, non-owning *)
|
||||||
| Array of int64 * t (* [n T] inline, a value, copies *)
|
| Array of int64 * t (* [n T] inline, a value, copies *)
|
||||||
| Map of t * t (* (Map K V) *)
|
| 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
|
(* [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
|
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
|
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
|
| Slice (a, x), Slice (b, y) -> a = b && equal x y
|
||||||
| Array (n, x), Array (m, y) -> Int64.equal n m && 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'
|
| 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
|
| Alloc, Alloc -> true
|
||||||
| Vec x, Vec y -> equal x y
|
| Vec x, Vec y -> equal x y
|
||||||
| Option x, Option 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 ^ "]"
|
| Slice (Const, t) -> "[const " ^ to_string t ^ "]"
|
||||||
| Array (n, t) -> Printf.sprintf "[%Ld %s]" n (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)
|
| 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"
|
| Alloc -> "Allocator"
|
||||||
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
||||||
| Option t -> "(Option " ^ to_string t ^ ")"
|
| Option t -> "(Option " ^ to_string t ^ ")"
|
||||||
@ -344,7 +345,8 @@ let join a b =
|
|||||||
same at run time. *)
|
same at run time. *)
|
||||||
let rec const_widens ~(from : t) ~(into : t) =
|
let rec const_widens ~(from : t) ~(into : t) =
|
||||||
match from, into with
|
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
|
| _ -> false
|
||||||
|
|
||||||
(* A function of one signature standing where another is wanted, when the
|
(* A function of one signature standing where another is wanted, when the
|
||||||
|
|||||||
18
lib/x86.ml
18
lib/x86.ml
@ -1554,7 +1554,7 @@ type arg =
|
|||||||
move-only container by address. *)
|
move-only container by address. *)
|
||||||
let classify_c (l : loc) (t : Types.t) =
|
let classify_c (l : loc) (t : Types.t) =
|
||||||
match t with
|
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.Unit | Types.Never -> []
|
||||||
| Types.Vec _ | Types.Map _ -> [ Aptr l ]
|
| Types.Vec _ | Types.Map _ -> [ Aptr l ]
|
||||||
(* A fixed array crossing into a dyn view (M2 item 3) needs its address for
|
(* 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;
|
store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8;
|
||||||
(match env with
|
(match env with
|
||||||
| None -> xor_rr f.b ~dst:rax ~src:rax
|
| 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
|
store_int f.b ~src:rax ~mm:(lmem f (shift dst 8) ~scratch:r11) ~size:8
|
||||||
| Tast.FnAddr r ->
|
| Tast.FnAddr r ->
|
||||||
fnaddr_at f ~loc:e.Tast.loc ~reg:rax 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 c = eval f callee in
|
||||||
let env =
|
let env =
|
||||||
match callee.Tast.ty with
|
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
|
| _ -> None
|
||||||
in
|
in
|
||||||
call_flan f ?env ~target:(`Loc c) ~args ~rty:t dst
|
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
|
(match h.Tast.henv with
|
||||||
| Some ev ->
|
| Some ev ->
|
||||||
let l = scoped f (fun () -> eval f ev) in
|
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);
|
| None -> xor_rr f.b ~dst:rax ~src:rax);
|
||||||
store_int f.b ~src:rax ~mm:(Frame (slot + h_env)) ~size:8;
|
store_int f.b ~src:rax ~mm:(Frame (slot + h_env)) ~size:8;
|
||||||
lea f.b ~dst:rdi ~mm:(Frame slot);
|
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 =
|
and field_loc f (base : loc) (ty : Types.t) i =
|
||||||
match ty with
|
match ty with
|
||||||
| Types.Named sn -> shift base (List.nth (field_offsets f sn) i)
|
| 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)
|
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.String | Types.Slice _ -> shift base (if i = 0 then 0 else 8)
|
||||||
| Types.Option el -> let ot, ov = option_lay f el in
|
| 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 ->
|
| i :: rest ->
|
||||||
let elem =
|
let elem =
|
||||||
match ty with
|
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
|
| Types.String -> Types.Int Types.U8
|
||||||
| t -> unsupported "index into %s" (Types.to_string t)
|
| t -> unsupported "index into %s" (Types.to_string t)
|
||||||
in
|
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 =
|
and element f (base : loc) (ty : Types.t) (i : Tast.expr) : loc =
|
||||||
let elem =
|
let elem =
|
||||||
match ty with
|
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
|
| Types.String -> Types.Int Types.U8
|
||||||
| t -> unsupported "index into %s" (Types.to_string t)
|
| t -> unsupported "index into %s" (Types.to_string t)
|
||||||
in
|
in
|
||||||
@ -2966,7 +2966,7 @@ and call_flan f ?env ~target ~args ~rty dst =
|
|||||||
in
|
in
|
||||||
(* The channel is this frame's own: a callee that transfers writes through
|
(* 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. *)
|
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
|
(* 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
|
a [(Fn ...)] value, which cannot know whether the body it reaches
|
||||||
declared one. Every other call passes what it always passed — this is
|
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
|
args
|
||||||
in
|
in
|
||||||
let flat = List.concat_map (fun (l, ty) -> classify_c l ty) vals 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
|
let nsse = emit_args f flat in
|
||||||
(* [al] is how many SSE registers were used, which a variadic callee reads.
|
(* [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. *)
|
Harmless on a fixed one, and a [declare] does not say which it is. *)
|
||||||
|
|||||||
@ -2325,7 +2325,7 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) {
|
|||||||
}
|
}
|
||||||
{
|
{
|
||||||
static const char why[] =
|
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";
|
"a null, or a stack overflow\n";
|
||||||
crash_puts(why, sizeof why - 1);
|
crash_puts(why, sizeof why - 1);
|
||||||
}
|
}
|
||||||
|
|||||||
@ -95,10 +95,10 @@ forever="dev-loop dev-watch dev-chatty agent-auto"
|
|||||||
# sweep now and they are five of the MATCHes.
|
# sweep now and they are five of the MATCHes.
|
||||||
|
|
||||||
# The one whose whole point is a fault, and which therefore cannot be compared
|
# 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
|
# at this sweep's optimisation level. dev-segv stores through a null pointer,
|
||||||
# string literal's bytes, which is a store into .rodata: LLVM at -O2 deletes it
|
# which is undefined: what LLVM at -O2 does with it is its own business, and
|
||||||
# as undefined and exits 0, and this backend has no optimiser and exits 139.
|
# this backend has no optimiser and exits 139. That is not a lowering
|
||||||
# That is not a lowering disagreement. test_dev.ml builds it in a dev session,
|
# disagreement. test_dev.ml builds it in a dev session,
|
||||||
# where the fault is the thing asserted. It also calls agent/start, so it
|
# 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
|
# leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks
|
||||||
# in the break loop instead of dying.
|
# in the break loop instead of dying.
|
||||||
|
|||||||
@ -18,6 +18,9 @@
|
|||||||
(set n (+ n (length (at parts i)))))
|
(set n (+ n (length (at parts i)))))
|
||||||
n))
|
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
|
;; 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.
|
;; one returning a writable slice where a read-only one is wanted.
|
||||||
(defn rd [s [const u8]] i32 (length s))
|
(defn rd [s [const u8]] i32 (length s))
|
||||||
@ -54,5 +57,9 @@
|
|||||||
(println (string (slice (join (slice f) (bytes-view "-"))))))
|
(println (string (slice (join (slice f) (bytes-view "-"))))))
|
||||||
(println (at r 0))
|
(println (at r 0))
|
||||||
(println (call-rd rd) (call-bare rd) (call-mk mk))
|
(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))
|
(free names))
|
||||||
0)
|
0)
|
||||||
|
|||||||
@ -1,22 +1,21 @@
|
|||||||
;;;; The dogfooding crash, replayed on purpose: a store through a pointer to
|
;;;; A hardware fault, taken on purpose: a store through a null pointer takes
|
||||||
;;;; a string literal's bytes lands in read-only memory and takes SIGSEGV. In
|
;;;; SIGSEGV. In a dev session that used to kill the whole process — daemon,
|
||||||
;;;; a dev session that used to kill the whole process — daemon, compiler and
|
;;;; compiler and socket together, with no message at all. The dev build's
|
||||||
;;;; socket together, with no message at all. The dev build's crash handler
|
;;;; crash handler turns it into the same park the no-channel traps take: one
|
||||||
;;;; turns it into the same park the no-channel traps take: one line naming
|
;;;; line naming the address and the frame, then the break loop, with the
|
||||||
;;;; the address and the frame, then the break loop, with the daemon alive
|
;;;; daemon alive and answering behind it. There is no restart to list — a
|
||||||
;;;; and answering behind it. There is no restart to list — a faulting
|
;;;; faulting instruction has nowhere to resume at — which is the same
|
||||||
;;;; instruction has nowhere to resume at — which is the same empty-list
|
;;;; empty-list shape dev-trap-null-alloc.flan pins for free-all.
|
||||||
;;;; shape dev-trap-null-alloc.flan pins for free-all.
|
|
||||||
;;;;
|
;;;;
|
||||||
;;;; Through a pointer, because a store through the [const u8] itself is
|
;;;; The crash that first raised this was a write through a bytes-view of a
|
||||||
;;;; refused at compile time; a (Ptr T) is the C boundary, where nothing is
|
;;;; string literal, which no longer compiles; a zeroed pointer is the
|
||||||
;;;; checked.
|
;;;; surviving way to fault.
|
||||||
(import agent "vendor:agent")
|
(import agent "vendor:agent")
|
||||||
|
|
||||||
|
(defonce nowhere (Ptr u8))
|
||||||
|
|
||||||
(defn main [] i32
|
(defn main [] i32
|
||||||
(agent/start "/tmp/flan-dev-segv-fallback.sock")
|
(agent/start "/tmp/flan-dev-segv-fallback.sock")
|
||||||
(let [v (bytes-view "INSERTIONSORT")
|
(set (deref nowhere) \Z)
|
||||||
p (addr (at v 0))]
|
(println "not reached")
|
||||||
(set (deref p) \Z)
|
0)
|
||||||
(print (string v))
|
|
||||||
0))
|
|
||||||
|
|||||||
@ -872,7 +872,7 @@ let () =
|
|||||||
(* [const T]: the checker's alone, so the three builds agree and every
|
(* [const T]: the checker's alone, so the three builds agree and every
|
||||||
row is about which values reach which parameters. *)
|
row is about which values reach which parameters. *)
|
||||||
let const_slice_out =
|
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
|
in
|
||||||
outputs "const slices" "programs/const-slice.flan" const_slice_out;
|
outputs "const slices" "programs/const-slice.flan" const_slice_out;
|
||||||
outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"
|
outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"
|
||||||
|
|||||||
@ -1922,7 +1922,7 @@ let () =
|
|||||||
if refault then begin
|
if refault then begin
|
||||||
let faulting =
|
let faulting =
|
||||||
"(:op \"eval-expr\" :code \
|
"(: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\")"
|
:file \"/tmp/buf.flan\")"
|
||||||
in
|
in
|
||||||
(match ask faulting with _ -> () | exception _ -> ());
|
(match ask faulting with _ -> () | exception _ -> ());
|
||||||
@ -2028,9 +2028,8 @@ let () =
|
|||||||
word. The dev build's crash handler (flan_dev_crash_enable) enters the
|
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
|
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
|
asserts for them holds here too: stopped and describable, an eval still
|
||||||
answered, a resume refused. The program writes through a pointer to
|
answered, a resume refused. The program stores through a null
|
||||||
a literal's bytes, which is the surviving spelling of that crash: a
|
pointer: the bytes-view write that first crashed no longer compiles. *)
|
||||||
store through the bytes-view itself no longer compiles. *)
|
|
||||||
trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" [];
|
trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" [];
|
||||||
|
|
||||||
(* ── The locals of a stopped frame ─────────────────────────────── *)
|
(* ── The locals of a stopped frame ─────────────────────────────── *)
|
||||||
|
|||||||
@ -2238,12 +2238,10 @@ let () =
|
|||||||
rejects_check "set through a string's slice"
|
rejects_check "set through a string's slice"
|
||||||
"(defn f [s string] () (set (at (slice s 1) 0) 65))"
|
"(defn f [s string] () (set (at (slice s 1) 0) 65))"
|
||||||
~needle:"not a place";
|
~needle:"not a place";
|
||||||
(* The address of one is the same question and gets the same answer, so
|
(* The address of one is a (Ptr const u8), so it is not a (Ptr u8). *)
|
||||||
the message has to fit a reader who asked for a pointer and not a
|
rejects_check "the address of a string's byte is read-only"
|
||||||
store. *)
|
|
||||||
rejects_check "the address of a string's byte"
|
|
||||||
"(defn f [s string] (Ptr u8) (addr (at s 0)))"
|
"(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
|
(* And a string is still not a [u8]: slicing one does not smuggle a byte
|
||||||
slice out of it. *)
|
slice out of it. *)
|
||||||
rejects_check "a string slice is not a byte slice"
|
rejects_check "a string slice is not a byte slice"
|
||||||
@ -2322,6 +2320,47 @@ let () =
|
|||||||
"(defn mk [] [const u8] (bytes-view \"a\")) \
|
"(defn mk [] [const u8] (bytes-view \"a\")) \
|
||||||
(defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))"
|
(defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))"
|
||||||
~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])";
|
~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"
|
rejects_check "const is not a name a constant can have"
|
||||||
"(defconst const 4)" ~needle:"const cannot be declared";
|
"(defconst const 4)" ~needle:"const cannot be declared";
|
||||||
(* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)
|
(* 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"
|
accepts "under a const slice the element converts too"
|
||||||
"(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))";
|
"(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))";
|
||||||
accepts "the address of a const element, for C"
|
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"
|
accepts "a generic reader takes both"
|
||||||
"(defn f [a [const i32] b [i32]] i64 (+ (sum-i32 a) (sum-i32 b)))";
|
"(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. *)
|
something different in a parameter than it does anywhere else. *)
|
||||||
emits "const char * as a string parameter"
|
emits "const char * as a string parameter"
|
||||||
"(declare-c name-length [text string] i32 \"name_length\")";
|
"(declare-c name-length [text string] i32 \"name_length\")";
|
||||||
emits "a pointer parameter"
|
(* const int * is a pointer C promises not to write through. *)
|
||||||
"(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")";
|
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
|
(* 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 —
|
describes it once, so both names have to land on the one defstruct —
|
||||||
raylib does exactly this with Texture2D and TextureCubemap. *)
|
raylib does exactly this with Texture2D and TextureCubemap. *)
|
||||||
@ -5140,6 +5180,10 @@ let () =
|
|||||||
"(declare-c name-length [text string] i32 \"name_length\")";
|
"(declare-c name-length [text string] i32 \"name_length\")";
|
||||||
agreed "a pointer that matches the header exactly"
|
agreed "a pointer that matches the header exactly"
|
||||||
"(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")";
|
"(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
|
(* 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. *)
|
the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *)
|
||||||
agreed "any pointer where the header says void *"
|
agreed "any pointer where the header says void *"
|
||||||
@ -5155,12 +5199,17 @@ let () =
|
|||||||
name the disagreement. *)
|
name the disagreement. *)
|
||||||
differs "a pointer to the wrong named type"
|
differs "a pointer to the wrong named type"
|
||||||
"(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")"
|
"(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"
|
differs "a pointer to the wrong width"
|
||||||
"(declare-c count-at [values (Ptr f64) n i32] i32 \"count_at\")"
|
"(declare-c count-at [values (Ptr f64) n i32] i32 \"count_at\")"
|
||||||
"parameter values is (Ptr f64)";
|
"parameter values is (Ptr f64)";
|
||||||
(* void * gives up the element type and nothing else. It is still a pointer,
|
(* void * gives up the element type and nothing else. It is still a pointer,
|
||||||
and a scalar declared against one is still a finding. *)
|
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 *"
|
differs "a scalar where the header says void *"
|
||||||
"(declare-c blit [dst i64 src (Ptr u8) n i32] \"blit\")"
|
"(declare-c blit [dst i64 src (Ptr u8) n i32] \"blit\")"
|
||||||
"parameter dst is i64";
|
"parameter dst is i64";
|
||||||
|
|||||||
@ -441,9 +441,8 @@ let dev_sweep () =
|
|||||||
sanitized run must produce ASan's report and must NOT produce the
|
sanitized run must produce ASan's report and must NOT produce the
|
||||||
handler's line, and that is the assertion.
|
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
|
And it has to be built at -O0. At the sweep's -O2 a store through a null
|
||||||
pointer to a string literal's bytes does not fault at all — measured, both
|
pointer is undefined and need not fault — so a case that is about what happens
|
||||||
builds print the unmodified string — so a case that is about what happens
|
|
||||||
on a fault has to be compiled where the fault happens. Same family as the
|
on a fault has to be compiled where the fault happens. Same family as the
|
||||||
-O0/-O2 split [unchecked_controls] records for bounds.flan.
|
-O0/-O2 split [unchecked_controls] records for bounds.flan.
|
||||||
|
|
||||||
|
|||||||
54
vendor/raylib/generated.flan
vendored
54
vendor/raylib/generated.flan
vendored
@ -78,7 +78,7 @@
|
|||||||
(declare-c load-file-data [file-name string data-size (Ptr i32)] (Ptr u8) "LoadFileData")
|
(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 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 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 file-exists [file-name string] bool "FileExists")
|
||||||
(declare-c directory-exists [dir-path string] bool "DirectoryExists")
|
(declare-c directory-exists [dir-path string] bool "DirectoryExists")
|
||||||
(declare-c file-extension? [file-name string ext string] bool "IsFileExtension")
|
(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 path-file? [path string] bool "IsPathFile")
|
||||||
(declare-c file-name-valid? [file-name string] bool "IsFileNameValid")
|
(declare-c file-name-valid? [file-name string] bool "IsFileNameValid")
|
||||||
(declare-c file-dropped? [] bool "IsFileDropped")
|
(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 compress-data [data (Ptr const 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 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 u8) output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64")
|
(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-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-md5 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeMD5")
|
||||||
(declare-c compute-sha1 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeSHA1")
|
(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 set-mouse-scale [scale-x f32 scale-y f32] "SetMouseScale")
|
||||||
(declare-c get-mouse-wheel-move-v [] Vector2 "GetMouseWheelMoveV")
|
(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 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-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 [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")
|
(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-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-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-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-fan-raw [points (Ptr const 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-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 [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 [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-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-linear-raw [points (Ptr const 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-basis-raw [points (Ptr const 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-catmull-rom-raw [points (Ptr const 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-quadratic-raw [points (Ptr const 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-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-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-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")
|
(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 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-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 [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-texture [texture Texture2D] Image "LoadImageFromTexture")
|
||||||
(declare-c load-image-from-screen [] Image "LoadImageFromScreen")
|
(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")
|
(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-mask [image (Ptr Image) alpha-mask Image] "ImageAlphaMask")
|
||||||
(declare-c image-alpha-premultiply [image (Ptr Image)] "ImageAlphaPremultiply")
|
(declare-c image-alpha-premultiply [image (Ptr Image)] "ImageAlphaPremultiply")
|
||||||
(declare-c image-blur-gaussian [image (Ptr Image) blur-size i32] "ImageBlurGaussian")
|
(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-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-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")
|
(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 [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 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 load-texture-cubemap [image Image layout i32] Texture2D "LoadTextureCubemap")
|
||||||
(declare-c update-texture [texture Texture2D pixels (Ptr u8)] "UpdateTexture")
|
(declare-c update-texture [texture Texture2D pixels (Ptr const u8)] "UpdateTexture")
|
||||||
(declare-c update-texture-rec [texture Texture2D rec Rectangle pixels (Ptr u8)] "UpdateTextureRec")
|
(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 gen-texture-mipmaps [texture (Ptr Texture2D)] "GenTextureMipmaps")
|
||||||
(declare-c set-texture-wrap [texture Texture2D wrap i32] "SetTextureWrap")
|
(declare-c set-texture-wrap [texture Texture2D wrap i32] "SetTextureWrap")
|
||||||
(declare-c color-is-equal [col-1 Color col-2 Color] bool "ColorIsEqual")
|
(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 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 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-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-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 u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32 type i32] (Ptr GlyphInfo) "LoadFontData")
|
(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 GlyphInfo) glyph-recs (Ptr (Ptr Rectangle)) glyph-count i32 font-size i32 padding i32 pack-method i32] Image "GenImageFontAtlas")
|
(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 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 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-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 set-text-line-spacing [spacing i32] "SetTextLineSpacing")
|
||||||
(declare-c load-codepoints [text string count (Ptr i32)] (Ptr i32) "LoadCodepoints")
|
(declare-c load-codepoints [text string count (Ptr i32)] (Ptr i32) "LoadCodepoints")
|
||||||
(declare-c unload-codepoints [codepoints (Ptr i32)] "UnloadCodepoints")
|
(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-is-equal [text-1 string text-2 string] bool "TextIsEqual")
|
||||||
(declare-c text-length [text string] u32 "TextLength")
|
(declare-c text-length [text string] u32 "TextLength")
|
||||||
(declare-c text-subtext [text string position i32 length i32] string "TextSubtext")
|
(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-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-find-index [text string find string] i32 "TextFindIndex")
|
||||||
(declare-c text-to-upper [text string] string "TextToUpper")
|
(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-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-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-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-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-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")
|
(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-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 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 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 unload-mesh [mesh Mesh] "UnloadMesh")
|
||||||
(declare-c get-mesh-bounding-box [mesh Mesh] BoundingBox "GetMeshBoundingBox")
|
(declare-c get-mesh-bounding-box [mesh Mesh] BoundingBox "GetMeshBoundingBox")
|
||||||
(declare-c gen-mesh-tangents [mesh (Ptr Mesh)] "GenMeshTangents")
|
(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-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-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 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 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 u8) sample-count i32] "UpdateSound")
|
(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 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 load-audio-stream [sample-rate u32 sample-size u32 channels u32] AudioStream "LoadAudioStream")
|
||||||
(declare-c audio-stream-valid? [stream AudioStream] bool "IsAudioStreamValid")
|
(declare-c audio-stream-valid? [stream AudioStream] bool "IsAudioStreamValid")
|
||||||
(declare-c unload-audio-stream [stream AudioStream] "UnloadAudioStream")
|
(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 audio-stream-processed? [stream AudioStream] bool "IsAudioStreamProcessed")
|
||||||
(declare-c play-audio-stream [stream AudioStream] "PlayAudioStream")
|
(declare-c play-audio-stream [stream AudioStream] "PlayAudioStream")
|
||||||
(declare-c pause-audio-stream [stream AudioStream] "PauseAudioStream")
|
(declare-c pause-audio-stream [stream AudioStream] "PauseAudioStream")
|
||||||
|
|||||||
26
vendor/raylib/raylib.flan
vendored
26
vendor/raylib/raylib.flan
vendored
@ -582,10 +582,10 @@
|
|||||||
;; out-of-bounds read, and raylib answers false for a polygon with no points
|
;; out-of-bounds read, and raylib answers false for a polygon with no points
|
||||||
;; anyway.
|
;; anyway.
|
||||||
(declare-c collision-point-poly?-raw
|
(declare-c collision-point-poly?-raw
|
||||||
[point Vector2 points (Ptr Vector2) count i32] bool
|
[point Vector2 points (Ptr const Vector2) count i32] bool
|
||||||
"CheckCollisionPointPoly")
|
"CheckCollisionPointPoly")
|
||||||
|
|
||||||
(defn collision-point-poly? [point Vector2 points [Vector2]] bool
|
(defn collision-point-poly? [point Vector2 points [const Vector2]] bool
|
||||||
(if (= (length points) 0)
|
(if (= (length points) 0)
|
||||||
false
|
false
|
||||||
(collision-point-poly?-raw point (addr (at points 0)) (length points))))
|
(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
|
;; 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.
|
;; slice apart, which is where that idiom lives everywhere else in this file.
|
||||||
(declare-c load-image-from-memory-raw
|
(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")
|
"LoadImageFromMemory")
|
||||||
|
|
||||||
;; Empty is answered here rather than passed on, exactly as in
|
;; 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
|
;; Each -raw below is a generated declaration whose name moved aside; see the
|
||||||
;; `name` lines at the foot of `bindings`.
|
;; `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)
|
(when (> (length points) 0)
|
||||||
(draw-line-strip-raw (addr (at points 0)) (length points) color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-triangle-fan-raw (addr (at points 0)) (length points) color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-triangle-strip-raw (addr (at points 0)) (length points) color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-triangle-strip-3d-raw (addr (at points 0)) (length points) color)))
|
(draw-triangle-strip-3d-raw (addr (at points 0)) (length points) color)))
|
||||||
|
|
||||||
;; The five spline drawers. raylib reads the same point array five different
|
;; The five spline drawers. raylib reads the same point array five different
|
||||||
;; ways; the only difference between these wrappers is which one it calls.
|
;; 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)
|
(when (> (length points) 0)
|
||||||
(draw-spline-linear-raw (addr (at points 0)) (length points) thick color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-spline-basis-raw (addr (at points 0)) (length points) thick color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-spline-catmull-rom-raw (addr (at points 0)) (length points) thick color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-spline-bezier-quadratic-raw
|
(draw-spline-bezier-quadratic-raw
|
||||||
(addr (at points 0)) (length points) thick color)))
|
(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)
|
(when (> (length points) 0)
|
||||||
(draw-spline-bezier-cubic-raw
|
(draw-spline-bezier-cubic-raw
|
||||||
(addr (at points 0)) (length points) thick color)))
|
(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
|
;; 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.
|
;; wrong for the only direction it reads in is worse than no binding.
|
||||||
(declare-c get-codepoint-previous-raw
|
(declare-c get-codepoint-previous-raw
|
||||||
[text (Ptr u8) codepoint-size (Ptr i32)] i32
|
[text (Ptr const u8) codepoint-size (Ptr i32)] i32
|
||||||
"GetCodepointPrevious")
|
"GetCodepointPrevious")
|
||||||
|
|
||||||
;; The face a caller wants: the bytes and an offset into them, rather than an
|
;; The face a caller wants: the bytes and an offset into them, rather than an
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user