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 [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
