Andreas D Ludwig

Dr Arnaud Saint-Jalmes

Dr Cristelle Mériadec

Franck Artzner

Dr Olivier Tasseau

Dr Fabienne Berrée

Loïc Lemiègre
email: loic.lemiegre@ensc-rennes.fr

Boron effect on sugar-based organogelators

Keywords: Organogel, boronate, glycolipid, alkylglucoside, water sensitive

The reaction of several alkylglucosides with phenyl boronic acid permitted an easy access to a series of alkylglucoside phenyl boronate derivatives. This type of compounds has structures similar to the known benzylidene glucoside organogelators except the presence of a boronate function in place of the acetal one. Low to very low concentrations of these amphiphilic molecules produced gelation of several organic solvents. The rheological properties of the corresponding soft materials characterized them as elastic solids. They were further characterized by SEM to obtain more information on their morphologies and by SAXS to determine the type of selfassembly involved within the gels. The sensitivity of the boronate function towards hydrolysis was also investigated. We demonstrated that a small amount of water (5% v/v) was sufficient to disrupt organogels leading to the original alkylglucoside and phenyl boronic acid; an important difference with the stable benzylidene-based organogelators. Such water sensitive boronated organogelators could be suitable substances for the preparation of smart soft material for topic drug delivery.

Introduction

The preparation of gels with low molecular weight gelators is possible thanks to weak intermolecular interactions such as van der Waals interactions, π-π interactions, hydrogen bonding or electrostatic interactions. [1] The corresponding self-assembly turns aqueous or organic solutions into hydrogels or organogels respectively. This important area of research provides soft materials which find various types of applications in oil remediation, [2] nanotube formation, [3] drug delivery [4] or sensitive materials [5] . Typical gelators are based on sugars, lipids, peptides, aromatics, that usually provide the required weak interactions. Sugar-based structures are often suitable for the preparation of hydrogels if the hydrophilicity of the carbohydrate is well balanced with hydrophobic tails. [6] Usually access to sugar-based organogelators requires further functionalization of the sugar moiety with the introduction of aromatic rings, acyl or alkyl chains, most of the time by creation of C-O linkages. [7] However, sugars in general, and glucoside derivatives in particular, are known to react selectively with boronic acids leading to corresponding boronic esters. [8] Several strategies have been developed for the detection of sugars or for the formation of molecular self-assembly, thanks to this easy and efficient reaction. [8a, 9] In regard to the specific case of glucoside derivatives, the boronic acid promotes the esterification of the hydroxyl functions available on the 4,6positions of the glucoside. [10] Boronic esters have already been involved in organogelator structures, [11] but only few examples have taken advantage of this function for the preparation of sugarbased organogelators [12] . One important illustration related to our research work was described by Shimizu et al. [12b-d] who designed a luminescent organogelator based on a glycolipid naphtyl boronic ester. We described herein a series of alkylglucoside phenylboronic esters 1 easily prepared in a single chemical step (Figure 1). Their chemical structures are similar to known benzylidene type organogelators 2 that already demonstrated their ability as good organogelators with typical minimum gelation concentration between 2 to 10 mg.mL -1 . [7e, 7j, 13] The replacement of the acetal function by a boronic ester group induces two main differences; 1) the tetrahedric carbon is replaced by a planar boron atom and 2) the presence of a vacant orbital on boron atom. As a consequence, the geometry of the molecule, and therefore its self-assembling properties, are supposed to dramatically change. Furthermore, the easier hydrolysis of the boronate function compared with the acetal one might conduce to water sensitive self-assembly. However, one could imagine that this slight difference would prevent these less stable boronate derivatives to provide gelation of organic solvents. Within this new family of organogelators, we investigated the impact of the alkyl chain length on the gelation of various solvents. The organogels were characterized at a macroscopic scale by rheology (mechanical properties, stability), at a microscopic scale by scanning electron microscopy (SEM) and molecular level was achieved by small angle X-ray scattering (SAXS) analysis. In addition, their sensitivity against water was confirmed.

Results and Discussion

The synthesis of boronic esters 1 was simply achieved by mixing equimolar amounts of alkylglucosides 4 and phenylboronic acid 3 without solvent. Elimination of water by heating under high vacuum displaced the equilibrium towards the formation of the final product (Scheme 1). Complete reactions were observed for alkylglucosides 4a-h within 15 minutes at 90°C whatever the alkyl tail equipping the glucoside (n-methyl, n-butyl, n-hexyl, n-heptyl, n-octyl, n-nonyl, n-decyl and n-dodecyl chains). All boronic esters 1a-h were isolated without purification or after simple washing with diisopropylether in excellent yields (84-99%) and purities. This series of boronic esters with a broad range of hydrophilic/lipophilic balance, was further engaged in gelation assays with various solvents. The a-butyl derivative a-1b was also prepared in the same manner (not shown) in order to investigate the stereochemical impact of the nature of the glycosidic bond (a or b).

Scheme 1. Synthesis of alkylglucoside boronic esters 1a-h.

To evaluate the potential of this series of new molecules as organogelators, we first selected several solvents covering different solvation behaviors. Toluene represents an example of aromatic solvent, cyclohexane is a typical cycloalkane, ethyl myristate and isopropyl palmitate are interesting bio-based solvents used in cosmetic applications and topical drug delivery. [4a] Table 1 gathers the results for each molecule/solvent combination. For each case, we determined if the molecule was insoluble even after heating (I), soluble after heating (S), behave as an opaque gel (G O ), as a transparent gel (G T ) or as a precipitate upon cooling (P) (Photos of representative gels are available in the SI). The first member of the series (methyl, 1a) was not soluble whatever the solvent used (Table 1, entry 1). This shortest chain length did not provide a sufficient hydrophilic/lipophilic balance to permit the gelation of the solvents considered here. Concerning the stereochemistry of the glycosidic bond, if the a isomer a-1b (entry 2) did not provide organogel either in toluene or in cyclohexane, conversely, the b isomer b-1b (entry 3) was able to gel the four solvents giving translucent organogels with toluene, cyclohexane and fatty esters. Indeed, stereochemistry is an important feature that dramatically changes the geometry of molecules and therefore their ability to self-assemble. [14] For the rest of the study, we only considered b isomers and evaluated the impact of the length of the alkyl chain on the gelation properties (entries 3-9). Indeed, the length of the alkyl chain had a remarkable influence on the gelation properties. n-Butyl derivative b-1b led to organogels with the all four solvents at low to very low concentrations (3 to 11 mg.mL -1 ) (entry 3). The addition of two carbon atoms (n-hexyl 1c, entry 4) provided very similar minimum gelation concentrations (MGC) for the four solvents. Middle chain length (n-heptyl, 1d and n-octyl, 1e; entries 5-6) led to organogels in all solvents except cyclohexane for which precipitation or insolubility were obtained. The n-nonyl derivative 1f did not lead to a full gelation except for ethyl myristate (entry 7). Increasing even more the chain length reduced the solubility in cyclohexane, increased the solubility in toluene but provided transparent organogels in fatty ester solvents at low concentrations (10 mg.mL -1 ) (n-decyl 1g, entry 8). Surprisingly, the n-dodecyl counterpart 1h (entry 9) had a different behavior in cyclohexane providing an organogel at a very low concentration (2 mg.mL -1 ) and in only one of the two fatty esters (isopropyl palmitate). a-D-n-butyl a-1b P I nd [b] nd [b] 3 Mechanical properties were investigated by rheological amplitude-sweep. Graphs of G' and G" against strain % are shown in Figure 2 (data shown for b-n-butyl derivative, graphs of other organogels are available in the SI). Experiments were performed with a frequency of 1 Hz at the MGC described in Table 1. Under such conditions, at low strains, all organogels exhibited storage moduli greater than loss moduli (Table 2). It demonstrates

b-D-n-butyl b-1b G T 11 G T 3 G T 10 G T 11 4 b-D-n-hexyl 1c G O 10 I G O 10 G O 10 5 b-D-n-heptyl 1d G T 9 P G T 9 G O 9 6 b-D-n-octyl 1e G O 12 I G O 8 G O 12 7 b-D-n-nonyl 1f G P 12 G P 4 G O 12 G P 11 8 b-D-n-decyl 1g S I G T 10 G T 10 9 b-D-n-dodecyl 1h S G T 2 S G
O HO OH O Alk 1a (Me), 1b (n-Bu), 1c (n-Hex), 1d (n-Hept), 1e (n-Oct), 1f (n-Non), 1g (n-Dec), 1h (

Accepted Manuscript

that the gels can be considered as elastic solids, but rather soft ones. Indeed, their elastic moduli reach only values from hundreds to a few thousands of Pa, and they remain only a few times larger than the viscous moduli. Interestingly the b-n-butyl derivative b-1b provided the largest G' and G'/G" values after gelation of toluene (Table 2, entry 1). The n-dodecyl derivative 1h induced the formation of stiffer gels in cyclohexane (Table 2,entry 17) and n-heptyl 1d and n-decyl 1g counterparts afforded stiffer gels (larger elastic moduli) in fatty ester solvents (Table 2,entries 9,15,16). These observations might result from different tightness of packing of organogelator fibers within the solvent.

Then interaction of the fibers with the solvent molecules would vary for each organogelator/solvent couple. Indeed, long chain fatty ester solvents are reasonably more compatible with long chain organogels whereas short chain organogelators would express a more aromatic behavior, more compatible with toluene for instance. G'/G" [a] At strain < 1%, 1 Hz frequency.

At high amplitudes of deformation, a same qualitative behavior is found for all the organogels: above a deformation threshold (typically ranging from 1 to 10%), the samples provide a viscous response to the mechanical solicitation, eventually dominating the elastic one (G'' > G'). In the case of b-n-butyl derivative b-1b, above amplitudes of around 2%, some first plastic rearrangements are induced inside the organogels, decreasing the elastic modulus G'. At amplitudes above 2.5 to 8%, the elasticity of the organogel vanished, with G' collapsing down to G". Under such amplitudes, the organogel structure could not effectively sustain the deformation and the sample started to irreversibly flow. Similar conclusions raised from the analysis of the other organogels (see SI). An experiment at 2% amplitude and 1 Hz frequency showed constant moduli over a period of 2 hours (Figure 3A). Thus, the constant rheological properties obtained under such conditions demonstrated the stability of the organogels over time. In addition, consecutive amplitude-sweep experiments on a same gel also showed that the low strain regime was independent of the number of measurements, but that the deformation threshold (where G' becomes smaller than G'') was dramatically modified after the first run (runs from the black line to red lines, Figure 3B) and then continuously by the repetition of tests (from red lines to blue and then green lines, Figure 3B). This implies that the first self-assembled structures obtained through the gelation process were irreversibly modified each time that they were deformed over their deformation threshold (Figure 3B and SI). Reorganization of the fiber network might occur during the deformation of the organogels. Toluene and cyclohexane-based organogels were freeze-dried and the corresponding xerogels were analyzed by scanning electron microscopy (SEM) (Figure 4). The morphology of xerogels originated from toluene revealed characteristic networks of fibers entangled one to another in the case of n-butyl, n-hexyl and n-octyl derivatives (Figures 4A,B,D,E). However, dense structures corresponding to a bundle of fibers were observed in the case of n-heptyl counterpart (Figure 4C). This exception would find its origin in the odd number of carbon atoms within the alkyl chain compared to the even number of carbon atoms for the other organogelators. The SEM images of xerogels obtained from cyclohexane (Figure 4F-H) also revealed fibrillar networks for nbutyl (Figure 4F) and n-nonyl (Figure 4G) derivatives whereas ndodecyl derivative led to a network involving large clusters of fibers (Figure 4H).

10.1002/chem.202001970

Accepted Manuscript

Chemistry -A European Journal The fibrillar networks observed by SEM originate from the selfassembly of the organogelators within the solvent. To better understand the type of self-assembly involved during gelation, we embarked on a small angle X-ray scattering (SAXS) study of some members of the series. Measurements were successfully achieved for organogels obtained in toluene with b-D-octyl 1e (Figure 5) and b-D-hexyl 1c (SI). Figure 5 compares SAXS profiles of the organogel at 20 mg.mL -1 of 1e in toluene (blue) and the corresponding xerogel (red). Both organogel and xerogel have the same scattering profiles. Indexations revealed the existence of a hexagonal phase exhibiting a 3D crystal packing (Table 3). This hexagonal phase was assigned without any ambiguity and consequently, tracing qhkl in a hexagonal lattice, where h, k, and l refer to Miller indices, gave access to repeating parameters of a = 26.8 Å and c = 5.47 Å. The unit cell volume is 3390 Å 3 and molecular weight of 1e is 378 g.mol -1 . With a density of 1.11, the number of molecules per unit cell is 6. The molecules may be localized on any position of the hexagonal lattice. It is simpler to imagine three sets of dimers centered on the C2 axes (Figure 6A-B). This dimer must exhibit smaller areas at both ends to fit in the center of the hexagonal phase and a larger area at its center to accommodate the space available (Figure 6B). This type of organization can be compared to self-assemblies involved in cylindrical micelles. [START_REF] Israelachvili | Intermolecular and Surface Forces[END_REF] Table 3. Theoretical and observed indexations of the hexagonal phase shown in Figure 5 This in mind, a compatible dimer structure involves: 1) disorganized alkyl chains at both ends which fit into the center of 10.1002/chem.202001970

Accepted Manuscript

the hexagonal phase and 2) interdigitated aromatic rings at the center of the dimer. Several types of packing can be envisaged based on the interaction between aromatic rings: face to face or edge to face including T-shaped geometry or herringbone packing.

The later fits the best with the repeating parameter c (5.47 Å) (Figure 6C). Indeed, edge-to-face stacking (T-shaped geometry) would have led to a wrong orientation of the two members of the dimer and face-to-face stacking would have required a larger repeating parameter (≈ 7 Å). It is also noteworthy that the herringbone packing was previously observed within the crystal packing of a similar boronate derivative (methyl-2-deoxy-a-Dglucopyranoside 4,6-phenylboronate). [START_REF] Heß | [END_REF] Thus, Figure 6C (extended chains are shown for clarity) represents the possible structure of the dimer, its vertical packing and interdigitation of aromatic rings in respect of parameter c (5.47 Å). Figure 6d represents the possible packing of three dimers within the hexagonal phase, the alkyl chain being disorganized in the center of each hexagon in respect of parameters a (26.8 Å). A very similar self-assembly was characterized for the organogel obtained with b-D-hexyl 1c. However, the scattering profile exhibited a liquid crystal state instead of the 3D crystal packing. This hexagonal phase was also assigned without any ambiguity (see SI). A comparable parameter (a = 28.7 Å) found its origin from a similar packing model (Figure 6D), the less crystallinity of the liquid crystal state would explain the slight difference between the parameters a of 1e and 1c in favor of 1c. The sp2 hybridization of a boron atom of a boronate function induces a planar geometry, whereas the sp3 hybridization of the carbon atom of an acetal function confers a tetrahedral geometry. It triggers a dramatic difference between the two organogelators 1 and 2 (Figure 7). Indeed, the particular geometry of the boronate function offers a different orientation of the aromatic ring in regard to the sugar moiety. Therefore, this orientation impacts the global shape of the molecule and is then responsible for the type of packing observed here and characterized by SAXS. As mentioned in the introduction, boronate functions are usually sensitive to aqueous media whereas benzylidene functions are stable in the presence of water, at least at neutral pH. Thus, we evaluated the behavior of the organogels obtained with the n-butyl derivative 1b selected as an example of the series. The organogels in toluene, ethyl myristate and isopropyl palmitate were exposed to water (5% v/v) at room temperature during the time of the experiment. Until 1h, the gels were partially disrupted with most of the material being in a gel state, between 1h and 3h, the gels loosed their structures towards a fluid state with some pieces of gel still present and after 3h, the gel state of all samples totally disappeared leading to biphasic or monophasic solutions depending on the solvent used for the formation of the gels (Figure 8). We also repeated the same experiments (gel from bbutyl b-1b in toluene) except that we replaced fresh distilled water by acetate buffer (pH = 4.8) or carbonate buffer (pH = 9.8). Very similar results were obtained after addition of 5% v/v of these two buffer solution. The 1 H NMR analysis of the water phase confirmed the hydrolysis of the organogelator into its two original components; phenylboronic acid and n-butyl-b-D-glucoside (Figure 9). It confirmed the water sensitivity of the boronate function which is then responsible for the disruption of the organogel.

Conclusion

A series of glycolipid phenylboronic esters was easily prepared in one step from alkylglucosides and phenylboronic acid. These new amphiphilic structures revealed good gelation abilities for the four typical organic solvents evaluated in this study (toluene, cyclohexane, fatty esters). Rheological properties and morphologies of the organogels were determined for each gel obtained with all possible solvent/organogelator combinations. It showed that the alkyl chain length on the glucoside played an important role on the gelation ability of the different solvents. The organogelators self-assembled within the solvent to form fibers observed by SEM. These fibers were the result of the packing of organogelators in a hexagonal lattice where they behave as dimers. In addition to the preparation and characterization of these organogels, we demonstrated that the addition of a small amount of water (5% v/v) was enough to disrupt the organogels in few hours (less than 3h). The mechanism of disruption is clearly related to the hydrolysis of the boronate function. Therefore, the introduction of a boron atom within the structure of these organogelators deeply impacts and enriches the properties of the so formed organogels. For instance, these soft materials represent useful systems for topical drug delivery with controlled release upon contact with aqueous media. Such applications and tuning of the water sensitivity are now under investigation in our laboratories.

Experimental Section

General Information. 1 H NMR spectra (300 MHz, 400 MHz), 13 C NMR (75 MHz, 101 MHz) and 11 B (96 MHz) were recorded on Bruker AC 300 and AC 400 spectrometers. Chemical shifts are given in ppm and coupling constants J in Hz. Multiplicities are presented as follows: s = singlet, d = doublet, t = triplet, q = quartet, quint = quintuplet, hex = hexuplet, m = multiplet, br = broad. The carbon bearing the boron atom was not observed due to the quadrupolar relaxation mechanism of 11 B nucleus. Highresolution mass spectra (HRMS) were recorded, either on a Bruker MaXis 4G, an Agilent 6510, or a Thermo Fisher Q-Exactive spectrometer (Centre Régional de Mesures Physiques de l'Ouest, Rennes) using positive ion Electron-Spray ionization techniques. Melting points were measured on a melting point apparatus Stuart SMP10 and are uncorrected. Specific rotation (in deg cm 3 g -1 ) was measured on a Perkin Elmer-341 polarimeter.

General procedure for the synthesis of boronic esters 1. In a 25 mL round bottom flask, alkylglucoside (0.3 mmol) and phenylboronic acid (37 mg, 0.3 mmol) were added. The mixture was then stirred in a kugelrohr distillation apparatus at 90°C; under 0.1 mm Hg for 15 minutes to give the product pure enough to make gels. Compounds were washed by diisopropylether when necessary.

Methyl-b-D-glucopyranoside 4,6-phenylboronate 1a. [17] 143 mg (99%); white solid; mp = 188-190°C.

Accepted Manuscript

Gel formation. The gels were prepared by mixing the appropriate amount of gelator into the appropriate organic solvent at various percentages in capped tubes. The tubes were heated at 60°C (cyclohexane), 80°C (toluene) or 120°C (fatty esters) for 1 h or until clear solutions were obtained. Clear solutions were then cooled down to room temperature to allow the formation of a gel.

Rheology. Organogel samples were presented under disc form (4 cm diameter). Rheological measurements were performed on an Anton-Paar MCR301 equipped with an upper plate of 75 mm diameter. The frequency (ω) was fixed to 1 Hz and the amplitude deformation (γ°) was gradually increased from 0 to 50% of shearing. Storage modulus G' and the loss modulus G" were obtained at 25°C.

Scanning Electron Microscopy (SEM).

Metalisation by Au/Pd. Scanning Electron Microscopy (SEM) of xerogels were evaluated using the JEOL IT 300 Scanning Electron Microscope. Samples were collected and deposited on a Teflon plot. Each sample was examined using a voltage of 5 or 10 kV. Images were analyzed by SMileView software.

Small Angle X-Ray Scattering (SAXS). Organogel and xerogel samples were prepared into capillaries. SAXS experiments were performed using X-ray patterns collected with a Pilatus 300k (Dectris, Grenoble, France), mounted on a microsource X-ray generator GeniX 3D (Xenocs, Sassenage, France) operating at 30 watts. The monochromatics CuKα radiation is of λ = 1.541 Å. The diffraction patterns were therefore recorded for reciprocal spacing q = 4π*sinθ/λ in a range of repetitive distances from 0.015 Å -1 (418 Å) and 1.77 Å -1 (8 Å). Images were transformed to graphics using the software program Fit2D (ESRF).

Molecular model. Cartoon representation of the self-assembly of the organogelators were obtained from the assembly of one molecule previously minimized. These preliminary minimizations were carried out in vacuum, in periodic boundaries and standard conditions taking into account Coulomb and Van der Waals interactions; with semi-empirical and restricted Hartree-Fock method, AM1 [18] coupled with an AMBER [19] force field; version for Yasara software [20] (YAMBER03). Assembly of several molecule and final representation were obtained using Samson software [21] .

Entry for the Table of Contents

Synthesis of alkyglucoside phenyl boronic esters provided a series of organogels in several solvents. Similar to benzylidene type organogelators, the replacement of the acetal group by a boronate function induced singular self-assembling properties and high sensitivity to water.

Accepted Manuscript

Chemistry -A European Journal

Figure 1 .

 1 Figure 1. Alkylglucoside phenyl boronic esters 1 and known benzylidene glucoside organogelators 2.

  T 12 [a] I: Insoluble; S: Soluble; P: Precipitate; G P : Partial gel; G T : Translucent gel; G O : Opaque gel. Values indicate minimum gelation concentrations (MGC) in mg.mL -1 . [b] Not determined.

Figure 2 .

 2 Figure 2. Storage modulus (G', plain line) and loss modulus (G", dashed line) against strain % of organogels obtained with b-n-butyl b-1b in toluene (A), cyclohexane (B), ethyl myristate (C) and in isopropyl palmitate (D).

Figure 3 .

 3 Figure 3. (A) Storage modulus (G', plain line) and loss modulus (G", dashed line) against time (Frequency = 1 Hz and Amplitude = 2%); (B) Ten successive amplitude-sweep experiments (First experiment in black line then red, blue, and green lines). Data for gel of b-n-butyl b-1b in isopropyl palmitate (IP).

Figure 4 .

 4 Figure 4. SEM images of xerogels (A: n-butyl/toluene; B: n-hexyl/toluene; C: nheptyl/toluene; D: n-octyl/toluene; E: n-octyl/toluene; F: n-butyl/cyclohexane; G: n-nonyl/cyclohexane; H: n-dodecyl/cyclohexane). Scale bar : 10 µm.

Figure 5 .

 5 Figure 5. SAXS profiles of organogel in blue (toluene) and xerogel in red obtained with b-D-octyl 1e.

Figure 6 .

 6 Figure 6. Representation of the hexagonal packing characterized by SAXS for 1e. A: distribution of 5 dimers (6 molecules) within the unit cell; B: self-assembly of dimers within the hexagonal phase and global shape of the dimer; C: selfassembly of 4 molecules and herringbone packing; D: self-assembly of 10 molecules within the unit cell.

Figure 7 .

 7 Figure 7. Representation of the impact of boronate and acetal geometries on the orientation of the aromatic rings (Minimization obtained at an AM1 level).

Figure 8 .

 8 Figure 8. Water sensitivity of organogels: disruption of a gel by addition of water (5% v/v) via hydrolysis of the boronate function (Images shown for isopropyl palmitate case).

Figure 9 .

 9 Figure 9. 1 H NMR spectra in D2O of phenylboronic acid (bottom), n-butyl-b-Dglucoside (middle) and water phase after disruption of the organogel (b-1b in toluene) with 5% v/v of water (top).

  [a]D= -21 (C 0.2, CH2Cl2). 1 H NMR (300 MHz, CDCl3) δ 7.81 (d, J = 7.2 Hz, 2H), 7.46 (t, J = 7.4 Hz, 1H), 7.36 (t, J = 7.4 Hz, 2H), 4.38 (d, J = 7.7 Hz, 1H, H1), 4.32 (dd, J = 10.4, 5.4 Hz, 1H, H6), 4.01 (t, J = 10.3 Hz, 1H, H6), 3.85-3.70 (m, 2H, H3 H4), 3.60 (s, 3H), 3.58-3.49 (m, 2H, H2 H5), 2.80 (d, J = 1.8 Hz, 1H, OH), 2.55 (d, J = 2.3 Hz, 1H, OH). 13 C NMR (75 MHz, CDCl3) δ 134.3, 131.4, 127.8, 104.4 (C1), 75.1 (C4), 74.7 (C2), 74.3 (C3), 68.7 (C5), 64.2 (C6), 57.7 (OCH3). The carbon α to the boron was not observed. 11 B NMR (96 MHz, CDCl3) δ 28.7. HRMS (ESI+) (M+Na) + calculated for C13H17O6 11 BNa 303.10159, found 303.1011. Butyl-b-D-glucopyranoside 4,6-phenylboronate b-1b. 134 mg (98%); white solid; mp = 153-155°C; [a]D= -87 (C 1, CH2Cl2). 1 H NMR (300 MHz, CDCl3) δ 7.80 (d, J = 7.1 Hz, 2H), 7.44 (t, J = 7.4 Hz, 1H), 7.35 (t, J = 7.5 Hz, 2H), 4.43 (d, J = 7.7 Hz, 1H, H1), 4.30 (dd, J = 10.4, 5.4 Hz, 1H, H6), 4.00 (t, J = 10.4 Hz, 1H, H6), 3.92 (dt, J = 9.5, 6.8 Hz, 1H, OCH2), 3.83-3.70 (m, 2H, H3 H4), 3.63-3.50 (m, 3H, OCH2 H5 H2), 2.95 (s, 1H, OH), 2.67 (d, J = 2.4 Hz, 1H, OH), 1.63 (quint, J = 6.8 Hz, 2H), 1.41 (hex, J = 7.3 Hz, 2H), 0.94 (t, J = 7.3 Hz, 3H). 13 C NMR (75 MHz, CDCl3) δ 134.1, 131.2, 127.6, 103.2 (C1), 74.9 (C3), 74.5 (C4), 74.1 (C2), 70.3 (OCH2), 68.6 (C5), 64.1 (C6), 31.6, 19.1, 13.8. The carbon α to the boron was not observed. 11 B NMR (96 MHz, CDCl3) δ 26.8. HRMS (ESI+) (M+Na) + calculated for C16H23O6 11 BNa 345.1485, found 345.1481. Butyl-a-D-glucopyranoside 4,6-phenylboronate a-1b. 115 mg (84%); white solid; mp = 100-102°C. [a]D= +95 (C 1, CH2Cl2

Table 1 .

 1 Gelation assays[a]

	Entry	Compound	Toluene	CyH	Ethyl	Isopropyl
					Myristate	Palmitate
	1	b-D-methyl 1a	I	I	I	I
	2

Table 2 .

 2 Storage and loss modulus at low strain of organogels.

	Entry	Compound	Solvent	Storage
				modulus
				[Pa]

[a]

Loss modulus [Pa]

[a]

Acknowledgements

We acknowledge the Ministère de l'Education Nationale, de la Recherche et de la Technologie. The authors thank F. Gouttefangeas and L. Joanny from the CMEBA (Centre de Microscopie Electronique à Balayage et microAnalyse, Rennes) for assistance in recording SEM images.


Yves Bertot
email: yves.bertot@sophia.inria.fr

Benjamin Grégoire
email: benjamin.gregoire@sophia.inria.fr

Xavier Leroy
email: xavier.leroy@inria.fr

A structured approach to proving compiler optimizations based on dataflow analysis

This paper reports on the correctness proof of compiler optimizations based on data-flow analysis. We formulate the optimizations and analyses as instances of a general framework for data-flow analyses and transformations, and prove that the optimizations preserve the behavior of the compiled programs. This development is a part of a larger effort of certifying an optimizing compiler by proving semantic equivalence between source and compiled code.

Introduction

Can you trust your compiler? It is generally taken for granted that compilers do not introduce bugs in the programs they transform from source code to executable code: users expect that the generated executable code behaves as prescribed by the semantics of the source code. However, compilers are complex programs that perform delicate transformations over complicated data structures; this is doubly true for optimizing compilers that exploit results of static analyses to eliminate inefficiencies in the code. Thus, bugs in compilers can (and do) happen, causing wrong executable programs to be generated from correct source programs.

For low-assurance software that is validated only by testing, compiler bugs are not a major problem: what is tested is the executable code generated by the compiler, therefore compiler bugs should be detected along with program bugs if the testing is sufficiently exhaustive. This is no longer true for critical, high-assurance software that must be validated using formal methods (program proof, model checking, etc): here, what is certified using formal methods is the source code, and compiler bugs can invalidate the guarantees obtained by this certification. The critical software industry is aware of this issue and uses a variety of techniques to alleviate it, such as compiling with optimizations turned off and conducting manual code reviews of the generated assembly code. These techniques do not fully address the issue, and are costly in terms of development time and program performance.

It is therefore high time to apply formal methods to the compiler itself in order to gain assurance that it preserves the behaviour of the source programs.

Many different approaches have been proposed and investigated, including proofcarrying code [START_REF] Necula | Proof-carrying code[END_REF], translation validation [START_REF] Pnueli | Translation validation. In Tools and Algorithms for Construction and Analysis of Systems[END_REF], credible compilation [START_REF] Rinard | Credible compilation[END_REF], and typepreserving compilers [START_REF] Morrisett | From system F to typed assembly language[END_REF]. In the ConCert project (Compiler Certification), we investigate the feasibility of performing program proof over the compiler itself: using the Coq proof assistant, we write a moderately-optimizing compiler from a C-like imperative language to PowerPC assembly code and we try to prove a semantic preservation theorem of the form For all correct source programs S, if the compiler terminates without errors and produces executable code C, then C has the same behaviour (up to observational equivalence) as S.

An original aspect of ConCert is that most of the compiler is written directly in the Coq specification language, in a purely functional style. The executable compiler is obtained by automatic extraction of Caml code from this specification.

In this paper, we report on the correctness proof of one part of the compiler: optimizations based on dataflow analyses performed over an intermediate code representation called RTL (Register Transfer Language). Section 2 gives an overview of the structure of the compiler. Section 3 defines the RTL language and its semantics. Section 4 develops a generic framework for dataflow analyses and transformations. Section 5 instantiates this framework for two particular optimizations: constant propagation and common subexpression elimination. We discuss related work in section 6 and conclude in section 7.

The work outlined in this paper integrates in a more ambitious project that is still in progress and is therefore subject to further modifications. A snapshot of this work can be found on the project site1 .

General scheme of the compiler

Cminor / / RTL / / CP CSE R R LTL / / Linear / / PowerPc Fig. 1.

Scheme of the compiler

The compiler that we consider is, classically, composed of a sequence of code transformations. Some transformations are non-optimizing translations from one language to another, lower-level language. Others are optimizations that rewrite the code to eliminate inefficiencies, while staying within the same intermediate language. Following common practice, the transformations are logically grouped into three phases:

1. The front-end : non-optimizing translations from the source language to the RTL intermediate language (three-address code operating on pseudo-registers and with control represented by a control-flow graph). 2. The optimizer : dataflow analyses and optimizations performed on the RTL form. 3. The back-end : translations from RTL to PowerPC assembly code.

In the following sections, we concentrate on phase 2: RTL and optimizations. To provide more context, we give now a quick overview of the front-end and back-end (phases 1 and 3).

The source language of the front-end is Cminor: a simple, C-like imperative language featuring expressions, statements and procedures. Control is expressed using structured constructs (conditionals, loops, blocks). We do not expect programmers to write Cminor code directly; rather, Cminor is an appropriate target language for translating higher-level languages such as the goto-less fragment of C. The translation from Cminor to RTL consists in decomposing expressions into machine-level instructions, assigning (temporary) pseudo-registers to Cminor local variables and intermediate results of expressions, and building the controlflow graph corresponding to Cminor structured control constructs.

The back-end transformations start with register allocation, which maps pseudo-registers (an infinity of which is available in RTL code) to actual hardware registers (in finite number) and slots in the stack-allocated activation record of the function. We use Appel and George's register allocator based on coloring of an interference graph. The result of this pass is LTL (Location Transfer Language) code, similar in structure to RTL but using hardware registers and stack slots instead of pseudo-registers. Next, we linearize the control-flow graph, introducing explicit goto instructions where necessary (Linear code). Finally, PowerPC assembly code is emitted from the Linear code.

RTL and its semantics

Syntax

The structure of the RTL language is outlined in figure 2. A full program is composed of a set of function definitions P F represented by a vector of pairs binding a function name and a function declaration, one of these function names should be declared as the main function P main . It also contains a set of global variable declarations represented by a vector of pairs binding global variable names and their corresponding memory size.

Each function declaration indicates various parameters for this function, like the arguments (args), or the size of the stack memory that is required for local usage (space). Important ingredients are the function code (C) and the entry point (ep). The record also contains "certificates": the field (in) contains a proof that the entry point is in the code, while the field (WC) contains a proof that the code is a well-connected graph.

global variable The code itself is given as a partial function from a type s of program locations to a type I of instructions. To encode this partial function, we view it as the pair of a total function and a domain predicate. Each instruction combines an instruction description and a vector of potential successors.

x program point c | s comparison cmp ::= = | = | < | ≤ | > | ≥ condition cnd ::= Ccomp cmp | Ccompu cmp | Ccomp imm cmp i | Ccompu imm cmp i | Ccompf cmp | Cnotcompf cmp | Ccompptr cmp | Cmaskzero i | Cmasknotzero i operation op ::= Omove | Oconstint i | Oconstfloat f | Oaddrglobal x | Oaddrstack i | arithmetic operations | pointer arithmetic | specific operations | Ocomp cnd memory chunk mc ::= int8 | uint8 | int16 | uint16 | int32 | float32 | float64 | addr addressing mode am ::= Aindexed | Aindexed imm i | Abased x i | Abased imm x i | Ainstack i
Instruction descriptions really specify what each instruction does: memory access, call to other functions, conditional and switch, or return instructions. A "no-operation" instruction is also provided: this instruction is useful to replace discarded instructions without changing the graph shape during optimizations.

Instruction descriptions do not contain the successor of instructions, this information is given at the upper level I by the list of successors. This organization makes it easier to describe some analyses on the code in an abstract way. For most instruction descriptions, exactly one successor is required, except for the Ireturn instruction, which takes no successor, the Icond instruction, which takes two successors and for the Iswitch instruction which takes one successor for each defined label (ı) and one for the default branch.

The syntactic categories of comparison (cmp), condition (cnd) and operation (op) are used to give a precise meaning to the various instructions. Note that the language makes a distinction between several kinds of numbers: integers, unsigned integers, floating point numbers, and pointers. This distinction appears in the existence of several kinds of comparison and arithmetic operations. Operations of each kind are distinguished by the suffix u, f, or ptr, or no suffix for plain integers. The arithmetic on pointers makes it possible to compare two pointers, to subtract them (this return a integer), and to add an integer to a pointer. The way pointers are handled in the language is also related to the way memory is handled in the store and load instructions.

Memory access instructions (Iload and Istore) take a memory chunk (mc) parameter that indicates the type of data that is read or written in memory. It also indicates how data is to be completed: when reading an 8-bit integer into a 32-bit register, it is necessary to choose the value of the remaining 24 bits. If the integer is considered unsigned, then the extra bits are all zeros, but if the data is signed, then the most significant bit actually is a sign bit and one may use complement to 2 representation. This way of handling numbers is common to most processors with 32-bit integer registers and 64-bit floating point registers.

A second parameter to load and store operations is the addressing mode. This addressing mode always takes two arguments: an address and an offset. The addressing modes given here are especially meaningful for the Power-PC micro-processor.

The language contains two instructions for function calls, Icall imm represents the usual function call where the function name is known at compile-time, whereas Icall represents a function call where the function is given as a location in a register2 . This capability is especially useful if we want to use Cminor or RTL as an intermediate language for the compilation of functional programming languages, where the possibility to manipulate and call function pointers is instrumental.

Values and memory model

To describe the way memory is handled in our language, we use a model that abstracts away from some of the true details of implementation. This abstraction has two advantages. First, it preserves some freedom of choice in the design of the compiler (especially with respect to stack operations); second it makes the correctness proofs easier. This abstraction also has drawbacks. The main drawback is that some programs that could be compiled without compiling errors and run without run-time error have no meaning according to our semantics.

The first point of view that one may have on memory access is that the memory may be viewed as a gigantic array of cells that all have the same size. Accessing a memory location relies on knowing this location's address, which can be manipulated just as any other integer. The stack also appears in the memory, and the address of objects on the stack can also be observed by some programs. If this memory model was used, then this would leave no freedom to the compiler designer: the semantics would prescribe detailed information such as the amount of memory that is allocated on the stack for a function call, because this information can be inferred by a cleverly written C program.

In practice, this point of view is too detailed, and the actual value of addresses may change from one run of the same program to another, for instance because the operating system interferes with the way memory is used by each program. The compiler should also be given some freedom in the way compiled programs are to use the stack, for instance in choosing which data is stored in the microprocessor's registers and which data is stored in the stack.

The abstract memory model that we have designed relies on the following feature: memory is always allocated as "blocks" and every address actually is the pair of a block address and an offset within this block. The fact that we use an offset makes it possible to have limited notions of pointer arithmetic: two addresses within the same block can be compared, their distance can be computed (as an integer), and so on. On the other hand, it makes no sense to compare two addresses coming from two different blocks, this leaves some freedom to the compiler to choose how much memory is used on the stack between two allocated chunks of memory. For extensions of the language, this also makes it possible to have memory management systems that store data around the blocks they allocate.

From the semantic point of view, this approach is enforced by the following features. First, our RTL language has a specific type of memory address for which direct conversion to integer is not possible, but we can add an integer to an address (we enforce the same restriction in our formal semantics of Cminor). Second, any memory access operation that refers to a block of a given size with an offset that is larger than this size has no semantics.

All the syntactic structures used for values and memory are described in Figure 3.

Our memory model relies on block allocation. Some of the blocks are longlived and stored in the main memory. Other blocks are short lived and correspond to local memory used in C functions (the memory allocated on a stack at each function call is often referred to as a frame). These blocks are "allocated" when the function is called and "deallocated" when the function returns the control to its caller. It is relevant to make sure that different blocks used for different call instances of functions are really understood as different blocks. To achieve this level of abstraction, we consider that there is an infinity of blocks with different status. Memory is then considered as a mapping from an infinite abstract type of head pointers to a collections of block.

Memory modifications correspond to changing the values associated to these head pointers. In the beginning, most head pointers are mapped to a NotYetAllocated block. When a function is called and a block of memory is allocated for this function, a head pointer is updated and becomes mapped to a vector of elementary memory cells (corresponding to bytes). When the block is released, the head pointer is updated again and becomes mapped to a Freed block. Our semantics description of the language gives no meaning to load and store operation in NotYetAllocated and Freed blocks. In this way, we are able to account for the limited life-span of some memory blocks.

To ensure the clean separation between memory addresses and integer values, we only specify that a memory address requires four bytes for storage 3 . We allow writing bytes into a location where an address was previously stored, but this has the side effect of storing an "unknown" value in all the other bytes of the address. We use the symbol ⊥ to denote these unknown values.

Blocks may also contain some code. This feature makes it possible to pass function pointers around and to implement function calls where the function is given by pointer. The level of abstraction is simple to state here: there is no way to know what size a piece of code is taking and only the head pointer of a block containing code may be used in a function call. Of course, reading an integer or an address from a block that contains code simply returns the unknown value ⊥. The semantics of individual instructions is described as an inductive relation using a judgment of the form (S, I) -→ (S ′ , s), where S is the input state, I is the instruction to execute, S ′ is the result state, and s is the location of the next instruction. In Figure 4, we include a few of the inference rules for this judgment. Each rule contains a few consistency checks: for instance, instructions expecting a single successor should not receive several potential successors, the registers providing the input for an arithmetic operation should contain values of the right type, and the register for the output value should also have the right type.

= p → B load load : m → mc → a → v load F : m → a → F store store : m → mc → a → v → m ⊥ storeF : m → mc → a → v → m ⊥
S id (x) = a load F (S mem , a) = f InitFun(f, S, r) = S 1 (S 1 , f ep ) f -→ (S 2 , v) Return(S, S 2 ) = S 3 CheckType(r d , v) (S, (Icall imm x r r d , [s])) -→ (S3[r d := v], s) of several instructions fC (c1) = I (S1, I) -→ (S2, c2) (S2, c2) f -→ (S3, v) (S1, c1) f -→ (S3, v) fC (c) = (Ireturn r, ∅) (S, c) f -→ (S, S.(r))

Evaluation of a program

InitProg(p) = S pF (pmain) = f InitFun(f, S, ∅) = S1 (S1, fep) f -→ (S2, v) Return(S, S2) = S3 p P -→ (S3, v)
To describe the execution of several instructions, we use a judgment of the form (S, c) f -→ (S ′ , v), where f is a function, c is the location of an instruction in the code graph of f , S ′ is the result state when the function execution terminates and v is the return value. So while the judgment (S, I) -→ (S ′ , s) is given in a style close to small step operational semantics, the judgment (S, c) f -→ (S ′ , v) describes a complete execution as we are accustomed to see in big step operational semantics or natural semantics. The two styles actually intertwine in the rule that describes the execution of the Icall imm instruction: to describe the behavior of the single Icall imm instruction, this rule requires that the code of the callee is executed completely to its end.

The rule for the Icall imm instruction first states that the function code must be fetched from memory, then that some initialization must be performed on the state. This initialization consists of allocating a new memory block for the data that is local to the function and moving the S stk field. Then, verifications must be performed: the registers that are supposed to contain the inputs to the called function must contain data of the right type. The registers that are used internally to receive the input arguments must be initialized. Then the function code is simply executed from its entry point, until it reaches a Ireturn statement, which marks the end of the function execution. An auxiliary function, called Return then modifies the state again, restoring the S stk field to its initial value and freeing the memory block that had been allocated.

Evaluating a program is straightforward. Some initialization is required for the global variables and the main function of the program is executed to its end.

When proving the correctness of optimizations, we intuitively want to prove that an optimized function performs the same computations as the initial function. A naive approach would be to express that the resulting state after executing the optimized function is the same as the resulting state after executing the initial function. However, this approach is too naive, because optimization forces the state to be different: since the function code is part of the program's memory, the optimized program necessarily executes from an initial state that is different and terminates in a state that is different. Our correctness statement must therefore abstract away from the details concerning the code stored in the memory.

A generic proof for the optimizations

In the sequel, we consider two optimization phases from RTL to RTL, the first one is constant propagation (CP) and the second is common subexpression elimination (CSE). Both are done procedure by procedure and follow the same scheme.

The first step is a data-flow analysis of the procedures. The result of this analysis is a map that associates to each program point the information that is "valid" before its execution. By "valid information" we mean that any execution would reach this program point in a state that is compatible with the value predicted by the analysis.

The second step is the transformation of the code. This transformation is done instruction by instruction and only requires the result of the analysis for one instruction to know how to transform it. Naturally, the power of the transformation depends directly on the analysis.

We wrote a generic program and its proof to automatically build the analyses, the transformations, and their proofs.

Analysis specification

A data-flow analysis is given by a set D (the domain of the analysis) representing abstractions of states and an analysis function A F that takes as input a function declaration and returns a map from program points to D. These two parameters represent the computation part of the analysis. For CP and CSE the domain is a mapping from registers to abstract values, e.g. a concrete value or "unknown" for CP, or a symbolic expression for CSE.

An analysis is correct when it satisfies some extra properties. In particular, we need an analysis property A P that describes when a concrete state in S is compatible with an abstract state in D. The result of the analysis should have the property that every reachable instruction can only be reached in a state that is compatible with the abstract state that is predicted by the analysis.

The first part of the correctness statement expresses that every state should be compatible with the abstract point that is computed for the entry point; this statement is called A entry .

The second part of the correctness statement expresses that every computation state should map a state compatible with the abstract state for an instruction to states that are compatible with the abstract states of all the successor; this statement is called A correct .

All the components of a valid analysis are gathered in a module type for Coq's module system.

Module Type ANALYSIS.

Parameter D : Set. Parameter A F : F → Map.T D.

Parameter A P : D → S → Prop. Parameter A entry : ∀f S, A P (A F (f ep ), S). Parameter A correct : ∀f c 1 c 2 S 1 S 2 , c 1 ∈ f C ⇒ (S 1 , f C (c 1 )) -→ (S 2 , c 2 ) ⇒ A P (A F (c 1 ), S 1 ) ⇒ A P (A F (c 2 ), S 2 ). End.
Correct analyses can be obtained in a variety of ways, but we rely on a generic implementation of Kildall's algorithm [START_REF] Kildall | A unified approach to global program optimization[END_REF]: the standard solver for data-flow equations using a work list. To compute an analysis, Kildall's algorithm observes each instruction separately. Given a program point c, it computes the value of the analysis for the instruction c using a function A i . Then it update the abstract state of every successor of c with an upper bound of itself and the value of A i at c. The function A i is the analysis of an instruction, it takes what is known before the instruction as argument and returns what is known after it. The termination of this algorithm is ensured because the code graph for a function is always finite and the domain of the analysis is a well-founded semilattice : a set D with a strict partial order > D , a decidable equality, a function that returns an upper bound of every pair of elements, and the extra property that the strict partial order is well-founded.

We don't give more details about Kildall's algorithm, for lack of place, but in our formal development, it is defined using Coq's module system as a functor (a parameterized module) taking as arguments the well-founded semi-lattice, the analysis function, and a few correctness properties. This functor is in turn used to define a generic functor that automatically builds new analyses. This functor takes as argument modules that satisfy the following signature:

Module Type ANALYSIS ENTRIES.

Declare Module D : SEMILATTICE.

Parameter A i : F → c → D.T → D.T . Parameter A P : D.T → S → Prop.
Parameter top P : ∀S, A P (D.top, S).

Parameter A correct : ∀f c, c ∈ f C ⇒ ∀c ′ S S ′ , (S, f C (c)) -→ (S ′ , c ′ ) ⇒ ∀d, A P (d, S) ⇒ A P (A i (d, c), S ′ ). Parameter A ≥D : ∀d 1 d 2 , d 2 ≥ D d 1 ⇒ ∀S, A P (d 1 , S) ⇒ A P (d 2 , S). End.
Module Make Analysis (AE : ANALYSIS ENTRIES) <: ANALYSIS.

First, the semi-lattice's top element should be compatible with any state (top P ). At the entry point we make the assumption that nothing is known, hence the initial abstract state of the analysis is top. This property ensures that any initial state will satisfy the analysis property at the entry point. Second, the parameter A correct ensures that each time the Kildall algorithm analyzes an instruction the result will be compatible with the states occurring in the concrete execution. Then, the last property A ≥D expresses that the order relation on abstract states should be compatible with the subset ordering on S. This ensures that each time Kildall's algorithm computes a new upper bound, the result remains compatible.

Program transformations

The second part of an optimization is a transformation function that uses the results of the analysis to change the code, instruction per instruction. Here again, there is a generic structure for CP and CSE. First, a transformation is given by two functions T F and T P to transform function declarations and whole programs, respectively. The correctness of this transformation is expressed by saying that executing a program to completion should return the same result and equivalent states, whether one executes the original program or the optimized one (T correct ). Two states are equivalent when all locations in the memory have the same value, except that unoptimized code is replaced with optimized code, using a generic replacement map called T state .

Module Type TRANSFER.

Parameter T F : F → F . Parameter T P : P → P .

Parameter

T correct : ∀p S v, p P -→ (S, v) ⇒ T P (p) P -→ (T state (T F , S), v). End.
Here again, correct transformations can be obtained in a variety of ways, but we rely on a generic implementation that takes a correct instruction-wise transformation as a parameter.

We actually describe instruction-wise transformations that rely on an analysis A. The transformation itself is given by a function T i , which takes as input an instruction and the abstract state capturing what the compiler knows about the state before executing this instruction, and returns a new instruction. The correctness of this transformation is then expressed by a few extra conditions. First, the successors of the new instruction should be a subset of the original successors (T edges ). Second the execution of the transformed instruction in a state that is compatible with the abstract state obtained from the analysis should lead to the same new state and the new location in the code (T correct ). Third, a return instruction should be left unchanged (T return ). Fourth, the compatibility of a state with respect to an abstract state should not depend on the actual code functions that is stored in memory. All these aspects of an instruction-wise transformation are gathered in a module type TRANSFER ENTRIES.

Correct instruction-wise transformations never remove any instruction from the code graph. On the other hand, they may remove edges, if the analysis makes it possible to infer that these edges are never traversed during execution. This treatment also means that dead code is optimized at the same time as useful code. The actual removal of dead code is not part of these optimizations, it is just a side effect of the later translation from the LTL language to the Linear language.

Module Type TRANSFER ENTRIES.

Declare Module A : ANALYSIS.

Parameter T i : A.D → I → I. Parameter T edges : ∀d i s, s ∈ Succ T i (d, i) ⇒ s ∈ Succ i. Parameter T correct : ∀i s S S ′ d, A P (d, S) ⇒ (S, i) -→ (S ′ , s) ⇒ (S, T i (d, i)) -→ (S ′ , s
). Parameter T return : ∀d r s, T i (d, (Ireturn r, s)) = (Ireturn r, s). Parameter A mem : ∀(g : F → F ) d S, A P (d, S) ⇒ A P (d, T state (g, S)). End.

Transformations are thus obtained through an application of a functor that takes modules of type TRANSFER ENTRIES as input and returns modules of type TRANSFER. Some parts of the correctness proofs are done once and for all in this functor, but other parts are specific and done when establishing the facts T edges , T correct , T return , and A mem , which represent a big part of the proof (in number of lines) but are usually easy.

Instantiation

In this section we describe how we instantiate our functors to obtain the CP and CSE optimizations. The term optimization is a misnomer because there is no guarantee that the result code is the best possible. It is only the best that we can obtain using the information gathered by the analysis.

Constant propagation

The role of constant propagation is to replace some operations by a more efficient version: for example, by a "load constant" instruction when the result of the operation is known at compile time, or by an immediate operation when only one argument is known.

To use our predefined functor for analysis and transformation, the most difficult part is to define the semi-lattice corresponding to the domain of the analysis. Here, the goal of the analysis is to collect the known values associated to each register.

The domain of the analysis is the set of maps that associate to each register a numerical value when it is known. The set of maps from A to B is a semi-lattice if B itself is a semi-lattice and if A is a finite set. Therefore, we need to limit the number of registers. This is done using a dependent type: a register is a pair of a number (its identifier) and a proof that this identifier is less than a parameter map limit.

We define the semi-lattice corresponding to the codomain of the maps as the flat semi-lattice build upon the type of values that we can associate to registers at compile time :

v ::= n | f | (x, n)
that is, an integer, a float or the address of a known global variable plus an offset. Such a construction is possible since the equality on the type v is decidable. The analysis of an instruction consists in evaluating its result value and updating the register where the result is stored with this value. Naturally, this evaluation is only possible if all the arguments of the instruction have known values. Otherwise, the result register is set to top. The correctness criterion for this analysis is that if it claims that a register has a known value at some point, the actual value of the register at this point in every execution is equal to the claimed value.

Then, the transformation of an instruction first tries to evaluate the instruction and replaces the instruction by an instruction that directly stores the result in a register, when this is possible. For example, if r 1 = 1 and r 2 = 3 the instruction Iop Oadd r 1 r 2 r d will be replaced by Iop (Oconstint 4) r d .

If only some of the arguments are known, then the transformation tries to replace the instruction by a more efficient one. For example, if r 2 = n, then Iop Omul r 1 r 2 r d will be replaced by Iop (Oconstint 0) r d if n = 0, by Iop Omove r 1 r d if n = 1, by a left shift over r 1 if n a is a power of two, or by a immediate multiplication Iop (Omul imm n) r 1 r d otherwise.

Memory access is also optimized using a based addressing mode if the address is known at compile time. Finally, conditional branches are replaced by an Inop instruction, actually implementing an unconditional branch to the appropriate successor, if the result of the test is statically evaluable.

Common subexpression elimination

A program will frequently include multiple computations of equivalent expressions, e.g. array address calculations. The goal of common subexpression elimination is to factor out these redundant computations. An occurrence of an expression E is called a common subexpression if E was previously calculated and the values associated with the register that appear in E have not changed since the previous computation. In this case the compiler can replace the second occurrence of E by an access to the register containing the result of the first occurrence of E, thus saving the cost of recomputing E.

For example the sequence :

r 3 = r 1 + r 2 ; r 4 = r 1 ; r 5 = r 4 + r 2
will be replaced by :

r 3 = r 1 + r 2 ; r 4 = r 1 ; r 5 = r 3
Here the result of the analysis of an instruction is a map that associates to each register a symbolic expression corresponding to the operation that is stored in it. More precisely, the values associated to registers are a pair of a symbolic expression (the expression whose result is contained in the register) and a set of registers which contain the same value. The latter set is useful to keep track of multiple registers containing the result of the same computation, as often occurs following Imove instructions, and determine equivalence of symbolic expressions up to Imove instructions. For instance, in the code fragment above, it is known that the symbolic expressions r 1 + r 2 and r 4 + r 2 are equivalent because r 1 and r 4 contain the same value. Futhermore, we want to keep track that r 3 and r 5 contain the same value, even after a modification of r 2 that will invalidate the expression associated to both registers.

A concrete register set matches the result of the analysis at a given program point if the actual values of the registers satisfy the equalities between registers stated in the abstract values. The mappings of registers to symbolic expressions can be equipped with a well-founded semi-lattice structure, with the least upper bound operation corresponding roughly to the intersection of constraints. This semi-lattice construction is complex and we omit it here due to lack of space.

The analysis of an instruction that computes E and stores its result in a register r d first erases all references to r d in the map. If the register r d is not used as arguments of the instruction then the analysis tries to find a register containing an expression equivalent to E. In this case, the analysis updates the value associated to r d with the expression and the set of registers that contain the equivalent expression. It also adds the fact that registers in the set are all equal to r d . In all other cases, the value associated with r d is set to the expression E and an empty set of equal registers.

The transformation of an instruction r d = E is refreshingly simple: it becomes r d = r (a Imove instruction) if there exists a register r that contains the value of E, and is left unchanged otherwise. The Imove instructions thus introduced can disappear later during register allocation, if the register allocator manages to assign the same hardware register or stack location to both r and r d .

Related work and conclusions

In parallel with our work, several other teams developed machine-checked proofs of data-flow analyses and transformations. For instance, Cachera et al [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF] develop in Coq a general framework for lattices and data-flow equations over these lattices. Their framework is more general than ours, but they do not consider program transformations. Proofs of Kildall's work-list algorithm can also be found in machine-checked formalizations of Java byte-code verification such as [START_REF] Klein | Verified bytecode verifiers[END_REF].

Lerner et al [START_REF] Lerner | Automated soundness proofs for dataflow analyses and transformations via local rules[END_REF] propose Rhodium, a domain-specific language to express data-flow analyses and transformations exploiting the results of these analyses. Rhodium generates an implementation of both the analysis and the transformation and proof obligations that, once checked, imply the semantic correctness of the transformation. Rhodium specifications are definitely more concise than instantiations of our generic framework. However, the generated proof obligations do not appear significantly simpler than the proofs we have to provide for our functor applications. Moreover, the Rhodium tools must be trusted to generate correct implementations and sufficient proof obligations, while we obtain these guarantees by doing everything directly in Coq.

In summary, by exploiting the Coq module system, we have been able to factor out a significant part of specifications and correctness proofs for forward data-flow analyses and optimizations that exploit the results of these analyses. While the application of this framework to constant propagation is fairly standard, we believe we are the first to develop a mechanically verified proof for common subexpression elimination using the "Herbrand universe" approach. While this is not described in this paper, backward data-flow analyses is handled by a simple extension of our framework (basically, just reversing the control flow graph before using the forward analysis framework). We used this to prove correct liveness analysis as used in our register allocation phase.

A limitation of our approach, also found in Rhodium, is that we prove the correctness of transformations using simulation arguments that apply only when every instruction of the source code is mapped to zero, one or several instructions of the transformed code, and the states "before" and "after" the source instruction must match the states "before" and "after" the sequence of transformed instructions. This is not sufficient to prove some optimizations such as code motion, lifting of loop-invariant computations, or instruction scheduling, where computations occur in a different order in the source and transformed code. Because of this limitation, we envision to perform some optimizations such as loop optimizations not on the unstructured RTL intermediate code, but on the structured Cminor source code, whose big-step semantics makes it easier to reorder computations without worrying about intermediate computational states that do not match.

Fig. 2 .

 2 Fig. 2. RTL syntax

  head pointer p memory address a ::= (p, n) value v ::= n | f | a | ⊥ basic block b ::= ⊥ | c | a block B ::= C | b | Freed | NotYetAllocated memory m ::

Fig. 3 .

 3 Fig. 3. Value and memory

Fig. 4 .

 4 Fig. 4. Semantics of RTL

http://www-sop.inria.fr/lemme/concert/

as in C, when a pointer to a function is taken as argument.