Connect with us

Hi, what are you looking for?

Tecnología

¿Se puede confiar en el compilador de C?

Los lenguajes de programación vienen en “dos sabores”, intérpretes y compiladores. Los primeros, los intérpretes, obligan al sistema a analizar cada línea de código a ver si está correctamente escrita y si es así, ejecutar lo que el programador quiere. Si por alguna razón el sistema regresa a esa línea, tiene que volver a verificar que está bien escrita, aunque ya lo haya hecho antes. Por otra parte, los compiladores, traducen a código de máquina las instrucciones del programador. Así, el compilador genera un código que, en principio, corre unas 10 a 100 veces más rápido que la versión interpretada.

Crean algoritmo capaz de predecir tiros de tenis

Pero claramente, los programas que en general se escriben, resuelven problemas administrativos, financieros, o bien se usan para jugar, etcétera. Sin embargo, hay aplicaciones que concretamente tienen que correr correctamente porque pudiese estar la vida de alguien en juego. Pensemos por ejemplo en programas que llevan el control de un marcapasos, el cual no pude funcionar mal, no puede tener “bugs” que pongan en peligro la vida del paciente. O pensemos en un programa que corre en un dispositivo como una consola electrónica que usan los buzos y que da los parámetros para saber qué tan rápido debe subir a la superficie para no sufrir problemas por una mala descompresión.

Y esto hace pensar que una cosa es hacer un programa que haga cálculos para -digamos- controlar la contabilidad y otra cuando se pone en juego la vida de alguien. ¿Podríamos confiar entonces en que el compilador va a traducir correctamente el código? La pregunta puede ser muy sensible en algunos aspectos y hay quien trabaja ya en este tema.

Así, se ha desarrollado el compilador COMPCERT, el cual es un compilador formalmente verificado, lo que significa es que hay una prueba matemática que indica que al escribir código en C, se traduce correctamente a lenguaje de máquina. El compilador puede generar código para PowerPC, ARM, RISC-V y x86, el cual acepta un subconjunto del ISO C 99 con un par de extensiones. Es claro que este compilador probablemente no pueda generar código tan rápido como el gcc, pero lo que sí vale la pena destacar es que el código creado cumple con las especificaciones dadas.

Hay que reconocer que la idea de COMPCERT es buena, pero no hay garantía que un programa escrito con este compilador va a correr correctamente. Por ejemplo, si ponemos “x=1/A”, donde A es una variable entera y en algún caso, dicha variable se vuelve cero, tendremos un error y un problema con nuestra lógica en el software. Esto no es atribuible directamente al compilador. Vamos, es un error del usuario.

Para que un compilador de estas características pueda funcionar, se tienen que poner algunas restricciones, que en algunos compiladores se llaman “directivas”, pero que aquí no son opcionales. Por ejemplo, arreglos de longitud variable no están permitidos y no se puede usar longjmp ni setjmp. Hay restricciones en el caso de la instrucción “switch” también. Sin embargo, hay una variedad de opciones que permiten examinar el código corriendo a través de un intérprete.

Y más de uno podrá pensar que los compiladores normalmente traducen correctamente, pero la realidad es que en la documentación de los compiladores, se han hallado artículos (de 1995 al 2011), en donde se ha hallado errores en la forma de compilar, incluso en los compiladores más populares.

Para que el COMPCERT funcione correctamente, un asistente de la prueba matemática del código compilador checa el código pasando por el mismo en 15 ocasiones, y todas deben probarse como correctas. Incluso así, hay un 10% de código que se ha demostrado que no es correcto. Los desarrolladores de COMPCERT dedicaron 6 años de procesamiento de máquina paras hallar errores de compilación usando Csmith y no pudieron hallar ningún error, cosa que no fue así considerando otros compiladores.

Esta idea de los compiladores verificados es interesante aunque quizás no es necesaria en la mayoría de las aplicaciones. Sin embargo, es un paso para hacer que formalmente los compiladores sean herramientas más sólidas.

La entrada ¿Se puede confiar en el compilador de C? se publicó primero en unocero.

Click to comment

Comenta

Últimas noticias

Ambulancia roja y blanca estacionada en una calle urbana de noche, relacionada con un ataque armado en Culiacán.

Culiacán

Balacera en Rosario Uzarraga deja 2 muertos y 1 herido: Fiscalía investiga mientras policía municipal y Cruz Roja responden 🚨👮‍♂️🚑 #Culiacán #Seguridad

Soldado y camioneta militar en operativo tras hallazgo de cadáver en Culiacán Soldado y camioneta militar en operativo tras hallazgo de cadáver en Culiacán

Culiacán

Sangriento hallazgo en Culiacán: hombre ejecutado frente a edificio en ruinas, Fiscalía asegura escena con casquillos 🕵️‍♂️🔫 #Justicia #Culiacán

Dos militares en vigilancia urbana con equipo y armamento en Culiacán, cerca de una zona de hallazgo de cadáver. Dos militares en vigilancia urbana con equipo y armamento en Culiacán, cerca de una zona de hallazgo de cadáver.

Culiacán

Hallan ejecutado a hombre en Culiacán, crisis de inseguridad alcanza colonia Vicente Guerrero 😱🔥 #Inseguridad #Culiacán

Cinta amarilla de 'PROHIBIDO' en escena de crimen en San Cristóbal de la Barranca, Jalisco. Cinta amarilla de 'PROHIBIDO' en escena de crimen en San Cristóbal de la Barranca, Jalisco.

Nacionales

Masacre familiar en Jalisco: asesinan a cuatro en barranco y FGE investiga posible sobreviviente 💔🚨 #JusticiaYa #Jalisco

Cinco personas en un evento formal sobre inversión en salud en Sinaloa, con un hombre hablando al micrófono. Cinco personas en un evento formal sobre inversión en salud en Sinaloa, con un hombre hablando al micrófono.

Actualización

¡Claudia Sheinbaum activa 146 mdp para hospitales sinaloenses y estrena quirófano para trasplantes! 🏥💉 #SaludSinaloa #Culiacán

Ovidio Guzmán López en audiencia judicial en Illinois, julio 2025 Ovidio Guzmán López en audiencia judicial en Illinois, julio 2025

Internacionales

¡Ovidio Guzmán López se declara culpable, renuncia a apelar y confiesa homicidios en histórico pacto con EEUU⚖️💥 #Justicia #Narcotráfico

Suscríbete y recibe noticias

Tendencia

Sinaloa

Familiares y vecinos bloquean Rotarismo y base militar exigiendo: ¡VIVO se lo llevaron, VIVO lo queremos! ✊📢 #Justicia #Heriberto

Sinaloa

Crisis brutal: 2 000 comercios cierran, extorsiones suben 300% y UCC exige rescate urgente 💥📉💸 #CuliacánAlerta #RescateEconómico

Sinaloa

Violento machetazo termina con la vida del agente Demetrio Santiago N. 😢👮‍♂️🩸 #JusticiaParaDemetrio #Ahome

Sinaloa

Atracan con arma a funerario en carretera Guasave–León Fonseca, agresor huye con 1,920 pesos 🚨🔫 #Seguridad #Justicia

Business

Ovidio Guzmán se derrumba: admite crimen organizado, pacta $80M y coopera con EE.UU. 🔥🔒💰⚖️ #Justicia #Fentanilo

Sinaloa

Choque armado sacude El Quemadito: presuntos grupos rivales desatan violencia en Culiacán 🚨🔥 #Culiacán #Seguridad

Sinaloa

Brutal feminicidio: esposo acribilla a Rosa Elvira en Cosalá 😡🔫💔 #JusticiaParaRosa #NiUnaMenos

Internacionales

Brutal ataque viral en Torre Pacheco: jóvenes golpean a anciano por “likes” 😡📲 ¡Exigimos justicia! #NoALaViolencia #TorrePacheco

Desarrollado por
FIIXCOM