[bitc-dev] Simplified defrepr

[Swaroop Sridhar]

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.