From df86ea52ab4660fd3cb7b7f39d90bbf1d20832d4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 12 Sep 2019 18:58:04 +0200
Subject: [PATCH] [kernel] avoid generating ill-formed asm contracts in
presence of void ptrs
When a `void *` lval is referenced in an asm directive, use its conversion
as `char *` in the contract to obtain well-formed `assigns` clauses.
Fixes #609
---
src/kernel_internals/typing/asm_contracts.ml | 6 ++++++
tests/syntax/asm_with_contracts.i | 7 +++++++
.../oracle/asm_with_contracts.res.oracle | 19 +++++++++++++++++++
3 files changed, 32 insertions(+)
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 74ea3ab799e..b7b7c48bf13 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -79,6 +79,12 @@ let access_ptr_elts ~loc tlv =
let range = Logic_const.trange ~loc (None, None) in
let basetype = Cil.typeOfTermLval tlv in
let base = Logic_const.term ~loc (TLval tlv) basetype in
+ let base, basetype =
+ if Logic_utils.isLogicVoidPointerType basetype then begin
+ let typ = Ctype Cil.charPtrType in
+ Logic_const.term ~loc (TCastE(Cil.charPtrType,base)) typ, typ
+ end else base, basetype
+ in
let offset = Logic_const.term ~loc (TBinOp (PlusPI, base, range)) basetype in
TMem offset, TNoOffset
diff --git a/tests/syntax/asm_with_contracts.i b/tests/syntax/asm_with_contracts.i
index 215f8be829c..4631049bab3 100644
--- a/tests/syntax/asm_with_contracts.i
+++ b/tests/syntax/asm_with_contracts.i
@@ -22,3 +22,10 @@ int f(int z) {
return x;
}
+
+static __inline void
+insw (unsigned short int __port, void *__addr, unsigned long int __count)
+{
+ __asm__ __volatile__ ("cld ; rep ; insw":"=D" (__addr), "=c" (__count)
+ :"d" (__port), "0" (__addr), "1" (__count));
+}
diff --git a/tests/syntax/oracle/asm_with_contracts.res.oracle b/tests/syntax/oracle/asm_with_contracts.res.oracle
index 915bed6e6f7..de45604755b 100644
--- a/tests/syntax/oracle/asm_with_contracts.res.oracle
+++ b/tests/syntax/oracle/asm_with_contracts.res.oracle
@@ -25,4 +25,23 @@ int f(int z)
return x;
}
+__inline static void insw(unsigned short __port, void *__addr,
+ unsigned long __count)
+{
+ /*@ assigns __addr, __count, *((char *)__addr + (..));
+ assigns __addr
+ \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+ assigns __count
+ \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+ assigns *((char *)__addr + (..))
+ \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+ */
+ __asm__ volatile (
+ "cld ; rep ; insw"
+ : "=D" (__addr), "=c" (__count)
+ : "d" (__port), "0" (__addr), "1" (__count)
+ );
+ return;
+}
+
--
GitLab