From 9190cea1b268e8863eb41560d8579f08d302d3a4 Mon Sep 17 00:00:00 2001 From: Benedikt Becker Date: Wed, 19 Feb 2020 01:16:32 +0100 Subject: [PATCH] Log incompleteness messages to semantics and symbolic interpreter Not used in concrete interpreter. The incompleteness messages could be removed from semantics but this would require ignoring the logging buffer in all equalities between states. --- src/concrete/semantics.mlw | 13 +++++++++---- src/symbolic/symbolicInterpreter.mlw | 7 ++++--- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/concrete/semantics.mlw b/src/concrete/semantics.mlw index df5505d0..d641a898 100644 --- a/src/concrete/semantics.mlw +++ b/src/concrete/semantics.mlw @@ -77,6 +77,9 @@ module Buffers val function split_on_default_ifs string : list string + let constant loop_limit_message = "[INCOMPLETE] Loop limit" + let constant stack_limit_message = "[INCOMPLETE] Stack limit" + scope Stdout use bool.Bool @@ -106,10 +109,10 @@ module Buffers let function to_stdin out = reverse (all_lines out) - let output str out = + let function output str out = { out with line = String.concat out.line str } - let newline out = + let function newline out = { line = ""; lines = Cons out.line out.lines } (* http://pubs.opengroup.org/onlinepubs/9699919799/utilities/V3_chap02.html#tag_18_06_03 *) @@ -653,7 +656,8 @@ module Semantics eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) -> ctx.func_env[id] = Some ins -> inp.config.stack_size = Finite stk -> - eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1, ctx, BIncomplete) + let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in + eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1', ctx, BIncomplete) | eval_call_function: forall stk inp ctx ctx2 sta sta1 sta2 id es args ins bhv. eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) -> @@ -704,7 +708,8 @@ module Semantics | eval_while_loop_limit: forall stk ctr b inp ctx sta ins1 ins2. 0 <= ctr -> inp.config.loop_limit = Finite ctr -> - eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta, ctx, BIncomplete) ctr b + let sta' = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in + eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta', ctx, BIncomplete) ctr b (** Condition not normal *) | eval_while_abort_condition: forall stk ctr b inp ctx ctx1 sta sta1 ins1 ins2 bhv1. diff --git a/src/symbolic/symbolicInterpreter.mlw b/src/symbolic/symbolicInterpreter.mlw index 45517887..9c6f5082 100644 --- a/src/symbolic/symbolicInterpreter.mlw +++ b/src/symbolic/symbolicInterpreter.mlw @@ -686,7 +686,7 @@ module Interpreter if stk = get_finite inp.config.stack_size then (* Stack overflow *) let aux arg = let sta', _ = arg in - (* let sta' = { sta' with log = Stdout.(newline (output "INCOMPLETE: STACK_OVERFLOW" sta'.log)) } in *) + let sta' = { sta' with log = Stdout.(newline (output stack_limit_message sta'.log)) } in {state=sta'; context=ctx; data=()} in Rs.({empty with failure = Cn.map aux arg_res}) @@ -695,7 +695,8 @@ module Interpreter eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) -> ctx.func_env[id] = Some ins -> inp.config.stack_size = Finite stk -> - Rs.mem {state=sta1; context=ctx; data=()} BIncomplete result + let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in + Rs.mem {state=sta1'; context=ctx; data=()} BIncomplete result } else (* Execute function *) let res2 = @@ -1003,7 +1004,7 @@ module Interpreter } = let loop_limit = get_finite inp.config.loop_limit in if ctr = loop_limit then - (* let sta = { sta with log = Stdout.(newline (output "INCOMPLETE: LOOP_LIMIT" sta.log)) } in *) + let sta = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in Rs.({empty with failure=Cn.singleton {state=sta; context=ctx; data=(ctr, b)}}) else let res1_normal, res1_abort =