From c176223b118f4e0612043a1d6999bef1821a2ba3 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Fri, 1 Oct 2021 20:42:25 +0300 Subject: [PATCH 01/35] Remove some junk from bench scripts. --- update_bench.rb | 2 -- update_bench_traces.rb | 2 -- 2 files changed, 4 deletions(-) diff --git a/update_bench.rb b/update_bench.rb index 84d5a1d3d..1a3a765de 100755 --- a/update_bench.rb +++ b/update_bench.rb @@ -116,8 +116,6 @@ def print_res (i) f.puts "N/A" end end - gb_file = $testresults + File.basename(p.path,".c") + ".mutex.txt" - f.puts "" f.puts "" end f.puts "" diff --git a/update_bench_traces.rb b/update_bench_traces.rb index ac95cdb38..eef58bc3c 100755 --- a/update_bench_traces.rb +++ b/update_bench_traces.rb @@ -128,8 +128,6 @@ def print_res (i) end comparefile = File.basename(p.path,".c") + ".compare.txt" f.puts "compare" - gb_file = $testresults + File.basename(p.path,".c") + ".mutex.txt" - f.puts "" f.puts "" end f.puts "" From ea128039c4db38f657d1261f7606fa2cd5f3296a Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Fri, 1 Oct 2021 20:45:57 +0300 Subject: [PATCH 02/35] Add initial version of bencharking script. --- .gitignore | 1 + index/incremental.txt | 6 + linux/drivers/char/applicom01.patch | 4 + update_bench_incremental.rb | 314 ++++++++++++++++++++++++++++ 4 files changed, 325 insertions(+) create mode 100644 index/incremental.txt create mode 100644 linux/drivers/char/applicom01.patch create mode 100755 update_bench_incremental.rb diff --git a/.gitignore b/.gitignore index cae64517d..6c284fcc9 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ bench_result goblint juliet/C juliet/summary_table.html +incremental_data diff --git a/index/incremental.txt b/index/incremental.txt new file mode 100644 index 000000000..3d7562c3a --- /dev/null +++ b/index/incremental.txt @@ -0,0 +1,6 @@ +Group: Char Drivers + +char/applicom.c +linux! +drivers/char/applicom.c +- diff --git a/linux/drivers/char/applicom01.patch b/linux/drivers/char/applicom01.patch new file mode 100644 index 000000000..c6a64d05f --- /dev/null +++ b/linux/drivers/char/applicom01.patch @@ -0,0 +1,4 @@ +174c174 +< for (i = 0; i < MAX_BOARD; i++) { +--- +> for (i = 0; i <= MAX_BOARD; i++) { diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb new file mode 100755 index 000000000..96c1f27a7 --- /dev/null +++ b/update_bench_incremental.rb @@ -0,0 +1,314 @@ +#!/usr/bin/ruby +require 'fileutils' +Dir.chdir(File.dirname(__FILE__)) +$goblint = File.expand_path("../analyzer/goblint") +$goblint_conf = File.expand_path("../index/incremental.json") +fail "Please run script from goblint dir!" unless File.exist?($goblint) +$vrsn = `#{$goblint} --version` +results = "bench_result" +Dir.mkdir(results) unless Dir.exist?(results) +$testresults = File.expand_path("bench_result") + "/" +bench = "./" +linux = bench + "linux/" + +cmds = {"code2html" => lambda {|f,o| "code2html -l c -n #{f} 2> /dev/null 1> #{o}"}, + "source-highlight" => lambda {|f,o| "source-highlight -n -i #{f} -o #{o}"}, + "pygmentize" => lambda {|f,o| "pygmentize -O full,linenos=1 -o #{o} #{f}"} + } +$highlighter = nil +cmds.each do |name, cmd| + # if `which #{cmd} 2> /dev/null`.empty? then + if ENV['PATH'].split(':').map {|f| File.executable? "#{f}/#{name}"}.include?(true) then + $highlighter = cmd + break + end +end +if $highlighter.nil? then + puts "Warning: No syntax highlighter installed (code2html, source-highlight, pygmentize)." + $highlighter = lambda {|f,o| "cp #{f} #{o}"} +end + +class Project + attr_reader :id, :name, :group, :path, :patches, :size + attr_accessor :url, :params + def initialize(id, name, size, url, group, path, params, patches) + @id = id + @name = name + @size = size + @url = url + @group = group + @path = path + @params = params + @patches = patches + end + def to_html + "#{@id}#{@name}\n" + "#{@size}\n" + end + def to_s + "#{@name}" + end +end + +# class Patch +# attr_reader :name, :path +# attr_accessor :url, +# def initialize(size, url, group, path, params, patches) +# @size = size +# @url = url +# @path = path +# end +# def to_html +# "-#{@name}\n" + "#{@size}\n" +# end +# def to_s +# "#{@name}" +# end +# end + +$projects = [] + +$header = < + Benchmarks on #{`uname -n`.chomp} + + +END +$theresultfile = File.join($testresults, "index.html") + +def print_file_res (f, path) + $analyses.each do |a| + aname = a[0] + outfile = File.basename(path,".c") + ".#{aname}.txt" + if File.exists?($testresults + outfile) then + File.open($testresults + outfile, "r") do |g| + lines = g.readlines + vars, evals = lines.grep(/vars = (\d*).*evals = (\d+)/) { |x| [$1.to_i, $2.to_i] } .first + safely = lines.grep(/[^n]safe:[ ]*([0-9]*)/) { |x| $1.to_i } .first + vulner = lines.grep(/vulnerable:[ ]*([0-9]*)/) { |x| $1.to_i } .first + unsafe = lines.grep(/unsafe:[ ]*([0-9]*)/) { |x| $1.to_i } .first + uncalled = lines.grep(/will never be called/).reject {|x| x =~ /__check/}.size + res = lines.grep(/TIMEOUT\s*(.*) s.*$/) { |x| $1 } + if res == [] then + dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } + cod = lines.grep(/EXITCODE\s*(.*)$/) { |x| $1 } + if cod == [] and not dur == [] then + thenumbers = "#{safely}; " + thenumbers << "#{vulner} + " + thenumbers << "#{unsafe}" + thenumbers << "; #{uncalled}" if uncalled > 0 + f.puts "#{"%.2f" % dur} s / #{vars} vars / #{evals} evals (#{thenumbers})" + else + f.puts "failed (code: #{cod.first.to_s})" + end + else + f.puts "#{res.first.to_s} s (limit)" + end + end + else + f.puts "N/A" + end + end +end + +def print_res (i) + File.open($theresultfile, "w") do |f| + f.puts "" + f.puts $header + f.puts "" + f.puts "

Benchmarking in progress: #{i}/#{$projects.length}

" unless i.nil? + f.puts "" + gname = "" + $projects.each do |p| + if p.group != gname then + gname = p.group + f.puts "" + if $print_desc then + f.puts "" + else + f.puts "" + end + $analyses.each do |a| + aname = a[0] + f.puts "" + end + end + f.puts "" + f.puts p.to_html + print_file_res(f, p.path) + f.puts "" + p.patches.each do |pfile| + f.puts "" + f.puts "\n" + "\n" + print_file_res(f, pfile) + f.puts "" + end + end + f.puts "
#{gname}
#NameDescriptionSize
#NameSize#{aname}
-#{File.basename(pfile)}-
" + f.print "

" + f.puts "Last updated: #{Time.now.strftime("%Y-%m-%d %H:%M:%S %z")}" + f.puts "#{$vrsn}" + f.puts "

" + f.puts "" + f.puts "" + end +end + +#Command line parameters + +$timeout = 900 +$timeout = ARGV[0].to_i unless ARGV[0].nil? +only = ARGV[1] unless ARGV[1].nil? +if only == "group" then + only = nil + thegroup = ARGV[2] +end + +#processing the input file + +skipgrp = [] +file = "index/incremental.txt" +$linuxroot = "https://elixir.bootlin.com/linux/v4.0/source/" + +FileUtils.cp(file,File.join($testresults, "bench.txt")) + +$analyses = [["FromScratch", ""], ["Incremental", "--enable incremental.load"]] +File.open(file, "r") do |f| + id = 0 + while line = f.gets + next if line =~ /^\s*$/ + if line =~ /Group: (.*)/ + gname = $1.chomp + skipgrp << gname if line =~ /SKIP/ + else + name = line.chomp + url = f.gets.chomp + path = f.gets.chomp + params = f.gets.chomp + params = "" if params == "-" + if url == "linux!" then + params = "--enable kernel " + params + url = $linuxroot + path + path = File.expand_path(path, linux) + else + path = File.expand_path(path, bench) + end + size = `wc -l #{path}`.split[0] + " lines" + id += 1 + patches = Dir["#{path.chomp(".c")}*.patch"] + p = Project.new(id,name,size,url,gname,path,params,patches) + $projects << p + end + end +end + +#Process linux results! + +$fileheader = < + + Benchmarks on #{`uname -n`.chomp} + + + +END + + +def proc_linux_res(resultfile, url, filename) + File.open(resultfile, "r") do |f| + File.open(resultfile + ".html", "w") do |o| + o.puts $fileheader + while line = f.gets + line.sub!(/\@(#{filename}:(\d+))/, "@\\1") + if line =~ /race with/ + o.puts '' + line.chop + "" + else + o.puts line + end + end + o.puts "" + o.puts "" + end + end +end + + +$maxlen = $analyses.map { |x| x[0].length }.max + 1 +def analyze_project(p, save) + filepath = p.path + dirname = File.dirname(filepath) + filename = File.basename(filepath) + resname = File.basename(p.name,".c") + Dir.chdir(dirname) + outfiles = $testresults + resname + ".*" + `rm -f #{outfiles}` + if p.url == "generate!" then + system($highlighter.call(p.path, $testresults + resname + ".html")) + p.url = p.name + ".html" + end + puts "Analysing #{resname} (#{p.id}/#{$projects.length})" + first = true + $analyses.each do |a| + aname = a[0] + aparam = a[1] + aparam += " --enable incremental.save " if save && first + print " #{format("%*s", -$maxlen, aname)}" + STDOUT.flush + outfile = $testresults + resname + ".#{aname}.txt" + starttime = Time.now + #Add --sets cilout /dev/null to ignore CIL output. + cmd = "#{$goblint} --set dbg.timeout #{$timeout} #{aparam} #{filename} #{p.params} --enable dbg.uncalled --enable allglobs --enable printstats 1>#{outfile} 2>&1" + system(cmd) + status = $?.exitstatus + endtime = Time.now + File.open(outfile, "a") do |f| + f.puts "\n=== APPENDED BY BENCHMARKING SCRIPT ===" + f.puts "Analysis began: #{starttime}" + f.puts "Analysis ended: #{endtime}" + f.puts "Duration: #{format("%.02f", endtime-starttime)} s" + f.puts "Goblint params: #{cmd}" + f.puts $vrsn + end + if status != 0 then + if status == 124 then + puts "-- Timeout!" + `echo "TIMEOUT #{timeout} s" >> #{outfile}` + else + puts "-- Failed!" + `echo "EXITCODE #{status}" >> #{outfile}` + end + else + puts "-- Done!" + end + print_res p.id + proc_linux_res(outfile, p.url, filename) + end +end + +#analysing the files +gname = "" +$projects.each do |p| + next if skipgrp.member? p.group + next unless thegroup.nil? or p.group == thegroup + next unless only.nil? or p.name == only + if p.group != gname then + gname = p.group + puts gname + end + analyze_project(p, true) + p.patches.each do |pfile| + `patch -b #{p.path} #{pfile}` + pp = Project.new(p.id,pfile,p.size,"generate!",nil,p.path,p.params,nil) + analyze_project(pp, false) + `patch -b -R #{p.path} #{pfile}` + end +end +print_res nil +puts ("Results: " + $theresultfile) From d741a3393bff5109ea489114f85ccf02c65aaf5f Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 4 Oct 2021 09:56:26 +0300 Subject: [PATCH 03/35] Incremental script: almost correct logic now. --- update_bench_incremental.rb | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 96c1f27a7..896ba7e14 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -176,7 +176,7 @@ def print_res (i) FileUtils.cp(file,File.join($testresults, "bench.txt")) -$analyses = [["FromScratch", ""], ["Incremental", "--enable incremental.load"]] +$analyses = [["FromScratch", ""], ["Incremental", "--disable incremental.reluctant"], ["Reluctant", "--enable incremental.reluctant"]] File.open(file, "r") do |f| id = 0 while line = f.gets @@ -258,7 +258,12 @@ def analyze_project(p, save) $analyses.each do |a| aname = a[0] aparam = a[1] - aparam += " --enable incremental.save " if save && first + if first then + aparam += " --enable incremental.save " if save + first = false + else + aparam += " --enable incremental.load " + end print " #{format("%*s", -$maxlen, aname)}" STDOUT.flush outfile = $testresults + resname + ".#{aname}.txt" From 60d1924b61752cedee43e1f49cd304861df0a730 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 4 Oct 2021 10:48:21 +0300 Subject: [PATCH 04/35] Add patches to incremental bench. --- index/incremental.txt | 16 +++++++++++++++- linux/drivers/char/apm-emulation01.patch | 17 +++++++++++++++++ linux/drivers/char/apm-emulation02.patch | 17 +++++++++++++++++ linux/drivers/char/apm-emulation03.patch | 13 +++++++++++++ linux/drivers/char/bsr01.patch | 13 +++++++++++++ linux/drivers/char/dtlk01.patch | 13 +++++++++++++ linux/drivers/char/dtlk02.patch | 12 ++++++++++++ linux/drivers/char/dtlk03.patch | 16 ++++++++++++++++ linux/drivers/char/dtlk04.patch | 13 +++++++++++++ update_bench_incremental.rb | 3 ++- 10 files changed, 131 insertions(+), 2 deletions(-) create mode 100644 linux/drivers/char/apm-emulation01.patch create mode 100644 linux/drivers/char/apm-emulation02.patch create mode 100644 linux/drivers/char/apm-emulation03.patch create mode 100644 linux/drivers/char/bsr01.patch create mode 100644 linux/drivers/char/dtlk01.patch create mode 100644 linux/drivers/char/dtlk02.patch create mode 100644 linux/drivers/char/dtlk03.patch create mode 100644 linux/drivers/char/dtlk04.patch diff --git a/index/incremental.txt b/index/incremental.txt index 3d7562c3a..ed807bab2 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,6 +1,20 @@ Group: Char Drivers +char/apm-emulation.c +linux! +drivers/char/apm-emulation.c +--set otherfun[+] apm_queue_event + char/applicom.c linux! drivers/char/applicom.c -- + +char/bsr.c +linux! +drivers/char/bsr.c +--set exp.extraspecials "['of_find_compatible_node', 'of_get_property', 'of_address_to_resource']" --set otherfun "['bsr_size_show', 'bsr_stride_show', 'bsr_length_show']" + +char/dtlk.c +linux! +drivers/char/dtlk.c +- \ No newline at end of file diff --git a/linux/drivers/char/apm-emulation01.patch b/linux/drivers/char/apm-emulation01.patch new file mode 100644 index 000000000..2a20f575d --- /dev/null +++ b/linux/drivers/char/apm-emulation01.patch @@ -0,0 +1,17 @@ +diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c +index dd9dfa1..324c821 100644 +--- linux/drivers/char/apm-emulation.c ++++ linux/drivers/char/apm-emulation.c +@@ -369,11 +369,11 @@ static int apm_open(struct inode * inode, struct file * filp) + * we might close the device immediately without doing a + * privileged operation -- cevans + */ ++ down_write(&user_list_lock); + as->suser = capable(CAP_SYS_ADMIN); + as->writer = (filp->f_mode & FMODE_WRITE) == FMODE_WRITE; + as->reader = (filp->f_mode & FMODE_READ) == FMODE_READ; + +- down_write(&user_list_lock); + list_add(&as->list, &apm_user_list); + up_write(&user_list_lock); + diff --git a/linux/drivers/char/apm-emulation02.patch b/linux/drivers/char/apm-emulation02.patch new file mode 100644 index 000000000..64f3622f0 --- /dev/null +++ b/linux/drivers/char/apm-emulation02.patch @@ -0,0 +1,17 @@ +diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c +index dd9dfa1..a628a88 100644 +--- linux/drivers/char/apm-emulation.c ++++ linux/drivers/char/apm-emulation.c +@@ -320,10 +320,10 @@ apm_ioctl(struct file *filp, u_int cmd, u_long arg) + as->suspend_result = pm_suspend(PM_SUSPEND_MEM); + } + +- mutex_lock(&state_lock); ++ //mutex_lock(&state_lock); + err = as->suspend_result; + as->suspend_state = SUSPEND_NONE; +- mutex_unlock(&state_lock); ++ //mutex_unlock(&state_lock); + break; + } + diff --git a/linux/drivers/char/apm-emulation03.patch b/linux/drivers/char/apm-emulation03.patch new file mode 100644 index 000000000..2452c8172 --- /dev/null +++ b/linux/drivers/char/apm-emulation03.patch @@ -0,0 +1,13 @@ +diff --git linux/drivers/char/apm-emulation.c linux/drivers/char/apm-emulation.c +index dd9dfa1..f89b8dd 100644 +--- linux/drivers/char/apm-emulation.c ++++ linux/drivers/char/apm-emulation.c +@@ -210,7 +210,7 @@ static ssize_t apm_read(struct file *fp, char __user *buf, size_t count, loff_t + { + struct apm_user *as = fp->private_data; + apm_event_t event; +- int i = count, ret = 0; ++ int i = count, ret = 1; + + if (count < sizeof(apm_event_t)) + return -EINVAL; diff --git a/linux/drivers/char/bsr01.patch b/linux/drivers/char/bsr01.patch new file mode 100644 index 000000000..233c2b337 --- /dev/null +++ b/linux/drivers/char/bsr01.patch @@ -0,0 +1,13 @@ +diff --git linux/drivers/char/bsr.c linux/drivers/char/bsr.c +index a6cef54..6c6efe2 100644 +--- linux/drivers/char/bsr.c ++++ linux/drivers/char/bsr.c +@@ -284,7 +284,7 @@ static int bsr_add_node(struct device_node *bn) + + static int bsr_create_devs(struct device_node *bn) + { +- int ret; ++ int ret = -1; + + while (bn) { + ret = bsr_add_node(bn); diff --git a/linux/drivers/char/dtlk01.patch b/linux/drivers/char/dtlk01.patch new file mode 100644 index 000000000..46eb5535c --- /dev/null +++ b/linux/drivers/char/dtlk01.patch @@ -0,0 +1,13 @@ +diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c +index 65a8d96..86157f6 100644 +--- linux/drivers/char/dtlk.c ++++ linux/drivers/char/dtlk.c +@@ -215,7 +215,7 @@ static ssize_t dtlk_write(struct file *file, const char __user *buf, + + msleep_interruptible(1); + +- if (++retries > 10 * HZ) { /* wait no more than 10 sec ++ if (++retries > 12 * HZ) { /* wait no more than 10 sec + from last write */ + printk("dtlk: write timeout. " + "inb_p(dtlk_port_tts) = 0x%02x\n", diff --git a/linux/drivers/char/dtlk02.patch b/linux/drivers/char/dtlk02.patch new file mode 100644 index 000000000..0b2b0d5ea --- /dev/null +++ b/linux/drivers/char/dtlk02.patch @@ -0,0 +1,12 @@ +diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c +index 65a8d96..9257c7d 100644 +--- linux/drivers/char/dtlk.c ++++ linux/drivers/char/dtlk.c +@@ -261,7 +261,7 @@ static unsigned int dtlk_poll(struct file *file, poll_table * wait) + + static void dtlk_timer_tick(unsigned long data) + { +- TRACE_TEXT(" dtlk_timer_tick"); ++ TRACE_TEXT(" dtlk_timer_tick_tock"); + wake_up_interruptible(&dtlk_process_list); + } diff --git a/linux/drivers/char/dtlk03.patch b/linux/drivers/char/dtlk03.patch new file mode 100644 index 000000000..d7fbebb1d --- /dev/null +++ b/linux/drivers/char/dtlk03.patch @@ -0,0 +1,16 @@ +diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c +index 65a8d96..4a5499e 100644 +--- linux/drivers/char/dtlk.c ++++ linux/drivers/char/dtlk.c +@@ -277,9 +277,9 @@ static long dtlk_ioctl(struct file *file, + switch (cmd) { + + case DTLK_INTERROGATE: +- mutex_lock(&dtlk_mutex); ++ //mutex_lock(&dtlk_mutex); + sp = dtlk_interrogate(); +- mutex_unlock(&dtlk_mutex); ++ //mutex_unlock(&dtlk_mutex); + if (copy_to_user(argp, sp, sizeof(struct dtlk_settings))) + return -EINVAL; + return 0; diff --git a/linux/drivers/char/dtlk04.patch b/linux/drivers/char/dtlk04.patch new file mode 100644 index 000000000..b6af59625 --- /dev/null +++ b/linux/drivers/char/dtlk04.patch @@ -0,0 +1,13 @@ +diff --git linux/drivers/char/dtlk.c linux/drivers/char/dtlk.c +index 65a8d96..deff366 100644 +--- linux/drivers/char/dtlk.c ++++ linux/drivers/char/dtlk.c +@@ -302,7 +302,7 @@ static int dtlk_open(struct inode *inode, struct file *file) + switch (iminor(inode)) { + case DTLK_MINOR: + if (dtlk_busy) +- return -EBUSY; ++ return -EPIPE; + return nonseekable_open(inode, file); + + default: diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 896ba7e14..7226e3bae 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -200,7 +200,7 @@ def print_res (i) size = `wc -l #{path}`.split[0] + " lines" id += 1 patches = Dir["#{path.chomp(".c")}*.patch"] - p = Project.new(id,name,size,url,gname,path,params,patches) + p = Project.new(id,name,size,url,gname,path,params,patches.sort) $projects << p end end @@ -313,6 +313,7 @@ def analyze_project(p, save) pp = Project.new(p.id,pfile,p.size,"generate!",nil,p.path,p.params,nil) analyze_project(pp, false) `patch -b -R #{p.path} #{pfile}` + `rm #{p.path}.orig` end end print_res nil From 3a82d0f5ad0d70802a771be4507edd6e4cba77f6 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 4 Oct 2021 13:13:43 +0300 Subject: [PATCH 05/35] Final tweaks to incremental script. --- index/incremental.txt | 4 ++++ update_bench_incremental.rb | 9 +++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/index/incremental.txt b/index/incremental.txt index ed807bab2..4841e8952 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,3 +1,7 @@ +FromScratch: +Incremental: --disable incremental.reluctant +Reluctant: --enable incremental.reluctant + Group: Char Drivers char/apm-emulation.c diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 7226e3bae..fdb4714df 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -143,7 +143,10 @@ def print_res (i) f.puts "" p.patches.each do |pfile| f.puts "" - f.puts "-#{File.basename(pfile)}\n" + "-\n" + pname = File.basename(pfile) + rpath = $testresults + pname + `cp #{pfile} #{rpath}` + f.puts "-#{pname}\n" + "patched\n" print_file_res(f, pfile) f.puts "" end @@ -176,7 +179,7 @@ def print_res (i) FileUtils.cp(file,File.join($testresults, "bench.txt")) -$analyses = [["FromScratch", ""], ["Incremental", "--disable incremental.reluctant"], ["Reluctant", "--enable incremental.reluctant"]] +$analyses = [] File.open(file, "r") do |f| id = 0 while line = f.gets @@ -184,6 +187,8 @@ def print_res (i) if line =~ /Group: (.*)/ gname = $1.chomp skipgrp << gname if line =~ /SKIP/ + elsif line =~ /(.*): ?(.*)/ + $analyses << [$1,$2] else name = line.chomp url = f.gets.chomp From 6feb3da4d1f0aeaa03128b9c124eddc62475d307 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Tue, 5 Oct 2021 16:27:42 +0000 Subject: [PATCH 06/35] Incremental bench params update. --- index/incremental.txt | 6 +++--- update_bench_incremental.rb | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/index/incremental.txt b/index/incremental.txt index 4841e8952..cd73f20a2 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,6 +1,6 @@ FromScratch: -Incremental: --disable incremental.reluctant -Reluctant: --enable incremental.reluctant +Incremental: --disable incremental.reluctant.on +Reluctant: --enable incremental.reluctant.on Group: Char Drivers @@ -21,4 +21,4 @@ drivers/char/bsr.c char/dtlk.c linux! drivers/char/dtlk.c -- \ No newline at end of file +- diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index fdb4714df..e2db981f9 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -274,7 +274,7 @@ def analyze_project(p, save) outfile = $testresults + resname + ".#{aname}.txt" starttime = Time.now #Add --sets cilout /dev/null to ignore CIL output. - cmd = "#{$goblint} --set dbg.timeout #{$timeout} #{aparam} #{filename} #{p.params} --enable dbg.uncalled --enable allglobs --enable printstats 1>#{outfile} 2>&1" + cmd = "#{$goblint} -v --set dbg.timeout #{$timeout} #{aparam} #{filename} #{p.params} --enable dbg.uncalled --enable allglobs --enable printstats 1>#{outfile} 2>&1" system(cmd) status = $?.exitstatus endtime = Time.now From 1a1422ec8454fbbdefb39632591ecb2245b2b5f0 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Thu, 14 Oct 2021 19:21:19 +0300 Subject: [PATCH 07/35] Update README. --- README.md | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index f00f14f3e..caee6965e 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,23 @@ # Goblint benchmark suite -[![Gitter](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/goblint/bench?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge) +This contains the suite of benchmarks we currently use to evaluate Goblint. To run the benchmarks, make sure this repository is checked out in a directory with the same parent as the Goblint analyzer. -This contains the suite of benchmarks we currently use to evaluate Goblint. To run the benchmarks, make sure this repository is checked out in a directory with the same parent as the Goblint analyzer. Then, you can execute the script `./update_bench.rb` and view the results in bench_result/index.html. The kernel benchmarks rely on linux headers in the analyzer's directory (installed by executing `make headers`). +## Basic Benchmarks + +Execute the script `./update_bench.rb` and view the results in bench_result/index.html. The kernel benchmarks rely on linux headers in the analyzer's directory (installed by executing `make headers`). + +The benchmarks descriptions are assumed to be in a file called `bench.txt`. If this is absent it is symlinked to `index/dd.txt`. The idea was that one should locally replace with a hard copy without modifying the default descriptions. + + +## Incremental Benchmarks + +1. Edit the file `index/incremental.txt` to set the parameters. Do not add the incremental save and load commands since these are added by some ugly mechanism. (Be happy I'm keeping my hands away from goblint...) +2. Run `./update_bench_incremental.rb` + +Add patches by changing some benchmark and doing, e.g., `git diff --no-prefix dtlk.c > dtlk04.patch`, and then of course restore the file. + +## Other Benchmarking scripts + +- [parallel-run.sh](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/parallel-run.sh) to run the config in that script in parallel and log each program +- [csv-results.ml](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/csv-results.ml) to extract some numbers from each log and print a csv of it +- [precision.sh](https://github.com/goblint/bench/blob/2d8bc2c8cb2cd6499733c535b868643f45bcae49/precision.sh) to let goblint compare two variants for each program and write the result to a .precision file \ No newline at end of file From 8418b3332bfc4f70fcbf938544245206d930e757 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Thu, 14 Oct 2021 20:09:56 +0300 Subject: [PATCH 08/35] Add a few posix app diffs. --- index/incremental.txt | 13 +++++++++++++ pthread/aget_comb01.patch | 14 ++++++++++++++ pthread/aget_comb02.patch | 13 +++++++++++++ pthread/knot_comb01.patch | 13 +++++++++++++ pthread/knot_comb02.patch | 13 +++++++++++++ 5 files changed, 66 insertions(+) create mode 100644 pthread/aget_comb01.patch create mode 100644 pthread/aget_comb02.patch create mode 100644 pthread/knot_comb01.patch create mode 100644 pthread/knot_comb02.patch diff --git a/index/incremental.txt b/index/incremental.txt index cd73f20a2..e820f4dc0 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -2,6 +2,19 @@ FromScratch: Incremental: --disable incremental.reluctant.on Reluctant: --enable incremental.reluctant.on +Group: POSIX Apps + +aget_comb +Multithreaded wget +pthread/aget_comb.c +- + +knot_comb +Multithreaded web server +pthread/knot_comb.c +- + + Group: Char Drivers char/apm-emulation.c diff --git a/pthread/aget_comb01.patch b/pthread/aget_comb01.patch new file mode 100644 index 000000000..19d8efdb0 --- /dev/null +++ b/pthread/aget_comb01.patch @@ -0,0 +1,14 @@ +diff --git pthread/aget_comb.c pthread/aget_comb.c +index c7d24b4..d505c6e 100644 +--- pthread/aget_comb.c ++++ pthread/aget_comb.c +@@ -1017,7 +1017,8 @@ void *signal_waiter(void *arg ) + while (1) { + sigwait((sigset_t const * __restrict )(& signal_set), (int * __restrict )(& signal___0)); + switch (signal___0) { +- case 2: ++ case 2: ++ case 3: + sigint_handler(); + break; + case 14: diff --git a/pthread/aget_comb02.patch b/pthread/aget_comb02.patch new file mode 100644 index 000000000..5bbac0cdb --- /dev/null +++ b/pthread/aget_comb02.patch @@ -0,0 +1,13 @@ +diff --git pthread/aget_comb.c pthread/aget_comb.c +index c7d24b4..bd0a90a 100644 +--- pthread/aget_comb.c ++++ pthread/aget_comb.c +@@ -1094,7 +1094,7 @@ void *http_get(void *arg ) + tmp = calloc(8192U, sizeof(char )); + rbuf = (char *)tmp; + sd = socket(2, 1, 0); +- if (sd == -1) { ++ if (sd <= -1) { + tmp___0 = __errno_location(); + tmp___1 = strerror(*tmp___0); + Log((char *)" socket creation failed: %s", tid, tmp___1); diff --git a/pthread/knot_comb01.patch b/pthread/knot_comb01.patch new file mode 100644 index 000000000..cf6753845 --- /dev/null +++ b/pthread/knot_comb01.patch @@ -0,0 +1,13 @@ +diff --git pthread/knot_comb.c pthread/knot_comb.c +index ad59515..1a65063 100644 +--- pthread/knot_comb.c ++++ pthread/knot_comb.c +@@ -1106,7 +1106,7 @@ void accept_loop(int id , int s ) + if (! attr_init_done) { + pthread_attr_init(& attr); + rv = pthread_attr_setdetachstate(& attr, 1); +- if (! (rv == 0)) { ++ if (rv != 0) { + assert_failed((char *)"knot.c", 472U, "accept_loop", (char *)"rv == 0"); + } + attr_init_done = 1; diff --git a/pthread/knot_comb02.patch b/pthread/knot_comb02.patch new file mode 100644 index 000000000..2a52ce8a2 --- /dev/null +++ b/pthread/knot_comb02.patch @@ -0,0 +1,13 @@ +diff --git pthread/knot_comb.c pthread/knot_comb.c +index ad59515..de401be 100644 +--- pthread/knot_comb.c ++++ pthread/knot_comb.c +@@ -709,7 +709,7 @@ char *input_get_line(input_state *state ) + empty = & state->buf[state->valid]; + tmp = read(state->socket, (void *)empty, (unsigned int )(511 - state->valid)); + n = tmp; +- if (n <= 0) { ++ if (n == 0) { + result = (char *)((void *)0); + done = 1; + } else { From 57c0821b0750b64d13c50ad6f67ad2a3ef88daeb Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Thu, 14 Oct 2021 20:11:59 +0300 Subject: [PATCH 09/35] Make links relative. --- update_bench_incremental.rb | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index e2db981f9..72b67b746 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -144,9 +144,8 @@ def print_res (i) p.patches.each do |pfile| f.puts "" pname = File.basename(pfile) - rpath = $testresults + pname `cp #{pfile} #{rpath}` - f.puts "-#{pname}\n" + "patched\n" + f.puts "-#{pname}\n" + "patched\n" print_file_res(f, pfile) f.puts "" end @@ -254,7 +253,7 @@ def analyze_project(p, save) Dir.chdir(dirname) outfiles = $testresults + resname + ".*" `rm -f #{outfiles}` - if p.url == "generate!" then + if not p.url.start_with? "http" then system($highlighter.call(p.path, $testresults + resname + ".html")) p.url = p.name + ".html" end From 38f1e56366255e11e2f033297aaf42afa454f4b8 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Thu, 14 Oct 2021 20:21:04 +0300 Subject: [PATCH 10/35] Fix rushed edit in previous commit. --- update_bench_incremental.rb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 72b67b746..6b6ae78dc 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -144,7 +144,7 @@ def print_res (i) p.patches.each do |pfile| f.puts "" pname = File.basename(pfile) - `cp #{pfile} #{rpath}` + `cp #{pfile} #{$testresults + pname}` f.puts "-#{pname}\n" + "patched\n" print_file_res(f, pfile) f.puts "" From 507d300682b3776d9febd0a4ac55169fd64f431a Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 11:15:04 +0300 Subject: [PATCH 11/35] Add some restar params to the incremental suit. --- index/incremental.txt | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/index/incremental.txt b/index/incremental.txt index e820f4dc0..8c6f9dc91 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,6 +1,9 @@ -FromScratch: -Incremental: --disable incremental.reluctant.on -Reluctant: --enable incremental.reluctant.on +FromScratch: --enable incremental.restart.sided.enabled +Incremental: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on +Reluctant: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on +RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on +RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --enable incremental.reluctant.on + Group: POSIX Apps From 9965c89fc899827381892dd05f3b8cd6f84594ba Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 12:20:25 +0300 Subject: [PATCH 12/35] Add precision comparison to incremental script. --- update_bench_incremental.rb | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 6b6ae78dc..f5491348b 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -10,6 +10,7 @@ $testresults = File.expand_path("bench_result") + "/" bench = "./" linux = bench + "linux/" +$compare = true cmds = {"code2html" => lambda {|f,o| "code2html -l c -n #{f} 2> /dev/null 1> #{o}"}, "source-highlight" => lambda {|f,o| "source-highlight -n -i #{f} -o #{o}"}, @@ -101,6 +102,7 @@ def print_file_res (f, path) thenumbers << "#{vulner} + " thenumbers << "#{unsafe}" thenumbers << "; #{uncalled}" if uncalled > 0 + thenumbers << " -- compare!" if $compare f.puts "#{"%.2f" % dur} s / #{vars} vars / #{evals} evals (#{thenumbers})" else f.puts "failed (code: #{cod.first.to_s})" @@ -264,9 +266,11 @@ def analyze_project(p, save) aparam = a[1] if first then aparam += " --enable incremental.save " if save + aparam += " --set save_run original " if $compare first = false else aparam += " --enable incremental.load " + aparam += " --set save_run increment " if $compare end print " #{format("%*s", -$maxlen, aname)}" STDOUT.flush @@ -294,6 +298,7 @@ def analyze_project(p, save) `echo "EXITCODE #{status}" >> #{outfile}` end else + system("#{$goblint} --enable kernel original/config.json --compare_runs original increment #{filename} > #{outfile}.compare.txt") if $compare and not first puts "-- Done!" end print_res p.id From 559098422dc4690c75a2055936db64fbaf8cbd6b Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 14:41:28 +0300 Subject: [PATCH 13/35] Some cleanup; remove kernel benches for now. --- index/incremental.txt | 22 ---------------------- update_bench_incremental.rb | 25 +++++++++++++++++-------- 2 files changed, 17 insertions(+), 30 deletions(-) diff --git a/index/incremental.txt b/index/incremental.txt index 8c6f9dc91..69032452d 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -16,25 +16,3 @@ knot_comb Multithreaded web server pthread/knot_comb.c - - - -Group: Char Drivers - -char/apm-emulation.c -linux! -drivers/char/apm-emulation.c ---set otherfun[+] apm_queue_event - -char/applicom.c -linux! -drivers/char/applicom.c - -char/bsr.c -linux! -drivers/char/bsr.c ---set exp.extraspecials "['of_find_compatible_node', 'of_get_property', 'of_address_to_resource']" --set otherfun "['bsr_size_show', 'bsr_stride_show', 'bsr_length_show']" - -char/dtlk.c -linux! -drivers/char/dtlk.c -- diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index f5491348b..9f54555de 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -82,6 +82,7 @@ def to_s $theresultfile = File.join($testresults, "index.html") def print_file_res (f, path) + first = true $analyses.each do |a| aname = a[0] outfile = File.basename(path,".c") + ".#{aname}.txt" @@ -98,12 +99,18 @@ def print_file_res (f, path) dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } cod = lines.grep(/EXITCODE\s*(.*)$/) { |x| $1 } if cod == [] and not dur == [] then - thenumbers = "#{safely}; " - thenumbers << "#{vulner} + " - thenumbers << "#{unsafe}" - thenumbers << "; #{uncalled}" if uncalled > 0 - thenumbers << " -- compare!" if $compare - f.puts "#{"%.2f" % dur} s / #{vars} vars / #{evals} evals (#{thenumbers})" + if $compare then + compfile = "#{outfile}.compare.txt" + thenumbers = "" + thenumbers = "compare" unless first + else + thenumbers = "#{safely}; " + thenumbers << "#{vulner} + " + thenumbers << "#{unsafe}" + thenumbers << "; #{uncalled}" if uncalled > 0 + end + thenumbers = " (#{thenumbers})" if thenumbers != "" + f.puts "#{"%.2f" % dur} s / #{vars} vars / #{evals} evals#{thenumbers}" else f.puts "failed (code: #{cod.first.to_s})" end @@ -114,6 +121,7 @@ def print_file_res (f, path) else f.puts "N/A" end + first = false end end @@ -267,7 +275,6 @@ def analyze_project(p, save) if first then aparam += " --enable incremental.save " if save aparam += " --set save_run original " if $compare - first = false else aparam += " --enable incremental.load " aparam += " --set save_run increment " if $compare @@ -298,12 +305,14 @@ def analyze_project(p, save) `echo "EXITCODE #{status}" >> #{outfile}` end else - system("#{$goblint} --enable kernel original/config.json --compare_runs original increment #{filename} > #{outfile}.compare.txt") if $compare and not first + system("#{$goblint} original/config.json --compare_runs original increment #{filename} > #{outfile}.compare.txt") if $compare and not first puts "-- Done!" end + first = false print_res p.id proc_linux_res(outfile, p.url, filename) end + `rm -rf original increment` if $compare end #analysing the files From ece783b89d6d5c8f6ecfbe92fcf792af3dce6a5d Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 15:11:58 +0300 Subject: [PATCH 14/35] Bench scripts regex tweaks. --- update_bench.rb | 4 ++-- update_bench_incremental.rb | 6 +++--- update_bench_traces.rb | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/update_bench.rb b/update_bench.rb index 1a3a765de..22dfa4d5c 100755 --- a/update_bench.rb +++ b/update_bench.rb @@ -95,10 +95,10 @@ def print_res (i) vulner = lines.grep(/vulnerable:[ ]*([0-9]*)/) { |x| $1.to_i } .first unsafe = lines.grep(/unsafe:[ ]*([0-9]*)/) { |x| $1.to_i } .first uncalled = lines.grep(/will never be called/).reject {|x| x =~ /__check/}.size - res = lines.grep(/TIMEOUT\s*(.*) s.*$/) { |x| $1 } + res = lines.grep(/^TIMEOUT\s*(.*) s.*$/) { |x| $1 } if res == [] then dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } - cod = lines.grep(/EXITCODE\s*(.*)$/) { |x| $1 } + cod = lines.grep(/^EXITCODE\s*(.*)$/) { |x| $1 } if cod == [] and not dur == [] then thenumbers = "#{safely}; " thenumbers << "#{vulner} + " diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 9f54555de..56df1606b 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -94,10 +94,10 @@ def print_file_res (f, path) vulner = lines.grep(/vulnerable:[ ]*([0-9]*)/) { |x| $1.to_i } .first unsafe = lines.grep(/unsafe:[ ]*([0-9]*)/) { |x| $1.to_i } .first uncalled = lines.grep(/will never be called/).reject {|x| x =~ /__check/}.size - res = lines.grep(/TIMEOUT\s*(.*) s.*$/) { |x| $1 } + res = lines.grep(/^TIMEOUT\s*(.*) s.*$/) { |x| $1 } if res == [] then dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } - cod = lines.grep(/EXITCODE\s*(.*)$/) { |x| $1 } + cod = lines.grep(/^EXITCODE\s*(.*)$/) { |x| $1 } if cod == [] and not dur == [] then if $compare then compfile = "#{outfile}.compare.txt" @@ -299,7 +299,7 @@ def analyze_project(p, save) if status != 0 then if status == 124 then puts "-- Timeout!" - `echo "TIMEOUT #{timeout} s" >> #{outfile}` + `echo "TIMEOUT #{$timeout} s" >> #{outfile}` else puts "-- Failed!" `echo "EXITCODE #{status}" >> #{outfile}` diff --git a/update_bench_traces.rb b/update_bench_traces.rb index eef58bc3c..a050867a1 100755 --- a/update_bench_traces.rb +++ b/update_bench_traces.rb @@ -101,10 +101,10 @@ def print_res (i) live = lines.grep(/Live lines: ([0-9]*)/) { |x| $1.to_i } .first dead = lines.grep(/Found dead code on ([0-9]*) line/) { |x| $1.to_i } .first total = lines.grep(/Total lines \(logical LoC\): ([0-9]*)/) { |x| $1.to_i } .first - res = lines.grep(/TIMEOUT\s*(\d*) s.*$/) { |x| $1 } + res = lines.grep(/^TIMEOUT\s*(\d*) s.*$/) { |x| $1 } if res == [] then dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } - cod = lines.grep(/EXITCODE\s*(.*)$/) { |x| $1 } + cod = lines.grep(/^EXITCODE\s*(.*)$/) { |x| $1 } if cod == [] and not dur == [] then # thenumbers = "#{safely}; " # thenumbers << "#{vulner} + " From ee4b02136725c20ddc1551e5c30090dcabf94d6b Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 15:40:12 +0300 Subject: [PATCH 15/35] Add smtprc and ypbind. --- index/incremental.txt | 10 ++++++++++ pthread/smtprc_comb01.patch | 13 +++++++++++++ pthread/smtprc_comb02.patch | 13 +++++++++++++ pthread/ypbind_comb01.patch | 13 +++++++++++++ pthread/ypbind_comb02.patch | 13 +++++++++++++ 5 files changed, 62 insertions(+) create mode 100644 pthread/smtprc_comb01.patch create mode 100644 pthread/smtprc_comb02.patch create mode 100644 pthread/ypbind_comb01.patch create mode 100644 pthread/ypbind_comb02.patch diff --git a/index/incremental.txt b/index/incremental.txt index 69032452d..620286503 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -16,3 +16,13 @@ knot_comb Multithreaded web server pthread/knot_comb.c - + +ypbind_comb +Linux NIS daemon: ypbind-mt +pthread/ypbind_comb.c +- + +smtprc_comb +SMTP Open Relay Checker +pthread/smtprc_comb.c +- diff --git a/pthread/smtprc_comb01.patch b/pthread/smtprc_comb01.patch new file mode 100644 index 000000000..cbc963760 --- /dev/null +++ b/pthread/smtprc_comb01.patch @@ -0,0 +1,13 @@ +diff --git pthread/smtprc_comb.c pthread/smtprc_comb.c +index 8aaffec..7c8c514 100644 +--- pthread/smtprc_comb.c ++++ pthread/smtprc_comb.c +@@ -3789,7 +3789,7 @@ void print_link(FILE *fd , char *link___0 , char *text , char *color ) + { + x = 0; + while (1) { +- if (x < 20) { ++ if (x < 16) { + tmp = strlen((char const *)text); + if (! ((size_t )x < tmp)) { + break; diff --git a/pthread/smtprc_comb02.patch b/pthread/smtprc_comb02.patch new file mode 100644 index 000000000..2355da49a --- /dev/null +++ b/pthread/smtprc_comb02.patch @@ -0,0 +1,13 @@ +diff --git pthread/smtprc_comb.c pthread/smtprc_comb.c +index 8aaffec..6e4480a 100644 +--- pthread/smtprc_comb.c ++++ pthread/smtprc_comb.c +@@ -4150,7 +4150,7 @@ int relay_check(int *sockfd , long cur_host ) + strncat((char * __restrict )(checking), (char const * __restrict )" !", + 8192U); + printf((char const * __restrict )"%s\n", checking); +- return (-1); ++ return (-2); + } + rule___0 ++; + } diff --git a/pthread/ypbind_comb01.patch b/pthread/ypbind_comb01.patch new file mode 100644 index 000000000..345bbfa0a --- /dev/null +++ b/pthread/ypbind_comb01.patch @@ -0,0 +1,13 @@ +diff --git pthread/ypbind_comb.c pthread/ypbind_comb.c +index 255923b..444fe25 100644 +--- pthread/ypbind_comb.c ++++ pthread/ypbind_comb.c +@@ -4583,7 +4583,7 @@ int pthread_rdwr_wunlock_np(pthread_rdwr_t *rdwrp ) ; + #line 84 "serv_list.c" + static struct binding *domainlist = (struct binding *)((void *)0); + #line 85 "serv_list.c" +-static int max_domains = 0; ++static int max_domains = 4; + #line 86 "serv_list.c" + static struct __anonstruct_pthread_rdwr_t_72 domainlock = {0, 0, 0, {{0, 0U, 0, 0, 0U, {0}}}, {{0, 0U, 0ULL, 0ULL, 0ULL, (void *)0, 0U, 0U}}}; + #line 87 "serv_list.c" diff --git a/pthread/ypbind_comb02.patch b/pthread/ypbind_comb02.patch new file mode 100644 index 000000000..a1bdffa16 --- /dev/null +++ b/pthread/ypbind_comb02.patch @@ -0,0 +1,13 @@ +diff --git pthread/ypbind_comb.c pthread/ypbind_comb.c +index 255923b..e4d7179 100644 +--- pthread/ypbind_comb.c ++++ pthread/ypbind_comb.c +@@ -5010,7 +5010,7 @@ void find_domain(char const *domain___0 , ypbind_resp *result ) + #line 272 + if ((domainlist + i)->active == -2) { + #line 274 +- result->ypbind_status = 1; ++ result->ypbind_status = -1; + #line 275 + memcpy((void * __restrict )(& result->ypbind_resp_u.ypbind_bindinfo.ypbind_binding_addr), + (void const * __restrict )(& (domainlist + i)->ypset.addr), sizeof(struct in_addr )); From adfacbdb164e2fff925cfdc9288c1cbef59f26bd Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 18:59:03 +0300 Subject: [PATCH 16/35] Enable solverdiff --- update_bench_incremental.rb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 56df1606b..a5ed3631a 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -305,7 +305,7 @@ def analyze_project(p, save) `echo "EXITCODE #{status}" >> #{outfile}` end else - system("#{$goblint} original/config.json --compare_runs original increment #{filename} > #{outfile}.compare.txt") if $compare and not first + system("#{$goblint} original/config.json --enable solverdiffs --compare_runs original increment #{filename} > #{outfile}.compare.txt") if $compare and not first puts "-- Done!" end first = false From d693e6057649eaf65007a8f297f6b8c824b93f6f Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 19:07:14 +0300 Subject: [PATCH 17/35] Incremental suite: disable reluctant for restarts. --- index/incremental.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/index/incremental.txt b/index/incremental.txt index 620286503..ac05cb53e 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,8 +1,8 @@ FromScratch: --enable incremental.restart.sided.enabled Incremental: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on Reluctant: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on -RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on -RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --enable incremental.reluctant.on +RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on +RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --disable incremental.reluctant.on Group: POSIX Apps From 17a43aca5874ab2318d9543a6d6c3f0e4fece597 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Mon, 18 Oct 2021 19:07:22 +0300 Subject: [PATCH 18/35] Add one more patch. --- pthread/ypbind_comb03.patch | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 pthread/ypbind_comb03.patch diff --git a/pthread/ypbind_comb03.patch b/pthread/ypbind_comb03.patch new file mode 100644 index 000000000..20c3646ea --- /dev/null +++ b/pthread/ypbind_comb03.patch @@ -0,0 +1,25 @@ +diff --git pthread/ypbind_comb.c pthread/ypbind_comb.c +index 255923b..4be088a 100644 +--- pthread/ypbind_comb.c ++++ pthread/ypbind_comb.c +@@ -5628,16 +5628,19 @@ static bool_t eachresult(bool_t *out , struct sockaddr_in *addr ) + timeout___0.tv_sec = 1L; + #line 595 + timeout___0.tv_usec = 0L; +-#line 596 ++#line 596 ++ pthread_mutex_lock(& search_lock); + in_use->client_handle = clntudp_create(addr, 100004UL, 2UL, timeout___0, & sock); + #line 599 + if ((unsigned int )in_use->client_handle == (unsigned int )((void *)0)) { + #line 600 ++ pthread_mutex_unlock(& search_lock); + return (0); + } + #line 602 + in_use->active = 0; + #line 604 ++ pthread_mutex_unlock(& search_lock); + return (1); + } else { + #line 608 From c8b3b9b60b5e2b8db239619f428995c4f0f35c61 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Tue, 19 Oct 2021 17:38:55 +0000 Subject: [PATCH 19/35] Separate interactive/incremental configs. --- index/incremental.txt | 8 +++----- index/interactive.txt | 28 ++++++++++++++++++++++++++++ 2 files changed, 31 insertions(+), 5 deletions(-) create mode 100644 index/interactive.txt diff --git a/index/incremental.txt b/index/incremental.txt index ac05cb53e..9e1271e49 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -1,8 +1,6 @@ -FromScratch: --enable incremental.restart.sided.enabled -Incremental: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on -Reluctant: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on -RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on -RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --disable incremental.reluctant.on +FromScratch: +Incremental: --disable incremental.reluctant.on +Reluctant: --enable incremental.reluctant.on Group: POSIX Apps diff --git a/index/interactive.txt b/index/interactive.txt new file mode 100644 index 000000000..ac05cb53e --- /dev/null +++ b/index/interactive.txt @@ -0,0 +1,28 @@ +FromScratch: --enable incremental.restart.sided.enabled +Incremental: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on +Reluctant: --disable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --enable incremental.reluctant.on +RestartGlob: --enable incremental.restart.sided.enabled --disable incremental.restart.wpoint.enabled --disable incremental.reluctant.on +RestartLocal: --enable incremental.restart.sided.enabled --enable incremental.restart.wpoint.enabled --disable incremental.reluctant.on + + +Group: POSIX Apps + +aget_comb +Multithreaded wget +pthread/aget_comb.c +- + +knot_comb +Multithreaded web server +pthread/knot_comb.c +- + +ypbind_comb +Linux NIS daemon: ypbind-mt +pthread/ypbind_comb.c +- + +smtprc_comb +SMTP Open Relay Checker +pthread/smtprc_comb.c +- From 63d068560a0c71d0e7d93e0fc693b2ccbf4060ac Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Tue, 19 Oct 2021 17:41:37 +0000 Subject: [PATCH 20/35] Let from-scratch rename the ids. --- update_bench_incremental.rb | 1 + 1 file changed, 1 insertion(+) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index a5ed3631a..0712f9ce6 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -274,6 +274,7 @@ def analyze_project(p, save) aparam = a[1] if first then aparam += " --enable incremental.save " if save + aparam += " --enable incremental.only-rename " if not save aparam += " --set save_run original " if $compare else aparam += " --enable incremental.load " From 97867673c8c570782528c509eb3b77315229705c Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Tue, 19 Oct 2021 21:51:31 +0300 Subject: [PATCH 21/35] Add restart-needing example. --- index/incremental.txt | 5 +++++ pthread/example.c | 42 +++++++++++++++++++++++++++++++++++++++++ pthread/example01.patch | 4 ++++ 3 files changed, 51 insertions(+) create mode 100644 pthread/example.c create mode 100644 pthread/example01.patch diff --git a/index/incremental.txt b/index/incremental.txt index 9e1271e49..03d8dbd29 100644 --- a/index/incremental.txt +++ b/index/incremental.txt @@ -5,6 +5,11 @@ Reluctant: --enable incremental.reluctant.on Group: POSIX Apps +example +Restarting example +pthread/example.c +- + aget_comb Multithreaded wget pthread/aget_comb.c diff --git a/pthread/example.c b/pthread/example.c new file mode 100644 index 000000000..735728db0 --- /dev/null +++ b/pthread/example.c @@ -0,0 +1,42 @@ +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +int (*fp)() = NULL; + +int bad() { + return -1; +} + +int good() { + return 1; +} + +void* consumer(void *arg) { + int res = 0; + pthread_mutex_lock(&mutex); + if (fp != NULL) { + res = fp(); + } + pthread_mutex_unlock(&mutex); + assert(res >= 0); + res = 0; + // change absorbed + return NULL; +} + +void* producer(void *arg) { + int res = 0; + pthread_mutex_lock(&mutex); + fp = bad; + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main() { + pthread_t id1 = NULL, id2 = NULL; + pthread_create(&id1, NULL, consumer, NULL); + pthread_create(&id2, NULL, producer, NULL); + return 0; +} \ No newline at end of file diff --git a/pthread/example01.patch b/pthread/example01.patch new file mode 100644 index 000000000..21c08b591 --- /dev/null +++ b/pthread/example01.patch @@ -0,0 +1,4 @@ +32c32 +< fp = bad; +--- +> fp = good; From 2b7e1f040451c843d694d39b7f0c1e710c60b45b Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Wed, 20 Oct 2021 18:50:10 +0300 Subject: [PATCH 22/35] Show comparison in table. --- update_bench_incremental.rb | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index 0712f9ce6..d8ecd479f 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -90,20 +90,27 @@ def print_file_res (f, path) File.open($testresults + outfile, "r") do |g| lines = g.readlines vars, evals = lines.grep(/vars = (\d*).*evals = (\d+)/) { |x| [$1.to_i, $2.to_i] } .first - safely = lines.grep(/[^n]safe:[ ]*([0-9]*)/) { |x| $1.to_i } .first - vulner = lines.grep(/vulnerable:[ ]*([0-9]*)/) { |x| $1.to_i } .first - unsafe = lines.grep(/unsafe:[ ]*([0-9]*)/) { |x| $1.to_i } .first - uncalled = lines.grep(/will never be called/).reject {|x| x =~ /__check/}.size res = lines.grep(/^TIMEOUT\s*(.*) s.*$/) { |x| $1 } if res == [] then dur = lines.grep(/^Duration: (.*) s/) { |x| $1 } cod = lines.grep(/^EXITCODE\s*(.*)$/) { |x| $1 } if cod == [] and not dur == [] then if $compare then - compfile = "#{outfile}.compare.txt" - thenumbers = "" - thenumbers = "compare" unless first - else + if not first then + compfile = "#{outfile}.compare.txt" + complines = File.readlines($testresults + compfile) + msg = "" + msg << "⊑" if complines.grep(/left = [1-9]/).any? + msg << "≸" if complines.grep(/incomparable = [1-9]/).any? + msg << "⊒" if complines.grep(/\#{msg}" + end + else + safely = lines.grep(/[^n]safe:[ ]*([0-9]*)/) { |x| $1.to_i } .first + vulner = lines.grep(/vulnerable:[ ]*([0-9]*)/) { |x| $1.to_i } .first + unsafe = lines.grep(/unsafe:[ ]*([0-9]*)/) { |x| $1.to_i } .first + uncalled = lines.grep(/will never be called/).reject {|x| x =~ /__check/}.size thenumbers = "#{safely}; " thenumbers << "#{vulner} + " thenumbers << "#{unsafe}" From 54ff40234b10e69a82f01056cc2df844f59aee10 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Wed, 20 Oct 2021 19:06:12 +0300 Subject: [PATCH 23/35] Read and show conf file (with intervals now). --- index/incremental.json | 7 +++++++ update_bench_incremental.rb | 6 ++++-- 2 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 index/incremental.json diff --git a/index/incremental.json b/index/incremental.json new file mode 100644 index 000000000..2e8a828f0 --- /dev/null +++ b/index/incremental.json @@ -0,0 +1,7 @@ +{ + "ana": { + "int": { + "interval": true + } + } +} diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index d8ecd479f..e991151c5 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -2,7 +2,7 @@ require 'fileutils' Dir.chdir(File.dirname(__FILE__)) $goblint = File.expand_path("../analyzer/goblint") -$goblint_conf = File.expand_path("../index/incremental.json") +$goblint_conf = File.expand_path("index/incremental.json") fail "Please run script from goblint dir!" unless File.exist?($goblint) $vrsn = `#{$goblint} --version` results = "bench_result" @@ -171,6 +171,7 @@ def print_res (i) f.print "

" f.puts "Last updated: #{Time.now.strftime("%Y-%m-%d %H:%M:%S %z")}" f.puts "#{$vrsn}" + f.puts "Goblint base configuration: conf.json." f.puts "

" f.puts "" f.puts "" @@ -292,7 +293,7 @@ def analyze_project(p, save) outfile = $testresults + resname + ".#{aname}.txt" starttime = Time.now #Add --sets cilout /dev/null to ignore CIL output. - cmd = "#{$goblint} -v --set dbg.timeout #{$timeout} #{aparam} #{filename} #{p.params} --enable dbg.uncalled --enable allglobs --enable printstats 1>#{outfile} 2>&1" + cmd = "#{$goblint} --conf #{$goblint_conf} -v --set dbg.timeout #{$timeout} #{aparam} #{filename} #{p.params} --enable dbg.uncalled --enable allglobs --enable printstats 1>#{outfile} 2>&1" system(cmd) status = $?.exitstatus endtime = Time.now @@ -325,6 +326,7 @@ def analyze_project(p, save) #analysing the files gname = "" +system("#{$goblint} --conf #{$goblint_conf} --writeconf #{$testresults}/conf.json") $projects.each do |p| next if skipgrp.member? p.group next unless thegroup.nil? or p.group == thegroup From 33e24d04084cc2b9ea5a21b78251c7cc4f5073ff Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Fri, 22 Oct 2021 14:39:49 +0000 Subject: [PATCH 24/35] Mostly html fixes. --- update_bench_incremental.rb | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/update_bench_incremental.rb b/update_bench_incremental.rb index e991151c5..699b95478 100755 --- a/update_bench_incremental.rb +++ b/update_bench_incremental.rb @@ -69,9 +69,12 @@ def to_s $projects = [] $header = < + + Benchmarks on #{`uname -n`.chomp} -