[bitc-dev] Simplified defrepr
Jonathan S. Shapiro
shap at eros-os.com
Sun Feb 25 10:09:42 CST 2007
Some corrections on Swaroop's note.
First, the keyword was "when", but I actually like "where" better.
Second, Swaroop writes:
>* Identically named fields within the `when' clauses of two different
> constructor forms must be located at the same bit level offset from the
> beginning of both the constructor forms. That is, fpx = fpy implies
> offset(fpx) = offset(fpy).
Two errors here:
1. The offsets must agree to the BIT offset level. That is:
bitoffset(fpx) == bitoffset(fpy).
2. The requirement is not limited to fields mentioned in the when
clause. If the same field name appears in multiple legs of a
DEFREPR, that field must appear at the same bit offset in all legs
where it appears.
Because of this rule:
;; Illegal -- bit offset of 'b' does not match:
(defrepr name
(case1 a:int32 b:int32)
(case2 b:int32))
We may relax this restriction later.
> * Currently, the defrepr form will not accept type arguments over
> which it can be instantiated.
In English: no alpha types. DEFREPR is intended for low-level structure
specification. Such things aren't generally things that you can
parameterize. By imposing this restriction, we can check the DEFREPR for
errors early.
As Swaroop mentions, we *could* defer this check until instantiation
time. Unfortunately, this would cause it to be a *runtime* error in some
implementations, so I don't think that we will do that.
> * Note that the numbering scheme for constructors and fields used
> above ...
I have no idea what this means either.
It was our intention that the RESERVED syntax should also be legal in
normal structures and unions.
On Sat, 2007-02-24 at 19:28 -0500, Swaroop Sridhar wrote:
> The current BitC spec contains a specification for a language construct
> called `defrepr' which can be used to declare (low level hardware)
> data-structures which involve nested union discriminators, and at the
> same time need to conform to an overall bit-level layout (See:
> http://coyotos.org/docs/bitc/spec.html#3.6.3).
>
> On Thursday, we contemplated introducing a simplified form of defrepr
> based on the approach proposed in the ICFP2005 paper by Iavor Diatchi
> et. al.: http://www.cse.ogi.edu/~diatchki/papers/bitdata.pdf.
>
> The new defrepr (hereinafter just called defrepr) has the following form:
>
> (defrepr name
> (Ctr1 f11:type f21:type ... fn1:type
> (where fp1=val11 fq1=val21 ... fm1=valm1))
>
> (Ctr2 f12:type f22:type ... fn2:type
> (where fp2=val12 fq2=val22 ... fm2=valm2))
>
> ... )
>
> The following restrictions apply:
>
> For all constructors Ctrx, Ctry, Ctrz ...:
>
> * All fields fpx, fqx...fmx appearing in the `when' clause of a
> constructor form Ctrx must be described within the body of Ctrx. That
> is, {fpx, fqx...fmx} <= {f1x ... fnx}
>
> * Identically named fields within the `when' clauses of two different
> constructor forms must be located at the same bit level offset from the
> beginning of both the constructor forms. That is, fpx = fpy implies
> offset(fpx) = offset(fpy).
>
> * The fields within the when clauses of all constructor forms must
> uniquely distinguish all constructible values of the union. The compiler
> will not introduce any more tag bits for any defrepr value.
>
> * Note that the numbering scheme for constructors and fields used above
> is just a placeholder for simplicity of definition (that is, it must not
> be understood as enforced by the language). They can be uniquely renamed
> to any legal identifier.
>
> * Currently, the defrepr form will not accept type arguments over which
> it can be instantiated.
>
> That is, there is no:
> (defrepr (name 'a 'b ... ) ... )
>
> This may later be relaxed with an instantiation time check for
> well-formedness.
>
> We can envision a larger language construct DEFUNION, which accepts both
> type arguments and `when' clauses. The defunion and defrepr are just
> specializations of this DEFUNION construct. However, currently the
> language only supports defunion (which does not accept the when clause)
> and defrepr (which does not accept type arguments).
>
> The main limitations of the new defrepr wrt the old defrepr are:
>
> i) Common fields must be repeated in all constructor forms
> ii) There is no facility that allows dealing with constructor forms that
> share common substructure within the same case of a switch statement.
>
> I tried to write the Pentium IA32 Data structure using both the old and
> new schemes below. (I have attempted to code the structure precisely,
> but may have may have one or two bits wrong).
>
> The following code uses one additional construct:
>
> (reserved type value)
>
> which fills required that a particular field in a structure /
> constructor form always have a fixed value.
>
> ** NEW defrepr:
>
> (defrepr GDT
> (DataSeg
> loLimit:(bitfield uint32 16)
> loBase:(bitfield uint32 16)
> midBase:(bitfield uint32 8)
> a:(bitfield uint32 1)
> w:(bitfield uint32 1)
> e:(bitfield uint32 1)
> cd:(bitfield uint32 1) ;; TAG: code/data segment
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> hiLimit:(bitfield uint32 4)
> avl:(bitfield uint32 1)
> l:(bitfield uint32 1)
> sz:(bitfield uint32 1)
> G:(bitfield uint32 1)
> hiBase:(bitfield uint32 8)
> (where us=1 cd=0))
>
> (CodeSeg
> loLimit:(bitfield uint32 16)
> loBase:(bitfield uint32 16)
> midBase:(bitfield uint32 8)
> a:(bitfield uint32 1)
> r:(bitfield uint32 1)
> c:(bitfield uint32 1)
> cd:(bitfield uint32 1) ;; TAG: code/data segment
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> hiLimit:(bitfield uint32 4)
> avl:(bitfield uint32 1)
> l:(bitfield uint32 1)
> sz:(bitfield uint32 1)
> G:(bitfield uint32 1)
> hiBase:(bitfield uint32 8)
> (where us=1 cd=0))
>
> (CallGate
> loOffset:(bitfield uint32 16)
> loSelector:(bitfield uint32 16)
> params:(bitfield uint32 5)
> (reserved (bitfield uint32 3) 0)
> gate:(bitfield uint32 2) ;; TAG: which gate?
> (reserved (bitfield uint32 2) 3)
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> hiOffset:(bitfield uint32 16)
> (where us=0 gate=0))
>
> (taskGate
> (reserved (bitfield uint32 16) 0)
> loSelector:(bitfield uint32 16)
> (reserved (bitfield uint32 8) 0)
> gate:(bitfield uint32 2) ;; TAG: which gate?
> (reserved (bitfield uint32 2) 1)
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> (reserved (bitfield uint32 16) 0)
> (where us=0 gate=1))
>
> (intGate
> loOffset:(bitfield uint32 16)
> loSelector:(bitfield uint32 16)
> (reserved (bitfield uint32 8) 0)
> gate:(bitfield uint32 2) ;; TAG: which gate?
> (reserved (bitfield uint32 1) 1)
> D:(bitfield uint32 1)
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> hiOffset:(bitfield uint32 16)
> (where us=0 gate=2))
>
> (trapGate
> loOffset:(bitfield uint32 16)
> loSelector:(bitfield uint32 16)
> (reserved (bitfield uint32 8) 0)
> gate:(bitfield uint32 2) ;; TAG: which gate?
> (reserved (bitfield uint32 1) 1)
> D:(bitfield uint32 1)
> us:(bitfield uint32 1) ;; TAG: user/system segment
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1)
> hiOffset:(bitfield uint32 16)
> (where us=0 gate=3)))
>
>
> ** OLD defrepr:
>
> (defrepr GDT
> (case (segment
> loLimit:(bitfield uint32 16)
> loBase:(bitfield uint32 16)
> midBase:(bitfield uint32 8))
> (system
> (case ((callG intG)
> loOffset:(bitfield uint32 16)))
> selector:(bitfield uint32 16)
> (case (callG
> params:(bitfield uint32 5)
> (reserved (bitfield uint32 3) 0))
> ((trapG intG taskG)
> (reserved (bitfield uint32 8) 0)))))
>
> ;; Segment Type Handling
> (case (segment
> a:(bitfield uint32 1) ;accessed
> (case (data
> w:(bitfield uint32 1) ;writable
> e:(bitfield uint32 1)) ;expansion direction
> (code
> r:(bitfield uint32 1) ;readable
> c:(bitfield uint32 1))) ;conforming
> (tag data code):(bitfield uint32 1))
> (system
> (tag callG taskG intG trapG):(bitfield uint32 2)
> (case (callG
> (reserved (bitfield uint32 2) 3))
> (taskG
> (reserved (bitfield uint32 2) 1))
> ((intG trapG)
> D:(bitfield uint32 1) ; size of gate
> (reserved (bitfield uint32 1) 1)))))
>
> (tag system segment):(bitfield uint32 1)
>
> dpl:(bitfield uint32 2)
> p:(bitfield uint32 1) ;present
> (case
> (segment
> hiLimit:(bitfield uint32 4)
> avl:(bitfield uint32 1) ;available
> l:(bitfield uint32 1) ;64 bit segment
> sz:(bitfield uint32 1) ;16 or 32 bit
> G:(bitfield uint32 1) ;page/byte granularity
> hiBase:(bitfield uint32 8))
> (system
> (case ((callG intG trapG)
> hiOffset:(bitfield uint32 16))))))
>
> Swaroop.
> _______________________________________________
> bitc-dev mailing list
> bitc-dev at coyotos.org
> http://www.coyotos.org/mailman/listinfo/bitc-dev
--
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100
More information about the bitc-dev
mailing list