Commit 0605b34e authored by Dario Pinto's avatar Dario Pinto
Browse files

add reducercommutativity

parent b8c8e612
......@@ -11,3 +11,8 @@ sed -i 's/__VERIFIER_nondet_uchar()/Frama_C_interval(0, UCHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_char()/Frama_C_interval(CHAR_MIN, CHAR_MAX)/g' $*
sed -i 's/__VERIFIER_nondet_ulong()/Frama_C_unsigned_long_interval(0, ULONG_MAX)/g' $*
sed -i 's/extern int Frama_C_interval(INT_MIN, INT_MAX);//g' $*
sed -i 's/extern short Frama_C_interval(SHRT_MIN, SHRT_MAX);//g' $*
sed -i 's/extern unsigned chard Frama_C_interval(0, UCHAR_MAX);//g' $*
sed -i 's/extern char Frama_C_interval(CHAR_MIN, CHAR_MAX);//g' $*
sed -i 's/exterm unsigned long Frama_C_unsigned_long_interval(0, ULONG_MAX);//g' $*
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
MACHDEP = x86_32
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
-D__FC_PATCHED \
-I../../lib \
-I../../../frama-c/share/libc
## General flags
FCFLAGS += \
-add-symbolic-path=.:..\
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
-c11\
## Eva-specific flags
EVAFLAGS += \
-eva-precision 5 \
-eva-warn-key builtins:missing-spec=abort \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..\
# exclude files with recursive functions, and those testing memory leaks
filter-out-substring = $(foreach v,$(2),$(if $(findstring $(1),$(v)),,$(v)))
SRCS:=$(sort $(wildcard ../*.c))
# [target] converts a file name into a suitable target name,
# removing the initial '../', the final '.c'.
target = $(subst /,/,$(patsubst %.c,%,$(1:../%=%)))
EVA_TARGETS:=$(foreach s,$(SRCS),$(call target,$(s)).eva)
TARGETS:=$(EVA_TARGETS)
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
define generate-parse-rules =
$(call target,$(1)).parse: $(if $(findstring cross_file,$(1)),,) $(1)
$(call target,$(1)).parse: SRCS += ../../../frama-c/share/libc/__fc_builtin.c
$(call target,$(1)).eva/eval.txt: $(call target, $(1)).eva
./evaluate_case.sh $(subst .c,,$(1)).yml $$</alarms.csv $$</nonterm.log > $$</eval.txt
endef
$(foreach s,$(SRCS),$(eval $(call generate-parse-rules,$(s))))
eval_summary.txt: $(addsuffix /eval.txt, $(TARGETS))
cat $^ > eval_summary.txt
evaluate: eval_summary.txt
.PHONY: eval_summary.txt
fclean: clean
rm eval_summary.txt
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
###############################################################################
Termination spec: true
avg.eva/alarms.csv (true): Valid
Unreachability spec: true
avg.eva/alarms.csv (true): Imprecise
__________________________________
Termination spec: true
avg05-1.eva/alarms.csv (true): Valid
Unreachability spec: true
avg05-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
avg05-2.eva/alarms.csv (false): Valid
__________________________________
Defined Behavior spec: false
avg10-1.eva/alarms.csv (false): Valid
__________________________________
Termination spec: true
avg10-2.eva/alarms.csv (true): Valid
Unreachability spec: true
avg10-2.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
avg20-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
avg20-2.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
avg40-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
avg40-2.eva/alarms.csv (true): Valid
__________________________________
Unreachability spec: true
avg60-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
avg60-2.eva/alarms.csv (false): Valid
__________________________________
Termination spec: true
max.eva/alarms.csv (true): Valid
Unreachability spec: true
max.eva/alarms.csv (true): Imprecise
__________________________________
Termination spec: true
max05-1.eva/alarms.csv (true): Valid
Unreachability spec: true
max05-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
max05-2.eva/alarms.csv (false): Valid
__________________________________
Termination spec: true
max10-1.eva/alarms.csv (true): Valid
Unreachability spec: true
max10-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
max10-2.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
max20-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
max20-2.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
max40-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
max40-2.eva/alarms.csv (false): Valid
__________________________________
Defined Behavior spec: false
max60-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
max60-2.eva/alarms.csv (true): Valid
__________________________________
Termination spec: true
rangesum.eva/alarms.csv (true): Valid
Unreachability spec: false
rangesum.eva/alarms.csv (false): Imprecise
__________________________________
Termination spec: true
rangesum05.eva/alarms.csv (true): Valid
Unreachability spec: false
rangesum05.eva/alarms.csv (false): Imprecise
__________________________________
Termination spec: true
rangesum10.eva/alarms.csv (true): Valid
Unreachability spec: false
rangesum10.eva/alarms.csv (false): Imprecise
__________________________________
Unreachability spec: false
rangesum20.eva/alarms.csv (false): Imprecise
__________________________________
Unreachability spec: false
rangesum40.eva/alarms.csv (false): Imprecise
__________________________________
Unreachability spec: false
rangesum60.eva/alarms.csv (false): Imprecise
__________________________________
Termination spec: true
sep.eva/alarms.csv (true): Valid
Unreachability spec: true
sep.eva/alarms.csv (true): Imprecise
__________________________________
Termination spec: true
sep05-1.eva/alarms.csv (true): Valid
Unreachability spec: true
sep05-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sep05-2.eva/alarms.csv (false): Valid
__________________________________
Defined Behavior spec: false
sep10-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sep10-2.eva/alarms.csv (true): Valid
__________________________________
Unreachability spec: true
sep20-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sep20-2.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sep40-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sep40-2.eva/alarms.csv (false): Valid
__________________________________
Defined Behavior spec: false
sep60-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sep60-2.eva/alarms.csv (true): Valid
__________________________________
Termination spec: true
sum.eva/alarms.csv (true): Valid
Unreachability spec: true
sum.eva/alarms.csv (true): Imprecise
__________________________________
Defined Behavior spec: false
sum05-1.eva/alarms.csv (false): Valid
__________________________________
Termination spec: true
sum05-2.eva/alarms.csv (true): Valid
Unreachability spec: true
sum05-2.eva/alarms.csv (true): Valid
__________________________________
Termination spec: true
sum10-1.eva/alarms.csv (true): Valid
Unreachability spec: true
sum10-1.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sum10-2.eva/alarms.csv (false): Valid
__________________________________
Defined Behavior spec: false
sum20-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sum20-2.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sum40-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sum40-2.eva/alarms.csv (true): Valid
__________________________________
Defined Behavior spec: false
sum60-1.eva/alarms.csv (false): Valid
__________________________________
Unreachability spec: true
sum60-2.eva/alarms.csv (true): Valid
__________________________________
#!/bin/bash -u
# Script is not yet complete and shouldn't yet be used
# https://sv-comp.sosy-lab.org/2020/rules.php
# to check the meaning of all specs in *.yml files
if [ $# -lt 2 ]; then
echo "usage: $0 (dotyml_file_spec) path/to/alarms.csv path/to/nonterm.log"
exit 1
fi
#set argument variables
dotyml="$1"
alarmcsv="$2"
nontermlog="$3"
#get number of lines in FramaC's target alarm.csv file
alarms=$(wc -l $alarmcsv | cut -d' ' -f1)
#check and get FramaC's conclusion
valid_deref=$(grep "index_bound" $alarmcsv)
if [ -z "$valid_deref" ]; then
valid_deref=$(grep "mem_access" $alarmcsv)
fi
#check number of lines in target's nonterm.log
nonterm=$(wc -l $nontermlog | cut -d' ' -f1)
#check and get spec true/false
termination=$(grep "property_file: ../properties/termination.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
#check and get spec true/false
memsafety=$(grep "property_file: ../properties/valid-memsafety.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
#check and get spec true/false
defbehavior=$(grep "property_file: ../properties/def-behavior.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
#check and get spec true/false
unreachability=$(grep "property_file: ../properties/unreach-call.prp" $dotyml -A 1 | grep -v "property_file" | cut -d' ' -f6)
## This part is suppose to establish if program must terminate.
# if $termination = true then it must terminate one way or another, call to abort is accepted
# else if $termination = false, then program is most likely an infinite loop and must not exit by ordinary means, ie should be interrupted
#
# NO FALSE CASE IN ARRAY-EXAMPLES
if [ -n "$termination" ]; then
printf "\nTermination spec: $termination\n"
case $termination in
"true")
if [ "$nonterm" -ge 0 ]; then
echo "$2 ($termination): Valid"
else
echo "$2 ($termination): Imprecise"
fi
;;
*)
printf "An error occured in termination :C.\n"
exit 1
esac
fi
## This part is suppose to establish whether the error function __VERIFIER_error() was reached during a finite execution of the program.
#
# if $unreachability = true, then given function must never be reached in any path of the execution.
# else if $unreachability = false, then given __VERIFIER_error() function must be reached at some point of the program, and program must exit by a call to the abort(); function.
#
#
if [ -n "$unreachability" ]; then
printf "\nUnreachability spec: $unreachability\n"
case $unreachability in
"true")
if [ "$nonterm" -eq 0 ]; then
echo "$2 ($unreachability): Valid"
else
echo "$2 ($unreachability): Imprecise"
fi
;;
"false")
if [ "$nonterm" -ne 0 ]; then
echo "$2 ($unreachability): Valid"
else
echo "$2 ($unreachability): Imprecise"
fi
;;
*)
printf "An error occured in unreachability :C.\n"
exit 1
esac
fi
## This part tends to adress the memsafety spec. To verify a set of subspec found in all targets.yml files
#
# The only memsafety subspec present in ARRAY-EXAMPLES is VALID-DEREF. Therefore it's the only one this script checks
#
#FALSE case is omitted because of its absence in ARRAY-EXAMPLES
if [ -n "$memsafety" ]; then
printf "\nValid-Memsafety spec: $memsafety\n"
case $memsafety in
"false")
if [ -n "$valid_deref" ]; then
echo "$2 ($memsafety): Valid"
else
echo "$2 ($memsafety): Imprecise"
fi
;;
*)
printf "An error occured in memsafety :C.\n"
exit 1
esac
fi
## This part tends to handle the one and only case of Def-behaviour spec.
# it is FALSE and is found in standard_find_ground-2.yml and standard_sentinel-1.yml
if [ -n "$defbehavior" ]; then
printf "\nDefined Behavior spec: $defbehavior\n"
case $defbehavior in
"false")
if [ "$alarms" -ne 0 ]; then
echo "$2 ($defbehavior): Valid"
else
echo "$2 ($defbehavior): Imprecise"
fi
;;
*)
printf "An error occured in defbehavior :C.\n"
exit 1
esac
fi
echo "__________________________________"
../frama-c-cgc-path.mk
\ No newline at end of file
Copyright (c) 2015, Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND ANY
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
DAMAGE.
\ No newline at end of file
LEVEL := ../
include $(LEVEL)/Makefile.config
Benchmarks used in the paper "Commutativity of Reducers"
which was published at TACAS 2015 and
written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
We checks if a function is "deterministic" w.r.t. all possible permutations
of an input array. Such property is desirable for reducers in the
map-reduce programming model. It ensures that the program always computes
the same results on the same input data set.
Submitted by Matthias Heizmann.
/*
* Benchmarks used in the paper "Commutativity of Reducers"
* which was published at TACAS 2015 and
* written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
* http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
*
* We checks if a function is "deterministic" w.r.t. all possible permutations
* of an input array. Such property is desirable for reducers in the
* map-reduce programming model. It ensures that the program always computes
* the same results on the same input data set.
*/
#define fun avg
#include "common.h"
extern void abort(void);
void reach_error(){}
extern int __VERIFIER_nondet_int(void);
int N;
int avg (int x[N])
{
int i;
long long ret;
ret = 0;
for (i = 0; i < N; i++) {
ret = ret + x[i];
}
return ret / N;
}
int main ()
{
N = Frama_C_interval(INT_MIN, INT_MAX);
if (N > 1) {
int x[N];
int temp;
int ret;
int ret2;
int ret5;
ret = fun(x);
temp=x[0];x[0] = x[1]; x[1] = temp;
ret2 = fun(x);
temp=x[0];
for(int i =0 ; i<N-1; i++){
x[i] = x[i+1];
}
x[N-1] = temp;
ret5 = fun(x);
if(ret != ret2 || ret !=ret5){
{reach_error();abort();}
}
}
return 1;
}
format_version: '1.0'
# old file name: avg_true-unreach-call_true-termination.i
input_files: 'avg.i'
properties:
- property_file: ../properties/termination.prp
expected_verdict: true
- property_file: ../properties/unreach-call.prp
expected_verdict: true
- property_file: ../properties/coverage-branches.prp
- property_file: ../properties/coverage-conditions.prp
- property_file: ../properties/coverage-statements.prp
/*
* Benchmarks used in the paper "Commutativity of Reducers"
* which was published at TACAS 2015 and
* written by Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang.
* http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_9
*
* We checks if a function is "deterministic" w.r.t. all possible permutations
* of an input array. Such property is desirable for reducers in the
* map-reduce programming model. It ensures that the program always computes
* the same results on the same input data set.
*/
#define N 5
#define fun avg
#include "common.h"
extern void abort(void);
void reach_error(){}
int avg (int x[N])
{
int i;
long long ret;
ret = 0;
for (i = 0; i < N; i++) {
ret = ret + x[i];
}
return ret / N;
}
int main ()
{
int x[N];
int temp;
int ret;
int ret2;
int ret5;
for (int i = 0; i < N; i++) {
x[i] = Frama_C_interval(INT_MIN, INT_MAX);
}