Skip to content

Commit cf5e27e

Browse files
smitschsmitsch
committed
C code generator: log formula safety intervals (LaTeX)
1 parent f1bb253 commit cf5e27e

File tree

1 file changed

+212
-1
lines changed

1 file changed

+212
-1
lines changed

‎keymaerax-webui/src/main/scala/edu/cmu/cs/ls/keymaerax/codegen/CExpression.scala

+212-1
Original file line numberDiff line numberDiff line change
@@ -285,4 +285,215 @@ class CExpressionLogPrettyPrinter extends (CExpression => String) {
285285
case COr(l, r) => "or(" + print(l) + ", " + print(r) + ")"
286286
}
287287

288-
}
288+
}
289+
290+
/** Prints C expressions that keep track of the reason for their value. NOT interval arithmetic, intervals are for
291+
* comparisons and formulas. Logs original formula and does unverified metric conversion to measure safety. */
292+
class CExpressionIntervalLaTeXLogPrettyPrinter extends (CExpression => String) {
293+
294+
override def apply(e: CExpression): String = {
295+
"eval(" + print(e) + ")"
296+
}
297+
298+
def printOperators: String = {
299+
"""typedef struct expr {
300+
| long double low;
301+
| long double high;
302+
| const char* source;
303+
|} expr;
304+
|
305+
|const char* klog(const char* format, ...) {
306+
| va_list args;
307+
| va_start(args, format);
308+
| /* don't care about memory leak */
309+
| char* res = (char*)malloc(32758 * sizeof(char));
310+
| vsnprintf(res, 32758, format, args);
311+
| va_end(args);
312+
| return res;
313+
|}
314+
|
315+
|expr number(long double v) {
316+
| return (expr) {
317+
| .low = v,
318+
| .high = v,
319+
| .source = klog("%Lf", v)
320+
| };
321+
|}
322+
|
323+
|expr variable(long double v, const char* name) {
324+
| return (expr) {
325+
| .low = v,
326+
| .high = v,
327+
| .source = klog("\\overset{%Lf}{\\text{%s}}", name, v)
328+
| };
329+
|}
330+
|
331+
|expr neg(expr c) {
332+
| return (expr) {
333+
| .low = -c.high,
334+
| .high = -c.low,
335+
| .source = klog("-(%s)", c.source)
336+
| };
337+
|}
338+
|
339+
|expr minus(expr l, expr r) {
340+
| return (expr) {
341+
| .low = l.low - r.low,
342+
| .high = l.high - r.high,
343+
| .source = klog("(%s) - (%s)", l.source, r.source)
344+
| };
345+
|}
346+
|expr plus(expr l, expr r) {
347+
| return (expr) {
348+
| .low = l.low + r.low,
349+
| .high = l.high + r.high,
350+
| .source = klog("(%s) + (%s)", l.source, r.source)
351+
| };
352+
|}
353+
|expr times(expr l, expr r) {
354+
| return (expr) {
355+
| .low = l.low * r.low,
356+
| .high = l.high * r.high,
357+
| .source = klog("(%s) * (%s)", l.source, r.source)
358+
| };
359+
|}
360+
|expr divide(expr l, expr r) {
361+
| return (expr) {
362+
| .low = l.low / r.low,
363+
| .high = l.high / r.high,
364+
| .source = klog("(%s) / (%s)", l.source, r.source)
365+
| };
366+
|}
367+
|expr power(expr l, expr r) {
368+
| return (expr) {
369+
| .low = pow(l.low, r.low),
370+
| .high = pow(l.high, r.high),
371+
| .source = klog("(%s)^(%s)", l.source, r.source)
372+
| };
373+
|}
374+
|expr kmin(expr l, expr r) {
375+
| return (expr) {
376+
| .low = fminl(l.low, r.low),
377+
| .high = fminl(l.high, r.high),
378+
| .source = fminl(l.low, r.low)==l.low ? klog("min(%s, _)", l.source) : klog("min(_, %s)", r.source)
379+
| };
380+
|}
381+
|expr kmax(expr l, expr r) {
382+
| return (expr) {
383+
| .low = fmaxl(l.low, r.low),
384+
| .high = fmaxl(l.high, r.high),
385+
| .source = fmaxl(l.low, r.low)==l.low ? klog("max(%s, _)", l.source, l.low) : klog("max(_, %s)", r.source, r.low),
386+
| };
387+
|}
388+
|expr kabs(expr c) {
389+
| return (expr) {
390+
| .low = fabsl(c.low),
391+
| .high = fabsl(c.high),
392+
| .source = klog("abs(%s)", c.source)
393+
| };
394+
|}
395+
|expr lt(expr l, expr r) {
396+
| return (expr) {
397+
| .low = l.low - r.low, /* todo: wrong answer when == */
398+
| .high = l.low - r.low,
399+
| .source = klog("%s \\overset{%Lf}{<} %s", l.source, l.low-r.low, r.source)
400+
| };
401+
|}
402+
|expr leq(expr l, expr r) {
403+
| return (expr) {
404+
| .low = l.low - r.low,
405+
| .high = l.low - r.low,
406+
| .source = klog("%s \\overset{%Lf}{\\leq} %s", l.source, l.low-r.low, r.source)
407+
| };
408+
|}
409+
|expr eq(expr l, expr r) {
410+
| return (expr) {
411+
| .low = -fabsl(l.low - r.low),
412+
| .high = -fabsl(l.low - r.low),
413+
| .source = klog("%s \\overset{%Lf}{=} %s", l.source, -fabsl(l.low-r.low), r.source)
414+
| };
415+
|}
416+
|expr neq(expr l, expr r) {
417+
| return (expr) {
418+
| .low = fabsl(l.low - r.low), /* note: wrong answer when == */
419+
| .high = fabsl(l.low - r.low),
420+
| .source = klog("%s \\overset{%Lf}{\\neq} %s", l.source, fabsl(l.low-r.low), r.source)
421+
| };
422+
|}
423+
|expr geq(expr l, expr r) {
424+
| return (expr) {
425+
| .low = r.low - l.low,
426+
| .high = r.low - l.low,
427+
| .source = klog("%s \\overset{%Lf}{\\geq} %s", l.source, r.low-l.low, r.source)
428+
| };
429+
|}
430+
|expr gt(expr l, expr r) {
431+
| return (expr) {
432+
| .low = r.low - l.low, /* todo: wrong answer when == */
433+
| .high = r.low - l.low,
434+
| .source = klog("%s \\overset{%Lf}{>} %s", l.source, r.low-l.low, r.source)
435+
| };
436+
|}
437+
|expr and(expr l, expr r) {
438+
| return (expr) {
439+
| .low = fminl(l.low, r.low),
440+
| .high = fmaxl(l.high, r.high),
441+
| .source = l.high <= 0 ? (r.high <= 0 ? klog("%s \\overset{[%Lf,%Lf]}{\\wedge} %s", l.source, fminl(l.low, r.low), fmaxl(l.high, r.high), r.source) : klog("\\_ \\overset{[%Lf,%Lf]}{\\wedge} %s", r.source, fminl(l.low, r.low), fmaxl(l.high, r.high))) : klog("%s \\overset{[%Lf,%Lf]}{\\wedge} \\_", l.source, fminl(l.low, r.low), fmaxl(l.high, r.high))
442+
| };
443+
|}
444+
|expr or(expr l, expr r) {
445+
| return (expr) {
446+
| .low = fmaxl(l.low, r.low),
447+
| .high = fminl(l.high, r.high),
448+
| .source = l.low <= 0 ? klog("%s \\overset{[%Lf,%Lf]}{\\vee} \\_", l.source, fmaxl(l.low, r.low), fminl(l.high, r.high)) : (r.low <= 0 ? klog("\\_ \\overset{[%Lf,%Lf]}{\\vee} %s", r.source, fmaxl(l.low, r.low), fminl(l.high, r.high)) : klog("%s \\overset{[%Lf,%Lf]}{\\vee} %s", l.source, fmaxl(l.low, r.low), fminl(l.high, r.high), r.source))
449+
| };
450+
|}
451+
|expr not(expr c) {
452+
| return (expr) {
453+
| .low = c.high,
454+
| .high = c.low,
455+
| .source = klog("\\overset{[%Lf,%Lf]}{\\neg}(%s)", c.source, c.high, c.low)
456+
| };
457+
|}
458+
|long double eval(expr e) {
459+
| printf("expr = [%Lf,%Lf] from %s\r\n", e.low, e.high, e.source);
460+
| return e.high;
461+
|}
462+
""".stripMargin
463+
}
464+
465+
//@todo print only necessary parentheses
466+
private def print(e: CExpression): String = e match {
467+
case CNumber(n) => "number(" + n.underlying().toString + ")"
468+
case CVariable(n) => "variable(" + n + ", \"" + n + "\")"
469+
case CUnaryFunction(n, arg) => n + "(" + print(arg) + ")"
470+
case CPair(l, r) => print(l) + "," + print(r)
471+
case CNeg(c) => "neg(" + print(c) + ")"
472+
case CPlus(l, r) => "plus(" + print(l) + ", " + print(r) + ")"
473+
case CMinus(l, r) => "minus(" + print(l) + ", " + print(r) + ")"
474+
case CTimes(l, r) => "times(" + print(l) + ", " + print(r) + ")"
475+
case CDivide(l, r) => "divide(" + print(l) + ", " + print(r) + ")"
476+
case CPower(l, r) => "power(" + print(l) + ", " + print(r) + ")"
477+
/** Convert interpreted functions to corresponding C functions.
478+
*
479+
* C 99 standard:
480+
* double fabs()
481+
* float fabsf()
482+
* long double fabsl()
483+
*/
484+
case CMin(l, r) => "kmin(" + print(l) + ", " + print(r) + ")"
485+
case CMax(l, r) => "kmax(" + print(l) + ", " + print(r) + ")"
486+
case CAbs(c) => "kabs(" + print(c) + ")"
487+
488+
case CLess(l, r) => "lt(" + print(l) + ", " + print(r) + ")"
489+
case CLessEqual(l, r) => "leq(" + print(l) + ", " + print(r) + ")"
490+
case CEqual(l, r) => "eq(" + print(l) + ", " + print(r) + ")"
491+
case CGreaterEqual(l, r) => "geq(" + print(l) + ", " + print(r) + ")"
492+
case CGreater(l, r) => "gt(" + print(l) + ", " + print(r) + ")"
493+
case CNotEqual(l, r) => "neq(" + print(l) + ", " + print(r) + ")"
494+
case CNot(c) => "not(" + print(c) + ")"
495+
case CAnd(l, r) => "and(" + print(l) + ", " + print(r) + ")"
496+
case COr(l, r) => "or(" + print(l) + ", " + print(r) + ")"
497+
}
498+
499+
}

0 commit comments

Comments
 (0)